Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/ExtrSCaml.v

Last active January 7, 2020 15:13
Show Gist options
  • Save yoshihiro503/7a4161917e01973a8c619edcd37ae1bd to your computer and use it in GitHub Desktop.
Save yoshihiro503/7a4161917e01973a8c619edcd37ae1bd to your computer and use it in GitHub Desktop.
Download ZIP
Raw
_CoqProject
SCaml.v
ExtrSCaml.v
SCamlTest.v
Raw
ExtrSCaml.v
Require Export ExtrOcamlBasic.
Require Import SCaml.
Extract Inlined Constant int => "SCaml.int".
Extract Inlined Constant operation => "Scaml.operation".
Extract Inlined Constant int_plus => "SCaml.(+)".
Extract Inlined Constant int_sub => "SCaml.(-)".
Raw
SCaml.v
Parameter nat : Set.
Parameter int : Set.
Parameter int_plus : int -> int -> int.
Parameter int_sub : int -> int -> int.
Infix "+" := int_plus.
Infix "-" := int_sub.
Parameter operation : Set.
Raw
SCamlTest.v
Require Import SCaml ExtrSCaml.
Inductive action : Set :=
| Increment (i : int)
| Decrement (i : int).
Definition main action storage :=
match action with
| Increment i => (nil : list operation, storage + i)
| Decrement i => (nil : list operation, storage - i)
end.
Extraction Language OCaml.
Extraction "test.ml" main.
@yoshihiro503
Copy link
Author

yoshihiro503 commented Jan 7, 2020 •
edited
Loading

A simple smart contract using Coq. This code compiled to smart contract VM language Michelson via SCaml.

The VM code obtained is here:

parameter (or int int) ;
storage int ;
code { { /* defs */ } ;
       { /* entry point init */ DUP ; CDR ; DIP { CAR } } ;
       { /* entry point */
         { /* entry main_1007 */
           { /* __storage_1172 */
             { /* = storage_1009, = __v_1173, = __storage_1163 */ { /* var storage_1160 */ DUP } } } ;
           { /* = __v_1168, = __parameter0_1175, = parameter0_1008, = __v_1176, = __parameter0_1162 */
             { /* var global_param_1161 */ DIG 2 ; DUP ; DUG 3 } } ;
           IF_LEFT
             { { /* = __i_1165, = i_1010 */ { /* var __l_1169 */ DUP } } ;
               { /* var __storage_1172 */ DIG 2 ; DUP ; DUG 3 } ;
               ADD ;
               NIL operation ;
               PAIR ;
               DIP { DROP } }
             { { /* = __i_1167, = i_1011 */ { /* var __r_1170 */ DUP } } ;
               { /* var __storage_1172 */ DIG 2 ; DUP ; DUG 3 } ;
               SUB ;
               NIL operation ;
               PAIR ;
               DIP { DROP } } ;
           { /* clean __storage_1172 */ DIP { DROP } } } } ;
       { /* final clean up */ DIP { DROP 2 } } } ;

Requirement

  • Coq version 8.10
  • SCaml version 1.0.0

How to build

coq_makefile -f _CoqProject -o Makefile
make && rm test.mli
scamlc test.ml

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment