Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Verified translation #1

Draft
wants to merge 6 commits into
base: verified_translation
Choose a base branch
from
Draft

Verified translation #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
0838ed9
Updated ADT
joaosreis Jul 11, 2022
c24cab3
Verification of Michelson to Tezla translation
mariojppereira Jun 26, 2022
8688704
Verified Michelson to Tezla translation
mariojppereira Jun 27, 2022
33470f4
Completed definition of AST for typed ADT in Edo
mariojppereira Jun 27, 2022
1e2d2cf
Added dune instructions for Coq theories. Fixed Coq definitions
joaosreis Jul 11, 2022
1e0c537
Changed the syntax definition. Working on semantics
joaosreis Jul 14, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 51 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,3 +31,54 @@ _opam/

# Coverage test results
_coverage/
# Created by https://www.toptal.com/developers/gitignore/api/coq
# Edit at https://www.toptal.com/developers/gitignore?templates=coq

### Coq ###
.*.aux
.*.d
*.a
*.cma
*.cmi
*.cmo
*.cmx
*.cmxa
*.cmxs
*.glob
*.ml.d
*.ml4.d
*.mlg.d
*.mli.d
*.mllib.d
*.mlpack.d
*.native
*.o
*.v.d
*.vio
*.vo
*.vok
*.vos
.coq-native
.csdp.cache
.lia.cache
.nia.cache
.nlia.cache
.nra.cache
csdp.cache
lia.cache
nia.cache
nlia.cache
nra.cache
native_compute_profile_*.data

# generated timing files
*.timing.diff
*.v.after-timing
*.v.before-timing
*.v.timing
time-of-build-after.log
time-of-build-before.log
time-of-build-both.log
time-of-build-pretty.log

# End of https://www.toptal.com/developers/gitignore/api/coq
16 changes: 16 additions & 0 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
all: Makefile.coq
@+$(MAKE) -f Makefile.coq all

clean: Makefile.coq
@+$(MAKE) -f Makefile.coq cleanall
@rm -f Makefile.coq Makefile.coq.conf

Makefile.coq: _CoqProject
coq_makefile -f _CoqProject -o Makefile.coq

force _CoqProject Makefile: ;

%: Makefile.coq force
@+$(MAKE) -f Makefile.coq $@

.PHONY: all clean force
8 changes: 8 additions & 0 deletions _CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
-Q src/verified Tezla

src/verified/Adt.v
src/verified/Common_adt.v
src/verified/Edo_adt.v
src/verified/Semantics.v
src/verified/Typ.v
src/verified/Var.v
5 changes: 4 additions & 1 deletion dune-project
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
(lang dune 2.8)

(using coq 0.3)

(name tezla)

