Skip to content

Commit

Permalink
Completed definition of AST for typed ADT in Edo
Browse files Browse the repository at this point in the history
  • Loading branch information
@mariojppereira
mariojppereira committed Jun 27, 2022
1 parent e1d0665 commit 9368535
Show file tree
Hide file tree
Showing 3 changed files with 308 additions and 1 deletion.
106 changes: 105 additions & 1 deletion verified/Adt.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,13 @@ From Coq Require Import Bool.Bool.
From Coq Require Import Strings.String.

From Tezla Require Import Edo_adt.
From Tezla Require Import Common_adt.
From Tezla Require Import Var.
From Tezla Require Import Operation.

Definition var : Type := Var.t.
Definition adt_typ : Type := Adt.typ.
Definition node (A: Type) : Type := Node.t A.

Inductive data_t : Type :=
| D_int : Z -> data_t
Expand All @@ -15,4 +20,103 @@ Inductive data_t : Type :=
| D_pair : data -> data -> data_t

with data : Type :=
data_raw : adt_typ -> data_t -> data.
data_raw : node (adt_typ * data_t) -> data

with expr_t : Type :=
| E_var : var -> expr_t
| E_push : data -> expr_t
| E_car : var -> expr_t
| E_cdr : var -> expr_t
| E_abs : var -> expr_t
| E_neg : var -> expr_t
| E_not : var -> expr_t
| E_add : var -> var -> expr_t
| E_sub : var -> var -> expr_t
| E_mul : var -> var -> expr_t
| E_div : var -> var -> expr_t
| E_shiftL : var -> var -> expr_t
| E_shiftR : var -> var -> expr_t
| E_and : var -> var -> expr_t
| E_or : var -> var -> expr_t
| E_xor : var -> var -> expr_t
| E_eq : var -> expr_t
| E_neq : var -> expr_t
| E_lt : var -> expr_t
| E_gt : var -> expr_t
| E_leq : var -> expr_t
| E_geq : var -> expr_t
| E_compare : var -> var -> expr_t
| E_cons : var -> var -> expr_t
| E_operation : operation -> expr_t
| E_unit : expr_t
| E_pair : var -> var -> expr_t
| E_pair_n : var list -> expr_t
| E_left : var -> adt_typ -> expr_t
| E_right : var -> adt_typ -> expr_t
| E_some : var -> expr_t
| E_none : adt_typ -> expr_t
| E_mem : var -> var -> expr_t
| E_get : var -> var -> expr_t
| E_update : var -> var -> var -> expr_t
| E_concat : var -> var -> expr_t
| E_concat_list : var -> expr_t
| E_slice : var -> var -> var -> expr_t
| E_pack : var -> expr_t
| E_unpack : adt_typ -> var -> expr_t
| E_self : expr_t
| E_contract_of_address : adt_typ -> var -> expr_t
| E_implicit_account : var -> expr_t
| E_now : expr_t
| E_amount : expr_t
| E_balance
| E_check_signature : var -> var -> var -> expr_t
| E_blake2b : var -> expr_t
| E_sha256 : var -> expr_t
| E_sha512 : var -> expr_t
| E_hash_key : var -> expr_t
| E_source : expr_t
| E_sender : expr_t
| E_address_of_contract : var -> expr_t
| E_create_contract_address : Edo_adt.Typed_adt.program -> var -> var -> var -> expr_t
| E_unlift_option : var -> expr_t
| E_unlift_or_left : var -> expr_t
| E_unlift_or_right : var -> expr_t
| E_hd : var -> expr_t
| E_tl : var -> expr_t
| E_size : var -> expr_t
| E_isnat : var -> expr_t
| E_int_of_nat : var -> expr_t
| E_chain_id : expr_t
| E_lambda : adt_typ -> var -> stmt -> expr_t
| E_exec : var -> var -> expr_t
| E_dup : var -> expr_t
| E_nil : adt_typ -> expr_t
| E_empty_set : adt_typ -> expr_t
| E_empty_map : adt_typ -> adt_typ -> expr_t
| E_empty_big_map : adt_typ -> adt_typ -> expr_t
| E_apply : var -> var -> expr_t
| E_append : var -> var -> expr_t
| E_special_empty_list : ttyp -> expr_t
| E_special_empty_map : ttyp -> ttyp -> expr_t
| E_create_account_operation : var -> var -> var -> var -> expr_t
| E_create_account_address : var -> var -> var -> var -> expr_t
| E_voting_power : var -> expr_t
| E_keccak : var -> expr_t
| E_sha3 : var -> expr_t
| E_total_voting_power
| E_pairing_check : var -> expr_t
| E_sapling_verify_update : var -> var -> expr_t
| E_sapling_empty_state : Bigint.t -> expr_t
| E_ticket : var -> var -> expr_t
| E_read_ticket_pair : var -> expr_t
| E_read_ticket_ticket : var -> expr_t
| E_split_ticket : var -> var -> expr_t
| E_join_ticket : var -> expr_t
| E_self_address : expr_t
| E_level : expr_t
| E_open_chest : var -> var -> var -> expr_t
| E_get_and_update_val : var -> var -> var -> expr_t
| E_get_and_update_map : var -> var -> var -> expr_t
| E_dup_n : Bigint.t -> var -> expr_t
| E_get_n : Bigint.t -> var -> expr_t
| E_update_n : Bigint.t -> var -> var -> expr_t.
196 changes: 196 additions & 0 deletions verified/Edo_adt.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ From Tezla Require Import Common_adt.
From Coq Require Import Lists.List.
From Coq Require Import Init.Datatypes.
From Coq Require Import ZArith.
From Coq Require Import Bool.Bool.
From Coq Require Import Strings.String.