(generate_opam_files true)
Expand Down Expand Up @@ -35,4 +37,5 @@
(>= v0.15))
bignum
michelson-adt
michelson-parser))
michelson-parser
coq))
218 changes: 166 additions & 52 deletions src/lib/adt/adt.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,17 +65,51 @@ and expr_t =
| E_car of var
| E_cdr of var
| E_abs of var
| E_neg of var
| E_not of var
| E_add of var * var
| E_sub of var * var
| E_mul of var * var
| E_div of var * var
| E_shiftL of var * var
| E_shiftR of var * var
| E_and of var * var
| E_or of var * var
| E_xor of var * var
| E_neg_nat of var
| E_neg_int of var
| E_neg_bls12_381_g1 of var
| E_neg_bls12_381_g2 of var
| E_neg_bls12_381_fr of var
| E_not_bool of var
| E_not_nat of var
| E_not_int of var
| E_add_nat of var * var
| E_add_nat_int of var * var
| E_add_int of var * var
| E_add_timestamp_int of var * var
| E_add_mutez of var * var
| E_add_bls12_381_g1 of var * var
| E_add_bls12_381_g2 of var * var
| E_add_bls12_381_fr of var * var
| E_sub_nat of var * var
| E_sub_nat_int of var * var
| E_sub_int of var * var
| E_sub_timestamp_int of var * var
| E_sub_timestamp of var * var
| E_sub_mutez of var * var
| E_mul_nat of var * var
| E_mul_nat_int of var * var
| E_mul_int of var * var
| E_mul_mutez_nat of var * var
| E_mul_bls12_381_g1_bls12_381_fr of var * var
| E_mul_bls12_381_g2_bls12_381_fr of var * var
| E_mul_bls12_381_fr_bls12_381_fr of var * var
| E_mul_nat_bls12_381_fr of var * var
| E_mul_int_bls12_381_fr of var * var
| E_ediv_nat of var * var
| E_ediv_nat_int of var * var
| E_ediv_int of var * var
| E_ediv_mutez_nat of var * var
| E_ediv_mutez of var * var
| E_lsl of var * var
| E_lsr of var * var
| E_and_bool of var * var
| E_and_nat of var * var
| E_and_int_nat of var * var
| E_or_bool of var * var
| E_or_nat of var * var
| E_xor_bool of var * var
| E_xor_nat of var * var
| E_eq of var
| E_neq of var
| E_lt of var
Expand All @@ -92,12 +126,20 @@ and expr_t =
| E_right of var * adt_typ
| E_some of var
| E_none of adt_typ
| E_mem of var * var
| E_get of var * var
| E_update of var * var * var
| E_concat of var * var
| E_concat_list of var
| E_slice of var * var * var
| E_mem_set of var * var
| E_mem_map of var * var
| E_mem_big_map of var * var
| E_get_map of var * var
| E_get_big_map of var * var
| E_update_set of var * var * var
| E_update_map of var * var * var
| E_update_big_map of var * var * var
| E_concat_string of var * var
| E_concat_bytes of var * var
| E_concat_list_string of var
| E_concat_list_bytes of var
| E_slice_string of var * var * var
| E_slice_bytes of var * var * var
| E_pack of var
| E_unpack of adt_typ * var
| E_self
Expand All @@ -120,7 +162,11 @@ and expr_t =
| E_unlift_or_right of var
| E_hd of var
| E_tl of var
| E_size of var
| E_size_list of var
| E_size_set of var
| E_size_map of var
| E_size_string of var
| E_size_bytes of var
| E_isnat of var
| E_int_of_nat of var
| E_chain_id
Expand All @@ -132,10 +178,9 @@ and expr_t =
| E_empty_map of adt_typ * adt_typ
| E_empty_big_map of adt_typ * adt_typ
| E_apply of var * var
| E_append of var * var
| E_list_append of var * var
| E_special_empty_list of ttyp
| E_special_empty_map of ttyp * ttyp
| E_create_account_operation of var * var * var * var
| E_create_account_address of var * var * var * var
| E_voting_power of var
| E_keccak of var
Expand Down Expand Up @@ -167,16 +212,19 @@ and stmt_t =
| S_skip
| S_drop of var list
| S_swap
| S_dig
| S_dug
| S_dig of Bigint.t
| S_dug of Bigint.t
| S_if of var * stmt * stmt
| S_if_none of var * stmt * stmt
| S_if_left of var * stmt * stmt
| S_if_cons of var * stmt * stmt
| S_loop of var * stmt
| S_loop_left of var * stmt
| S_map of var * stmt
| S_iter of var * stmt
| S_map_list of var * stmt
| S_map_map of var * stmt
| S_iter_set of var * stmt
| S_iter_list of var * stmt
| S_iter_map of var * stmt
| S_failwith of var
| S_return of var
[@@deriving ord, sexp]
Expand Down Expand Up @@ -224,8 +272,14 @@ module Expr = Make_common (struct
| E_car e -> [%string "CAR %{e#Var}"]
| E_cdr e -> [%string "CDR %{e#Var}"]
| E_abs e -> [%string "ABS %{e#Var}"]
| E_neg e -> [%string "NEG %{e#Var}"]
| E_not e -> [%string "NOT %{e#Var}"]
| E_neg_nat e -> [%string "NEG_nat %{e#Var}"]
| E_neg_int e -> [%string "NEG_int %{e#Var}"]
| E_neg_bls12_381_g1 e -> [%string "NEG_bls12_381_g1 %{e#Var}"]
| E_neg_bls12_381_g2 e -> [%string "NEG_bls12_381_g2 %{e#Var}"]
| E_neg_bls12_381_fr v -> [%string "NEG_bls12_381_fr %{v#Var}"]
| E_not_bool e -> [%string "NOT_bool %{e#Var}"]
| E_not_int e -> [%string "NOT_int %{e#Var}"]
| E_not_nat e -> [%string "NOT_nat %{e#Var}"]
| E_eq e -> [%string "EQ %{e#Var}"]
| E_neq e -> [%string "NEQ %{e#Var}"]
| E_lt e -> [%string "LT %{e#Var}"]
Expand All @@ -243,26 +297,81 @@ module Expr = Make_common (struct
| E_hash_key e -> [%string "HASH_KEY %{e#Var}"]
| E_unit -> "UNIT"
| E_none t -> [%string "NONE %{typ_to_string t}"]
| E_add (v_1, v_2) -> [%string "ADD %{v_1#Var} %{v_2#Var}"]
| E_sub (v_1, v_2) -> [%string "SUB %{v_1#Var} %{v_2#Var}"]
| E_mul (v_1, v_2) -> [%string "MUL %{v_1#Var} %{v_2#Var}"]
| E_div (v_1, v_2) -> [%string "EDIV %{v_1#Var} %{v_2#Var}"]
| E_shiftL (v_1, v_2) -> [%string "LSL %{v_1#Var} %{v_2#Var}"]
| E_shiftR (v_1, v_2) -> [%string "LSR %{v_1#Var} %{v_2#Var}"]
| E_and (v_1, v_2) -> [%string "AND %{v_1#Var} %{v_2#Var}"]
| E_or (v_1, v_2) -> [%string "OR %{v_1#Var} %{v_2#Var}"]
| E_xor (v_1, v_2) -> [%string "XOR %{v_1#Var} %{v_2#Var}"]
| E_add_int (v_1, v_2) -> [%string "ADD_int %{v_1#Var} %{v_2#Var}"]
| E_add_bls12_381_fr (v_1, v_2) ->
[%string "ADD_bls12_381_fr %{v_1#Var} %{v_2#Var}"]
| E_add_bls12_381_g1 (v_1, v_2) ->
[%string "ADD_bls12_381_g1 %{v_1#Var} %{v_2#Var}"]
| E_add_mutez (v_1, v_2) -> [%string "ADD_mutez %{v_1#Var} %{v_2#Var}"]
| E_add_nat (v_1, v_2) -> [%string "ADD_nat %{v_1#Var} %{v_2#Var}"]
| E_add_nat_int (v_1, v_2) -> [%string "ADD_nat_int %{v_1#Var} %{v_2#Var}"]
| E_add_timestamp_int (v_1, v_2) ->
[%string "ADD_timestamp_int %{v_1#Var} %{v_2#Var}"]
| E_add_bls12_381_g2 (v_1, v_2) ->
[%string "ADD_bls12_381_g2 %{v_1#Var} %{v_2#Var}"]
| E_sub_int (v_1, v_2) -> [%string "SUB_int %{v_1#Var} %{v_2#Var}"]
| E_sub_mutez (v_1, v_2) -> [%string "SUB_mutez %{v_1#Var} %{v_2#Var}"]
| E_sub_nat (v_1, v_2) -> [%string "SUB_nat %{v_1#Var} %{v_2#Var}"]
| E_sub_nat_int (v_1, v_2) -> [%string "SUB_nat_int %{v_1#Var} %{v_2#Var}"]
| E_sub_timestamp (v_1, v_2) ->
[%string "SUB_timestamp %{v_1#Var} %{v_2#Var}"]
| E_sub_timestamp_int (v_1, v_2) ->
[%string "SUB_timestamp_int %{v_1#Var} %{v_2#Var}"]
| E_mul_bls12_381_fr_bls12_381_fr (v_1, v_2) ->
[%string "MUL_bls12_381_fr_bls12_381_fr %{v_1#Var} %{v_2#Var}"]
| E_mul_bls12_381_g1_bls12_381_fr (v_1, v_2) ->
[%string "MUL_bls12_381_g1_bls12_381_fr %{v_1#Var} %{v_2#Var}"]
| E_mul_bls12_381_g2_bls12_381_fr (v_1, v_2) ->
[%string "MUL_bls12_381_g2_bls12_381_fr %{v_1#Var} %{v_2#Var}"]
| E_mul_int (v_1, v_2) -> [%string "MUL_int %{v_1#Var} %{v_2#Var}"]
| E_mul_int_bls12_381_fr (v_1, v_2) ->
[%string "MUL_int_bls12_381_fr %{v_1#Var} %{v_2#Var}"]
| E_mul_mutez_nat (v_1, v_2) ->
[%string "MUL_mutez_nat %{v_1#Var} %{v_2#Var}"]
| E_mul_nat (v_1, v_2) -> [%string "MUL_mutez_nat %{v_1#Var} %{v_2#Var}"]
| E_mul_nat_bls12_381_fr (v_1, v_2) ->
[%string "MUL_nat_bls12_381_fr %{v_1#Var} %{v_2#Var}"]
| E_mul_nat_int (v_1, v_2) -> [%string "MUL_nat_int %{v_1#Var} %{v_2#Var}"]
| E_ediv_int (v_1, v_2) -> [%string "EDIV_int %{v_1#Var} %{v_2#Var}"]
| E_ediv_mutez (v_1, v_2) -> [%string "EDIV_mutez %{v_1#Var} %{v_2#Var}"]
| E_ediv_mutez_nat (v_1, v_2) ->
[%string "EDIV_mutez_nat %{v_1#Var} %{v_2#Var}"]
| E_ediv_nat (v_1, v_2) -> [%string "EDIV_nat %{v_1#Var} %{v_2#Var}"]
| E_ediv_nat_int (v_1, v_2) ->
[%string "EDIV_nat_int %{v_1#Var} %{v_2#Var}"]
| E_lsl (v_1, v_2) -> [%string "LSL %{v_1#Var} %{v_2#Var}"]
| E_lsr (v_1, v_2) -> [%string "LSR %{v_1#Var} %{v_2#Var}"]
| E_and_bool (v_1, v_2) -> [%string "AND_bool %{v_1#Var} %{v_2#Var}"]
| E_and_int_nat (v_1, v_2) -> [%string "AND_int_nat %{v_1#Var} %{v_2#Var}"]
| E_and_nat (v_1, v_2) -> [%string "AND_nat %{v_1#Var} %{v_2#Var}"]
| E_or_bool (v_1, v_2) -> [%string "OR_bool %{v_1#Var} %{v_2#Var}"]
| E_or_nat (v_1, v_2) -> [%string "OR_nat %{v_1#Var} %{v_2#Var}"]
| E_xor_bool (v_1, v_2) -> [%string "XOR_bool %{v_1#Var} %{v_2#Var}"]
| E_xor_nat (v_1, v_2) -> [%string "XOR_nat %{v_1#Var} %{v_2#Var}"]
| E_compare (v_1, v_2) -> [%string "COMPARE %{v_1#Var} %{v_2#Var}"]
| E_cons (v_1, v_2) -> [%string "CONS %{v_1#Var} %{v_2#Var}"]
| E_pair (v_1, v_2) -> [%string "PAIR %{v_1#Var} %{v_2#Var}"]
| E_mem (v_1, v_2) -> [%string "MEM %{v_1#Var} %{v_2#Var}"]
| E_get (v_1, v_2) -> [%string "GET %{v_1#Var} %{v_2#Var}"]
| E_concat (v_1, v_2) -> [%string "CONCAT %{v_1#Var} %{v_2#Var}"]
| E_concat_list e -> [%string "CONCAT %{e#Var}"]
| E_update (v_1, v_2, v_3) ->
[%string "UPDATE %{v_1#Var} %{v_2#Var} %{v_3#Var}"]
| E_slice (v_1, v_2, v_3) ->
[%string "SLICE %{v_1#Var} %{v_2#Var} %{v_3#Var}"]
| E_mem_big_map (v_1, v_2) -> [%string "MEM_big_map %{v_1#Var} %{v_2#Var}"]
| E_mem_map (v_1, v_2) -> [%string "MEM_map %{v_1#Var} %{v_2#Var}"]
| E_mem_set (v_1, v_2) -> [%string "MEM_set %{v_1#Var} %{v_2#Var}"]
| E_get_map (v_1, v_2) -> [%string "GET_map %{v_1#Var} %{v_2#Var}"]
| E_get_big_map (v_1, v_2) -> [%string "GET_big_map %{v_1#Var} %{v_2#Var}"]
| E_concat_bytes (v_1, v_2) ->
[%string "CONCAT_bytes %{v_1#Var} %{v_2#Var}"]
| E_concat_string (v_1, v_2) ->
[%string "CONCAT_string %{v_1#Var} %{v_2#Var}"]
| E_concat_list_string v -> [%string "CONCAT_list_string %{v#Var}"]
| E_concat_list_bytes v -> [%string "CONCAT_list_bytes %{v#Var}"]
| E_update_set (v_1, v_2, v_3) ->
[%string "UPDATE_set %{v_1#Var} %{v_2#Var} %{v_3#Var}"]
| E_update_map (v_1, v_2, v_3) ->
[%string "UPDATE_map %{v_1#Var} %{v_2#Var} %{v_3#Var}"]
| E_update_big_map (v_1, v_2, v_3) ->
[%string "UPDATE_big_map %{v_1#Var} %{v_2#Var} %{v_3#Var}"]
| E_slice_string (v_1, v_2, v_3) ->
[%string "SLICE_string %{v_1#Var} %{v_2#Var} %{v_3#Var}"]
| E_slice_bytes (v_1, v_2, v_3) ->
[%string "SLICE_bytes %{v_1#Var} %{v_2#Var} %{v_3#Var}"]
| E_check_signature (v_1, v_2, v_3) ->
[%string "CHECK_SIGNATURE %{v_1#Var} %{v_2#Var} %{v_3#Var}"]
| E_unpack (t, v) -> [%string "UNPACK %{typ_to_string t} %{v#Var}"]
Expand Down Expand Up @@ -290,7 +399,7 @@ module Expr = Make_common (struct
[%string "CONTRACT %{typ_to_string t} %{v#Var}"]
| E_create_contract_address (_, v_1, v_2, v_3) ->
[%string "CREATE_CONTRACT {...} %{v_1#Var} %{v_2#Var} %{v_3#Var}"]
| E_operation o -> Operation.to_string o
| E_operation o -> [%string "%{o#Operation}_operation"]
| E_dup v -> [%string "DUP %{v#Var}"]
| E_nil t -> [%string "NIL %{typ_to_string t}"]
| E_empty_set t -> [%string "EMPTY_SET %{typ_to_string t}"]
Expand All @@ -299,16 +408,18 @@ module Expr = Make_common (struct
| E_empty_big_map (t_k, t_v) ->
[%string "EMPTY_BIG_MAP %{typ_to_string t_k} %{typ_to_string t_v}"]
| E_apply (v_1, v_2) -> [%string "APPLY %{v_1#Var} %{v_2#Var}"]
| E_append (v_1, v_2) -> [%string "append(%{v_1#Var}, %{v_2#Var})"]
| E_list_append (v_1, v_2) ->
[%string "list_append(%{v_1#Var}, %{v_2#Var})"]
| E_special_empty_list _ -> "{ }"
| E_special_empty_map _ -> "{ }"
| E_total_voting_power -> "TOTAL_VOTING_POWER"
| E_self_address -> "SELF_address"
| E_level -> "LEVEL"
| E_size v -> [%string "SIZE %{v#Var}"]
| E_create_account_operation (v_1, v_2, v_3, v_4) ->
[%string
"CREATE_ACCOUNT_operation %{v_1#Var} %{v_2#Var} %{v_3#Var} %{v_4#Var}"]
| E_size_bytes v -> [%string "SIZE_bytes %{v#Var}"]
| E_size_string v -> [%string "SIZE_string %{v#Var}"]
| E_size_list v -> [%string "SIZE_list %{v#Var}"]
| E_size_set v -> [%string "SIZE_set %{v#Var}"]
| E_size_map v -> [%string "SIZE_map %{v#Var}"]
| E_create_account_address (v_1, v_2, v_3, v_4) ->
[%string
"CREATE_ACCOUNT_address %{v_1#Var} %{v_2#Var} %{v_3#Var} %{v_4#Var}"]
Expand Down Expand Up @@ -362,9 +473,12 @@ module Stmt = struct
{ s with value = S_if_none (c, simpl s_1, simpl s_2) }
| S_loop (c, s) -> { s with value = S_loop (c, simpl s) }
| S_loop_left (c, s) -> { s with value = S_loop_left (c, simpl s) }
| S_iter (c, s) -> { s with value = S_iter (c, simpl s) }
| S_map (x, s) -> { s with value = S_map (x, simpl s) }
| S_skip | S_swap | S_dig | S_dug | S_assign _ | S_drop _ | S_failwith _
| S_iter_list (c, s) -> { s with value = S_iter_list (c, simpl s) }
| S_iter_set (c, s) -> { s with value = S_iter_set (c, simpl s) }
| S_iter_map (c, s) -> { s with value = S_iter_map (c, simpl s) }
| S_map_map (x, s) -> { s with value = S_map_map (x, simpl s) }
| S_map_list (x, s) -> { s with value = S_map_list (x, simpl s) }
| S_skip | S_swap | S_dig _ | S_dug _ | S_assign _ | S_drop _ | S_failwith _
| S_return _ ->
s
end
Loading