Module Adt.

Expand Down Expand Up @@ -88,3 +90,197 @@ Module Typ.
self : t' -> list Annot.t -> t.

End Typ.

Module Typed_adt.

Definition annot : Type := Annot.t.
Definition node (A: Type) : Type := Node.t A.
Definition typ : Type := Adt.typ.

Inductive data_t : Type :=
| D_int : Z -> data_t
| D_nat : Z -> data_t
| D_string : string -> data_t
(* | D_bytes of Bytes.t *)
| D_unit : data_t
| D_bool : bool-> data_t
| D_pair : data -> data -> data_t
| D_left : data -> data_t
| D_right : data -> data_t
| D_some : data -> data_t
| D_none : data_t
| D_list : list data -> data_t
| D_map : list (data * data) -> data_t
| D_instruction : inst -> data_t

with data : Type :=
| self : node (typ * data_t) -> data

with inst_t : Type :=
| I_abs : inst_t
| I_add_nat : inst_t
| I_add_nat_int : inst_t
| I_add_int : inst_t
| I_add_timestamp_int : inst_t
| I_add_mutez : inst_t
| I_add_bls12_381_g1 : inst_t
| I_add_bls12_381_g2 : inst_t
| I_add_bls12_381_fr : inst_t
| I_address : inst_t
| I_amount : inst_t
| I_and_bool : inst_t
| I_and_nat : inst_t
| I_and_int_nat : inst_t
| I_apply : inst_t
| I_balance : inst_t
| I_blake2b : inst_t
| I_car : inst_t
| I_cdr : inst_t
| I_chain_id : inst_t
| I_check_signature : inst_t
| I_compare : inst_t
| I_concat_string : inst_t
| I_concat_list_string : inst_t
| I_concat_bytes : inst_t
| I_concat_list_bytes : inst_t
| I_cons : inst_t
| I_contract : Adt.typ -> inst_t
| I_create_contract : program -> inst_t
| I_dig : Z -> inst_t
| I_dip : inst -> inst_t
| I_dip_n : Z -> inst -> inst_t
| I_drop : Z -> inst_t
| I_dug : Z -> inst_t
| I_dup : Z -> inst_t
| I_ediv_nat : inst_t
| I_ediv_nat_int : inst_t
| I_ediv_int : inst_t
| I_ediv_mutez_nat : inst_t
| I_ediv_mutez : inst_t
| I_empty_big_map : Adt.typ -> Adt.typ -> inst_t
| I_empty_map : Adt.typ -> Adt.typ -> inst_t
| I_empty_set : Adt.typ -> inst_t
| I_eq : inst_t
| I_exec : inst_t
| I_failwith : inst_t
| I_ge : inst_t
| I_get_map : inst_t
| I_get_big_map : inst_t
| I_get_n : Z -> inst_t
| I_get_and_update_map : inst_t
| I_get_and_update_big_map : inst_t
| I_gt : inst_t
| I_hash_key : inst_t
| I_if : inst -> inst -> inst_t
| I_if_cons : inst -> inst -> inst_t
| I_if_left : inst -> inst -> inst_t
| I_if_none : inst -> inst -> inst_t
| I_implicit_account : inst_t
| I_int_nat : inst_t
| I_int_bls12_381_fr : inst_t
| I_isnat : inst_t
| I_iter_set : inst -> inst_t
| I_iter_map : inst -> inst_t
| I_iter_list : inst -> inst_t
| I_join_tickets : inst_t
| I_keccak : inst_t
| I_lambda : Adt.typ -> Adt.typ -> inst -> inst_t
| I_le : inst_t
| I_left : Adt.typ -> inst_t
| I_level : inst_t
| I_loop : inst -> inst_t
| I_loop_left : inst -> inst_t
| I_lsl : inst_t
| I_lsr : inst_t
| I_lt : inst_t
| I_map_list : inst -> inst_t
| I_map_map : inst -> inst_t
| I_mem_set : inst_t
| I_mem_map : inst_t
| I_mem_big_map : inst_t
| I_mul_nat : inst_t
| I_mul_nat_int : inst_t
| I_mul_int : inst_t
| I_mul_mutez_nat : inst_t
| I_mul_bls12_381_g1_bls12_381_fr : inst_t
| I_mul_bls12_381_g2_bls12_381_fr : inst_t
| I_mul_bls12_381_fr_bls12_381_fr : inst_t
| I_mul_nat_bls12_381_fr : inst_t
| I_mul_int_bls12_381_fr : inst_t
| I_neg_nat : inst_t
| I_neg_int : inst_t
| I_neg_bls12_381_g1 : inst_t
| I_neg_bls12_381_g2 : inst_t
| I_neg_bls12_381_fr : inst_t
| I_neq : inst_t
| I_never : inst_t
| I_nil : Adt.typ -> inst_t
| I_none : Adt.typ -> inst_t
| I_not_bool : inst_t
| I_not_nat : inst_t
| I_not_int : inst_t
| I_now : inst_t
| I_or_bool : inst_t
| I_or_nat : inst_t
| I_pack : inst_t
| I_pair : inst_t
| I_pair_n : Z -> inst_t
| I_pairing_check : inst_t
| I_push : data -> inst_t
| I_read_ticket : inst_t
| I_right : Adt.typ -> inst_t
| I_sapling_empty_state : Z -> inst_t
| I_sapling_verify_update : inst_t
| I_self : inst_t
| I_self_address : inst_t
| I_sender : inst_t
| I_set_delegate : inst_t
| I_sha256 : inst_t
| I_sha512 : inst_t
| I_sha3 : inst_t
| I_size_set : inst_t
| I_size_map : inst_t
| I_size_list : inst_t
| I_size_string : inst_t
| I_size_bytes : inst_t
| I_slice_string : inst_t
| I_slice_bytes : inst_t
| I_some : inst_t
| I_source : inst_t
| I_split_ticket : inst_t
| I_sub_nat : inst_t
| I_sub_nat_int : inst_t
| I_sub_int : inst_t
| I_sub_timestamp_int : inst_t
| I_sub_timestamp : inst_t
| I_sub_mutez : inst_t
| I_swap : inst_t
| I_ticket : inst_t
| I_total_voting_power : inst_t
| I_transfer_tokens : inst_t
| I_unit : inst_t
| I_unpack : Adt.typ -> inst_t
| I_unpair : Z -> inst_t
| I_update_set : inst_t
| I_update_map : inst_t
| I_update_big_map : inst_t
| I_update_n : Z -> inst_t
| I_voting_power : inst_t
| I_xor_bool : inst_t
| I_xor_nat : inst_t
| I_seq : list inst -> inst_t
| I_noop : inst_t
| I_open_chest : inst_t
| I_cast : Adt.typ -> inst_t
| I_create_account : inst_t

with inst : Type :=
Inst : inst_t -> node (list annot) -> inst

with seq : Type :=
| Seq_i : inst -> seq | Seq_s : inst -> seq -> seq

with program : Type :=
Program (param : typ) (storage : typ) (code : inst).

End Typed_adt.
7 changes: 7 additions & 0 deletions verified/Operation.v
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
From Tezla Require Import Var.
From Tezla Require Import Edo_adt.

Definition var : Type := Var.t.

Inductive t : Type :=
| O_create_contract : Typed_adt.program -> var -> var -> var -> var -> t.

0 comments on commit 9368535

Please sign in to comment.