https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: b5a01c91f716d9562fb83af8ba8307482df69c4c authored by zhenlei on 30 July 2019, 15:44:25 UTC
[enable_pause_spec]en cours
[enable_pause_spec]en cours
Tip revision: b5a01c9
semantics.v
(* Open Source License *)
(* Copyright (c) 2019 Nomadic Labs. <contact@nomadic-labs.com> *)
(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)
(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)
(* Oprational semantics of the Michelson language *)
Require Import ZArith.
Require Import String.
Require Import syntax macros.
Require NPeano.
Require Eqdep_dec.
Require Import comparable error.
Module EnvDef(C:ContractContext)(S : SYNTAX C).
Export C.
Module macros := Macros C S. Export macros.
Definition Mtype_eq (m : M type) (b : type) : Datatypes.bool :=
match m with
| Failed _ _ => false
| Return _ a =>
if (type_decidable a b) then true else false
end.
Lemma Mtype_eq_intro {m b} : m = Return _ b -> Mtype_eq m b.
Proof.
destruct m.
- discriminate.
- intro H; injection H; intro He.
simpl.
case (type_decidable t b).
+ intro; constructor.
+ intro; contradiction.
Defined.
Fixpoint data (a : type) {struct a} : Set :=
match a with
| Comparable_type b => comparable_data b
| unit => Datatypes.unit
| signature => signature_constant
| operation => operation_constant
| key => key_constant
| pair a b => data a * data b
| or a _ b _ => sum (data a) (data b)
| option a => Datatypes.option (data a)
| list a => Datatypes.list (data a)
| set a => set.set (comparable_data a) (compare a)
| map a b => map.map (comparable_data a) (data b) (compare a)
| big_map a b => map.map (comparable_data a) (data b) (compare a)
| lambda a b =>
instruction None (a ::: nil) (b ::: nil)
| contract a =>
{s : address_constant & {an : annot_o | Mtype_eq (get_contract_type_with_entrypoint s an) a }}
end.
Record proto_env : Set :=
mk_proto_env
{
create_contract : forall g p,
comparable_data key_hash ->
Datatypes.option (comparable_data key_hash) ->
Datatypes.bool -> Datatypes.bool -> tez.mutez ->
instruction (Some p)
(pair (type_of_entrypoint_tree p) g ::: nil)
(pair (list operation) g ::: nil) ->
data g -> data (pair operation address);
create_account :
comparable_data key_hash ->
Datatypes.option (comparable_data key_hash) ->
Datatypes.bool -> tez.mutez ->
data (pair operation (contract unit));
transfer_tokens : forall p,
data p -> tez.mutez -> data (contract p) ->
data operation;
set_delegate : Datatypes.option (comparable_data key_hash) ->
data operation;
balance : tez.mutez;
address_ : forall p, data (contract p) -> data address;
contract_ : forall p, Datatypes.option annotation -> data address ->
data (option (contract p));
source : data address;
sender : data address;
amount : tez.mutez;
implicit_account :
comparable_data key_hash -> data (contract unit);
steps_to_quota : N;
now : comparable_data timestamp;
hash_key : data key -> comparable_data key_hash;
pack : forall a, data a -> data bytes;
unpack : forall a, data bytes -> data (option a);
blake2b : data bytes -> data bytes;
sha256 : data bytes -> data bytes;
sha512 : data bytes -> data bytes;
check_signature :
data key -> data signature -> data bytes -> data bool
}.
End EnvDef.
Module Type Env(C:ContractContext)(S : SYNTAX C).
Include EnvDef C S.
Parameter env:proto_env.
End Env.
Module Semantics(C:ContractContext)(S : SYNTAX C)(E:Env C S).
Export E.
Fixpoint stack (t : stack_type) : Set :=
match t with
| nil => Datatypes.unit
| cons a A => data a * stack A
end.
(** Stack manipulation *)
Inductive stack_ind : stack_type -> Set -> Prop :=
| stack_nil : stack_ind nil Datatypes.unit
| stack_cons : forall a A S,
stack_ind A S -> stack_ind (cons a A) (data a * S).
Lemma stack_iff_stack_ind : forall (t : stack_type) (s : Set),
stack t = s <-> stack_ind t s.
Proof.
intros t.
induction t as [|a t]; intros s; simpl.
- split; intros; subst.
+ constructor.
+ inversion H; reflexivity.
- split; intros; subst.
+ constructor. rewrite <- (IHt (stack t)); reflexivity.
+ inversion H; subst.
assert (stack t = S) by (rewrite (IHt S); assumption); subst; reflexivity.
Qed.
Lemma nltz : forall n: Datatypes.nat, n < 0 -> False.
Proof. intros; omega. Qed.
Definition stack_app {l1} {l2} (S1 : stack l1) (S2 : stack l2) : stack (l1+++l2).
Proof.
induction l1 as [|a l1]; simpl.
- assumption.
- inversion S1. split; auto.
Qed.
(* Dig stuff *)
Fixpoint stacktype_split_dig (l : stack_type) (n : Datatypes.nat) : n < List.length l -> (stack_type * type * stack_type) :=
match l, n with
| List.nil, _ => (fun pf => match nltz n pf with end)
| List.cons x tl, 0 => (fun _ => (nil, x, tl))
| List.cons x xs', S n' => (fun pf => let '(l1, a, l2) := stacktype_split_dig xs' n' (lt_S_n n' (Datatypes.length xs') pf) in (List.cons x l1, a, l2))
end.
Lemma length_app_cons_dig : forall n l1 l2 t,
n = Datatypes.length l1 ->
n < Datatypes.length (l1 +++ t ::: l2).
Proof.
intros n l1 l2 t Hlen.
rewrite List.app_length. rewrite <- Hlen.
simpl. omega.
Qed.
Lemma stacktype_dig_proof_irrelevant : forall l n Hlen1 Hlen2,
stacktype_split_dig l n Hlen1 = stacktype_split_dig l n Hlen2.
Proof.
induction l; intros n Hlen1 Hlen2.
- simpl. specialize (nltz _ Hlen1) as Hfalse. inversion Hfalse.
- simpl. destruct n. reflexivity.
erewrite IHl. erewrite IHl at 2. eauto.
Qed.
Lemma stacktype_split_dig_exact : forall l1 l2 t n (Hlen : n = Datatypes.length l1),
stacktype_split_dig (l1+++t:::l2) n (length_app_cons_dig _ l1 l2 t Hlen) = (l1, t, l2).
Proof.
induction l1; intros l2 t n Hlen; simpl.
- destruct n. reflexivity.
inversion Hlen.
- destruct n. inversion Hlen.
simpl in Hlen; inversion Hlen.
specialize (IHl1 l2 t n H0).
specialize (stacktype_dig_proof_irrelevant (l1+++t:::l2) n (length_app_cons_dig n l1 l2 t H0)
(lt_S_n n (Datatypes.length (l1 +++ t ::: l2))
(length_app_cons_dig (S n) (a ::: l1) l2 t Hlen))) as Hpi.
rewrite <- Hpi. rewrite IHl1. reflexivity.
Qed.
Fixpoint stack_split_dig {l} (SA : stack (l)) (n: Datatypes.nat) (pf : n < List.length l) :
let '(l1, a, l2) := stacktype_split_dig l n pf in (stack l1 * data a * stack l2).
Proof.
generalize dependent n.
induction l as [|a l]; intros n pf. simpl.
+ destruct (nltz n pf).
+ destruct n.
* simpl in *. destruct SA; repeat constructor; assumption.
* simpl in SA.
destruct SA as [x SA].
specialize (IHl SA n (lt_S_n n (Datatypes.length l) pf)). simpl in *. destruct (stacktype_split_dig l n (lt_S_n _ _ pf)) as [[l1' a'] l2'].
destruct IHl as [[sl1' sa'] sl2']; simpl. repeat constructor; assumption.
Defined.
Fixpoint stack_dig {l1 l2 t} (SA : stack (l1+++t:::l2)) (n: Datatypes.nat) (pf : n = Datatypes.length l1) : stack (t:::l1+++l2).
Proof.
specialize (stack_split_dig SA n (length_app_cons_dig _ l1 l2 t pf)).
rewrite stacktype_split_dig_exact.
intro H. simpl in *. destruct H as [[sl1 st] sl2]. split; auto.
apply stack_app; auto.
Defined.
(* Dug stuff *)
Lemma Snltz {A} : forall n',
S n' <= @Datatypes.length A nil -> False.
Proof.
intros n' Hlen; simpl in *. omega.
Qed.
Fixpoint stacktype_split_dug (l : stack_type) (n : Datatypes.nat) : n <= List.length l -> (stack_type * stack_type) :=
match l, n with
| _, 0 => (fun _ => (nil, l))
| List.nil, S n' => (fun pf => match (Snltz n' pf) with end)
| List.cons x xs', S n' => (fun pf => let '(l1, l2) := stacktype_split_dug xs' n' (le_S_n n' (Datatypes.length xs') pf) in (List.cons x l1, l2))
end.
Lemma stacktype_dug_proof_irrelevant : forall l n Hlen1 Hlen2,
stacktype_split_dug l n Hlen1 = stacktype_split_dug l n Hlen2.
Proof.
induction l; intros n Hlen1 Hlen2.
- simpl. destruct n. reflexivity.
simpl in Hlen1; omega.
- simpl. destruct n. reflexivity.
erewrite IHl. erewrite IHl at 2. eauto.
Qed.
Lemma length_app_cons_dug : forall n l1 l2,
n = Datatypes.length l1 ->
n <= Datatypes.length (l1 +++ l2).
Proof.
intros n l1 l2 Hlen.
simpl. rewrite List.app_length. rewrite <- Hlen.
omega.
Qed.
Lemma stacktype_split_dug_exact : forall l1 l2 n (Hlen : n = Datatypes.length l1),
stacktype_split_dug (l1+++l2) n (length_app_cons_dug _ l1 l2 Hlen) = (l1, l2).
Proof.
induction l1; intros l2 n Hlen; simpl.
- destruct n. induction l2; reflexivity.
inversion Hlen.
- destruct n. inversion Hlen.
simpl in Hlen; inversion Hlen.
specialize (IHl1 l2 n H0).
specialize (stacktype_dug_proof_irrelevant (l1+++l2) n (length_app_cons_dug n l1 l2 H0)
(le_S_n n (Datatypes.length (l1 +++ l2))
(length_app_cons_dug (S n) (a ::: l1) l2 Hlen))) as Hpi.
rewrite <- Hpi. rewrite IHl1. reflexivity.
Qed.
Fixpoint stack_split_dug {l} (SA : stack (l)) (n: Datatypes.nat) (pf : n <= List.length l) :
let '(l1, l2) := stacktype_split_dug l n pf in (stack l1 * stack l2).
Proof.
generalize dependent n.
induction l as [|a l]; intros n pf. simpl.
+ destruct n; simpl. constructor; auto.
destruct (Snltz _ pf).
+ destruct n.
* simpl in *. destruct SA; repeat constructor; assumption.
* simpl in SA.
destruct SA as [x SA].
specialize (IHl SA n (le_S_n n (Datatypes.length l) pf)). simpl in *. destruct (stacktype_split_dug l n (le_S_n _ _ pf)) as [l1' l2'].
destruct IHl as [sl1' sl2']; simpl. repeat constructor; assumption.
Defined.
Fixpoint stack_dug {l1 l2 t} (SA : stack (t:::l1+++l2)) (n: Datatypes.nat) (pf : n = Datatypes.length l1) : stack (l1+++t:::l2).
Proof.
inversion SA.
specialize (stack_split_dug H0 n (length_app_cons_dug _ l1 l2 pf)) as Hsplit.
rewrite stacktype_split_dug_exact in Hsplit. destruct Hsplit as [sl1 sl2].
apply stack_app; simpl; auto.
Defined.
Fixpoint concrete_data_to_data (a : type) (d : concrete_data a) : data a :=
match d with
| Int_constant x => x
| Nat_constant x => x
| String_constant x => x
| Timestamp_constant x => x
| Signature_constant x => Mk_sig x
| Key_constant x => Mk_key x
| Key_hash_constant x => Mk_key_hash x
| Mutez_constant (Mk_mutez x) => x
| @Contract_constant _ x an H => existT _ x (exist _ an (Mtype_eq_intro H))
| Unit => tt
| True_ => true
| False_ => false
| Pair a b => (concrete_data_to_data _ a, concrete_data_to_data _ b)
| Left a => inl (concrete_data_to_data _ a)
| Right b => inr (concrete_data_to_data _ b)
| Some_ a => Some (concrete_data_to_data _ a)
| None_ => None
| Concrete_list l => List.map (concrete_data_to_data _) l
| @Concrete_set a l =>
(fix concrete_data_set_to_data (l : Datatypes.list (concrete_data a)) :=
match l with
| nil => set.empty _ _
| cons x l =>
set.insert
(data a)
(comparable.compare a)
(comparable.compare_eq_iff a)
(comparable.lt_trans a)
(comparable.gt_trans a)
(concrete_data_to_data a x)
(concrete_data_set_to_data l)
end) l
| @Concrete_map a b l =>
(fix concrete_data_map_to_data
(l : Datatypes.list (elt_pair (concrete_data a) (concrete_data b))) :=
match l with
| nil => map.empty _ _ _
| cons (Elt _ _ x y) l =>
map.update
(data a)
(data b)
(comparable.compare a)
(comparable.compare_eq_iff a)
(comparable.lt_trans a)
(comparable.gt_trans a)
(concrete_data_to_data _ x)
(Some (concrete_data_to_data _ y))
(concrete_data_map_to_data l)
end) l
| Instruction i => i
end.
Definition or_fun a (v : bitwise_variant a) : data a -> data a -> data a :=
match v with
| Bitwise_variant_bool => orb
| Bitwise_variant_nat => N.lor
end.
Definition and a (v : bitwise_variant a) : data a -> data a -> data a :=
match v with
| Bitwise_variant_bool => andb
| Bitwise_variant_nat => N.land
end.
Definition xor a (v : bitwise_variant a) : data a -> data a -> data a :=
match v with
| Bitwise_variant_bool => xorb
| Bitwise_variant_nat => N.lxor
end.
Definition not a b (v : not_variant a b) : data a -> data b :=
match v with
| Not_variant_bool => negb
| Not_variant_int => fun x => (- 1 - x)%Z
| Not_variant_nat => fun x => (- 1 - Z.of_N x)%Z
end.
Definition neg a (v : neg_variant a) : data a -> data int :=
match v with
| Neg_variant_nat => fun x => (- Z.of_N x)%Z
| Neg_variant_int => fun x => (- x)%Z
end.
Definition add a b c (v : add_variant a b c) : data a -> data b -> M (data c) :=
match v with
| Add_variant_nat_nat => fun x y => Return _ (x + y)%N
| Add_variant_nat_int => fun x y => Return _ (Z.of_N x + y)%Z
| Add_variant_int_nat => fun x y => Return _ (x + Z.of_N y)%Z
| Add_variant_int_int => fun x y => Return _ (x + y)%Z
| Add_variant_timestamp_int => fun x y => Return _ (x + y)%Z
| Add_variant_int_timestamp => fun x y => Return _ (x + y)%Z
| Add_variant_tez_tez =>
fun x y => tez.of_Z (tez.to_Z x + tez.to_Z y)
end.
Definition sub a b c (v : sub_variant a b c) : data a -> data b -> M (data c) :=
match v with
| Sub_variant_nat_nat => fun x y => Return _ (Z.of_N x - Z.of_N y)%Z
| Sub_variant_nat_int => fun x y => Return _ (Z.of_N x - y)%Z
| Sub_variant_int_nat => fun x y => Return _ (x - Z.of_N y)%Z
| Sub_variant_int_int => fun x y => Return _ (x - y)%Z
| Sub_variant_timestamp_int => fun x y => Return _ (x - y)%Z
| Sub_variant_timestamp_timestamp => fun x y => Return _ (x - y)%Z
| Sub_variant_tez_tez => fun x y => tez.of_Z (tez.to_Z x - tez.to_Z y)
end.
Definition mul a b c (v : mul_variant a b c) : data a -> data b -> M (data c) :=
match v with
| Mul_variant_nat_nat => fun x y => Return _ (x * y)%N
| Mul_variant_nat_int => fun x y => Return _ (Z.of_N x * y)%Z
| Mul_variant_int_nat => fun x y => Return _ (x * Z.of_N y)%Z
| Mul_variant_int_int => fun x y => Return _ (x * y)%Z
| Mul_variant_tez_nat => fun x y => tez.of_Z (tez.to_Z x * Z.of_N y)
| Mul_variant_nat_tez => fun x y => tez.of_Z (Z.of_N x * tez.to_Z y)
end.
Definition ediv_Z x y :=
if (y =? 0)%Z then None else Some (x / y, Z.to_N (x mod y))%Z.
Definition ediv_N x y :=
if (y =? 0)%N then None else Some (x / y, x mod y)%N.
Definition ediv a b c d (v : ediv_variant a b c d) : data a -> data b -> data (option (pair c d)) :=
match v with
| Ediv_variant_nat_nat => fun x y => ediv_N x y
| Ediv_variant_nat_int => fun x y => ediv_Z (Z.of_N x) y
| Ediv_variant_int_nat => fun x y => ediv_Z x (Z.of_N y)
| Ediv_variant_int_int => fun x y => ediv_Z x y
| Ediv_variant_tez_nat =>
fun x y =>
match ediv_Z (tez.to_Z x) (Z.of_N y) with
| None => None
| Some (quo, rem) =>
match tez.of_Z quo, tez.of_Z (Z.of_N rem) with
| Return _ quo, Return _ rem => Some (quo, rem)
| _, _ => None
end
end
| Ediv_variant_tez_tez =>
fun x y =>
match ediv_Z (tez.to_Z x) (tez.to_Z y) with
| None => None
| Some (quo, rem) =>
match tez.of_Z (Z.of_N rem) with
| Return _ rem => Some (Z.to_N quo, rem)
| _ => None
end
end
end.
Definition concat a (v : stringlike_variant a) : data a -> data a -> data a :=
match v with
| Stringlike_variant_string => String.append
| Stringlike_variant_bytes => String.append
end.
Definition slice a (v : stringlike_variant a) : data nat -> data nat -> data a -> data (option a) :=
match v with
| Stringlike_variant_string =>
fun (n1 n2 : N) (s : data string) =>
if (n1 + n2 <=? N.of_nat (String.length s))%N then
(Some (String.substring (N.to_nat n1) (N.to_nat n2) s)
: data (option string))
else None
| Stringlike_variant_bytes =>
fun n1 n2 s =>
if (n1 + n2 <=? N.of_nat (String.length s))%N then
Some (String.substring (N.to_nat n1) (N.to_nat n2) s)
else None
end.
Definition mem a b (v : mem_variant a b) : data a -> data b -> data bool :=
match v with
| Mem_variant_set a =>
fun (x : data a) (y : data (set a)) => set.mem _ _ x y
| Mem_variant_map _ _ => map.mem _ _ _
| Mem_variant_bigmap _ _ => map.mem _ _ _
end.
Definition update a b c (v : update_variant a b c) :
data a -> data b -> data c -> data c :=
match v with
| Update_variant_set a =>
set.update _ _ (compare_eq_iff a) (lt_trans a) (gt_trans a)
| Update_variant_map k v =>
map.update _ _ _ (compare_eq_iff k) (lt_trans k) (gt_trans k)
| Update_variant_bigmap k _ =>
map.update _ _ _ (compare_eq_iff k) (lt_trans k) (gt_trans k)
end.
Definition size a (v : size_variant a) : data a -> Datatypes.nat :=
match v with
| Size_variant_list a => fun l => List.length l
| Size_variant_set a => set.size (data a) (compare a)
| Size_variant_map k v => map.size (data k) (data v) (compare k)
| Size_variant_string => String.length
| Size_variant_bytes => String.length
end.
Definition iter_destruct a b (v : iter_variant a b)
: data b -> data (option (pair a b)) :=
match v with
| Iter_variant_set _ => set.destruct _ _
| Iter_variant_map _ _ => set.destruct _ _
| Iter_variant_list _ =>
fun l => match l with
| nil => None
| cons a l => Some (a, l)
end
end.
Definition get k val c (v : get_variant k val c)
: data k -> data c -> data (option val) :=
match v with
| Get_variant_map _ _ => map.get _ _ _
| Get_variant_bigmap _ _ => map.get _ _ _
end.
Definition map_destruct a b ca cb (v : map_variant a b ca cb)
: data ca -> data (option (pair a ca)) :=
match v with
| Map_variant_map _ _ _ => set.destruct _ _
| Map_variant_list _ _ =>
fun l => match l with
| nil => None
| cons a l => Some (a, l)
end
end.
Definition map_empty a b ca cb (v : map_variant a b ca cb)
: data cb :=
match v with
| Map_variant_map _ _ _ => map.empty _ _ _
| Map_variant_list _ _ => nil
end.
Definition map_insert a b ca cb (v : map_variant a b ca cb)
: data a -> data b -> data cb -> data cb :=
match v with
| Map_variant_map k_ty _ v_ty =>
fun '(k, _) v (m : data (map k_ty v_ty)) =>
map.update _ _ _ (comparable.compare_eq_iff _) (comparable.lt_trans _) (comparable.gt_trans _) k (Some v) m
| Map_variant_list _ _ =>
fun _ => cons
end.
Definition self_address param_tree_opt :=
match param_tree_opt with
| None => Datatypes.unit (* A lambda does not have a self address *)
| Some t => {cst : address_constant | C.get_contract_type cst = Return _ t}
end.
Definition get_entrypoint_in_contract t (self : self_address (Some t)) an ty
(H : (get_entrypoint an t) = Return _ ty) :
data (contract ty).
Proof.
destruct self as (cst, Hself).
simpl.
exists cst.
exists an.
unfold get_contract_type_with_entrypoint.
rewrite Hself.
simpl.
apply Mtype_eq_intro.
assumption.
Defined.
(* The gas argument is used to ensure termination, it is not the
amount of gas that is actually required to run the contract because
in the SEQ case, both instructions are run with gas n *)
Fixpoint eval
param_tree_opt
(self : self_address param_tree_opt)
{A : stack_type} {B : stack_type}
(i : instruction param_tree_opt A B) (fuel : Datatypes.nat) {struct fuel} :
stack A -> M (stack B) :=
match fuel with
| O => fun SA => Failed _ Out_of_fuel
| S n =>
match i in instruction param_tree_opt A B return
self_address param_tree_opt ->
stack A -> M (stack B) with
| @FAILWITH _ A B a =>
fun _ '(x, _) => Failed _ (Assertion_Failure (data a) x)
(* According to the documentation, FAILWITH's argument should
not be part of the state reached by the instruction but the
whole point of this instruction (compared to the FAIL macro)
is to report the argument to the user. *)
| NOOP => fun _ SA => Return _ SA
| SEQ B C =>
fun self SA => bind (eval _ self C n) (eval _ self B n SA)
| IF_ bt bf =>
fun self '(b, SA) => if b then eval _ self bt n SA else eval _ self bf n SA
| LOOP body =>
fun self '(b, SA) => if b then eval _ self (body;; (LOOP body)) n SA else Return _ SA
| LOOP_LEFT body =>
fun self '(ab, SA) =>
match ab return M (stack (_ ::: _)) with
| inl x => eval _ self (body;; LOOP_LEFT body) n (x, SA)
| inr y => Return _ (y, SA)
end
| DIP i =>
fun self '(y, SA) => bind (fun SC => Return _ (y, SC)) (eval _ self i n SA)
| EXEC =>
fun self '(x, (f, SA)) =>
bind (fun '(y, tt) => Return _ (y, SA)) (eval None tt f n (x, tt))
| DROP => fun _ '(_, SA) => Return _ SA
| DUP => fun _ '(x, SA) => Return _ (x, (x, SA))
| SWAP => fun _ '(x, (y, SA)) => Return _ (y, (x, SA))
| PUSH a x => fun _ SA => Return _ (concrete_data_to_data _ x, SA)
| UNIT => fun _ SA => Return _ (tt, SA)
| LAMBDA a b code => fun _ SA => Return _ (code, SA)
| EQ => fun _ '(x, SA) => Return _ ((x =? 0)%Z, SA)
| NEQ => fun _ '(x, SA) => Return _ (negb (x =? 0)%Z, SA)
| LT => fun _ '(x, SA) => Return _ ((x <? 0)%Z, SA)
| GT => fun _ '(x, SA) => Return _ ((x >? 0)%Z, SA)
| LE => fun _ '(x, SA) => Return _ ((x <=? 0)%Z, SA)
| GE => fun _ '(x, SA) => Return _ ((x >=? 0)%Z, SA)
| @OR _ _ s =>
fun _ '(x, (y, SA)) => Return _ (or_fun _ (bitwise_variant_field _ s) x y, SA)
| @AND _ _ s =>
fun _ '(x, (y, SA)) => Return _ (and _ (bitwise_variant_field _ s) x y, SA)
| @XOR _ _ s =>
fun _ '(x, (y, SA)) => Return _ (xor _ (bitwise_variant_field _ s) x y, SA)
| @NOT _ _ s =>
fun _ '(x, SA) => Return _ (not _ _ (not_variant_field _ s) x, SA)
| @NEG _ _ s =>
fun _ '(x, SA) => Return _ (neg _ (neg_variant_field _ s) x, SA)
| ABS => fun _ '(x, SA) => Return _ (Z.abs_N x, SA)
| @ADD _ _ _ s =>
fun _ '(x, (y, SA)) =>
bind (fun r => Return _ (r, SA))
(add _ _ _ (add_variant_field _ _ s) x y)
| @SUB _ _ _ s =>
fun _ '(x, (y, SA)) =>
bind (fun r => Return _ (r, SA))
(sub _ _ _ (sub_variant_field _ _ s) x y)
| @MUL _ _ _ s =>
fun _ '(x, (y, SA)) =>
bind (fun r => Return _ (r, SA))
(mul _ _ _ (mul_variant_field _ _ s) x y)
| @EDIV _ _ _ s =>
fun _ '(x, (y, SA)) =>
Return _ (ediv _ _ _ _ (ediv_variant_field _ _ s) x y, SA)
| LSL => fun _ '(x, (y, SA)) => Return _ (N.shiftl x y, SA)
| LSR => fun _ '(x, (y, SA)) => Return _ (N.shiftr x y, SA)
| COMPARE =>
fun _ '(x, (y, SA)) => Return _ (comparison_to_int (compare _ x y), SA)
| @CONCAT _ _ s =>
fun _ '(x, (y, SA)) =>
Return _ (concat _ (stringlike_variant_field _ s) x y, SA)
| @SLICE _ _ i =>
fun _ '(n1, (n2, (s, SA))) =>
Return _ (slice _ (stringlike_variant_field _ i) n1 n2 s, SA)
| PAIR => fun _ '(x, (y, SA)) => Return _ ((x, y), SA)
| CAR => fun _ '((x, y), SA) => Return _ (x, SA)
| CDR => fun _ '((x, y), SA) => Return _ (y, SA)
| EMPTY_SET a => fun _ SA => Return _ (set.empty _ (compare a), SA)
| @MEM _ _ _ s =>
fun _ '(x, (y, SA)) =>
Return _ (mem _ _ (mem_variant_field _ _ s) x y, SA)
| @UPDATE _ _ _ _ s =>
fun _ '(x, (y, (z, SA))) =>
Return _ (update _ _ _ (update_variant_field _ _ _ s) x y z, SA)
| @ITER _ _ s _ body =>
fun self '(x, SA) =>
match iter_destruct _ _ (iter_variant_field _ s) x with
| None => Return _ SA
| Some (a, y) =>
bind (fun SB =>
eval _ self (ITER body) n (y, SB))
(eval _ self body n (a, SA))
end
| @SIZE _ _ s =>
fun _ '(x, SA) => Return _ (N.of_nat (size _ (size_variant_field _ s) x), SA)
| EMPTY_MAP k val =>
fun _ SA => Return _ (map.empty (comparable_data k) (data val) _, SA)
| @GET _ _ _ s =>
fun _ '(x, (y, SA)) =>
Return _ (get _ _ _ (get_variant_field _ _ s) x y, SA)
| @MAP _ _ _ s _ body =>
let v := (map_variant_field _ _ s) in
fun self '(x, SA) =>
match map_destruct _ _ _ _ v x with
| None => Return _ (map_empty _ _ _ _ v, SA)
| Some (a, y) =>
bind (fun '(b, SB) =>
bind (fun '(c, SC) =>
Return _ (map_insert _ _ _ _ v a b c,
SC))
(eval _ self (MAP body) n (y, SB)))
(eval _ self body n (a, SA))
end
| SOME => fun _ '(x, SA) => Return _ (Some x, SA)
| NONE _ => fun _ SA => Return _ (None, SA)
| IF_NONE bt bf =>
fun self '(b, SA) =>
match b with
| None => eval _ self bt n SA
| Some b => eval _ self bf n (b, SA)
end
| LEFT _ => fun _ '(x, SA) => Return _ (inl x, SA)
| RIGHT _ => fun _ '(x, SA) => Return _ (inr x, SA)
| IF_LEFT bt bf =>
fun self '(b, SA) =>
match b with
| inl a => eval _ self bt n (a, SA)
| inr b => eval _ self bf n (b, SA)
end
| IF_RIGHT bt bf =>
fun self '(b, SA) =>
match b with
| inl a => eval _ self bf n (a, SA)
| inr b => eval _ self bt n (b, SA)
end
| CONS => fun _ '(x, (y, SA)) => Return _ (cons x y, SA)
| NIL _ => fun _ SA => Return _ (nil, SA)
| IF_CONS bt bf =>
fun self '(l, SA) =>
match l with
| cons a b => eval _ self bt n (a, (b, SA))
| nil => eval _ self bf n SA
end
| CREATE_CONTRACT_literal _ _ f =>
fun _ '(a, (b, (c, (d, (e, (g, SA)))))) =>
let (oper, addr) := create_contract env _ _ a b c d e f g in
Return _ (oper, (addr, SA))
| CREATE_ACCOUNT =>
fun _ '(a, (b, (c, (d, SA)))) =>
let (oper, contract) := create_account env a b c d in
Return _ (oper, (contract, SA))
| TRANSFER_TOKENS =>
fun _ '(a, (b, (c, SA))) => Return _ (transfer_tokens env _ a b c, SA)
| SET_DELEGATE => fun _ '(x, SA) => Return _ (set_delegate env x, SA)
| BALANCE => fun _ SA => Return _ (balance env, SA)
| ADDRESS =>
fun _ '(x, SA) => Return _ (address_ env _ x, SA)
| CONTRACT p an =>
fun self '(x, SA) => Return _ (contract_ env p an x, SA)
| SOURCE => fun _ SA => Return _ (source env, SA)
| SENDER => fun _ SA => Return _ (sender env, SA)
| SELF an t H =>
fun self SA =>
Return _ (get_entrypoint_in_contract _ self an t H, SA)
| AMOUNT => fun _ SA => Return _ (amount env, SA)
| IMPLICIT_ACCOUNT =>
fun _ '(x, SA) => Return _ (implicit_account env x, SA)
| STEPS_TO_QUOTA =>
fun _ SA => Return _ (steps_to_quota env, SA)
| NOW => fun _ SA => Return _ (now env, SA)
| PACK => fun _ '(x, SA) => Return _ (pack env _ x, SA)
| UNPACK => fun _ '(x, SA) => Return _ (unpack env _ x, SA)
| HASH_KEY => fun _ '(x, SA) => Return _ (hash_key env x, SA)
| BLAKE2B => fun _ '(x, SA) => Return _ (blake2b env x, SA)
| SHA256 => fun _ '(x, SA) => Return _ (sha256 env x, SA)
| SHA512 => fun _ '(x, SA) => Return _ (sha512 env x, SA)
| CHECK_SIGNATURE =>
fun _ '(x, (y, (z, SA))) =>
Return _ (check_signature env x y z, SA)
end self
end.
(* The evaluator does not depend on the amount of fuel provided *)
Lemma eval_deterministic_le :
forall fuel1 fuel2,
fuel1 <= fuel2 ->
forall {self_address self} {A B} (i : instruction self_address A B) st,
success (eval self_address self i fuel1 st) ->
eval self_address self i fuel1 st = eval self_address self i fuel2 st.
Proof.
induction fuel1; intros fuel2 Hle self_address self A B i st Hsucc.
- apply not_false in Hsucc.
contradiction.
- destruct fuel2.
+ inversion Hle.
+ apply le_S_n in Hle.
specialize (IHfuel1 fuel2 Hle).
simpl.
destruct i; try reflexivity.
* simpl in Hsucc.
destruct (success_bind _ _ Hsucc) as (x, (H1, H2)).
rewrite <- IHfuel1.
-- rewrite H1.
simpl.
apply IHfuel1.
assumption.
-- apply success_eq_return in H1.
exact H1.
* destruct st as ([], st); rewrite IHfuel1; try assumption; reflexivity.
* destruct st as ([], st).
-- rewrite IHfuel1; try assumption; reflexivity.
-- reflexivity.
* destruct st as ([x|y], st).
-- rewrite IHfuel1; try assumption; reflexivity.
-- reflexivity.
* destruct st; rewrite IHfuel1.
-- reflexivity.
-- simpl in Hsucc.
destruct (success_bind _ _ Hsucc) as (x, (H1, H2)).
apply success_eq_return in H1.
exact H1.
* destruct st as (x, (f, SA)).
f_equal.
rewrite IHfuel1.
-- reflexivity.
-- simpl in Hsucc.
apply success_bind_arg in Hsucc.
assumption.
* destruct st as (x, SA).
generalize Hsucc; clear Hsucc.
simpl.
destruct (iter_destruct (iter_elt_type collection i) collection
(iter_variant_field collection i) x).
-- destruct d.
fold stack.
intro Hsucc.
rewrite <- IHfuel1.
++ destruct (success_bind _ _ Hsucc) as (SB, (Ha, Hb)).
rewrite Ha.
simpl.
apply IHfuel1.
assumption.
++ apply success_bind_arg in Hsucc.
assumption.
-- reflexivity.
* destruct st as (x, SA).
generalize Hsucc; clear Hsucc.
simpl.
fold stack.
destruct (map_destruct (map_in_type collection b i)
b
collection
(map_out_collection_type collection b i)
(map_variant_field collection b i) x).
-- destruct d.
intro Hsucc.
rewrite <- IHfuel1.
++ destruct (success_bind _ _ Hsucc) as ((c, SC), (Ha, Hb)).
destruct (success_bind _ _ Hb) as ((dd, SD), (Hm, _)).
rewrite Ha.
simpl.
rewrite <- IHfuel1.
** reflexivity.
** rewrite Hm.
constructor.
++ apply success_bind_arg in Hsucc.
assumption.
-- reflexivity.
* destruct st as ([|], SA); rewrite IHfuel1.
-- reflexivity.
-- exact Hsucc.
-- reflexivity.
-- exact Hsucc.
* destruct st as ([|], SA); rewrite IHfuel1.
-- reflexivity.
-- exact Hsucc.
-- reflexivity.
-- exact Hsucc.
* destruct st as ([|], SA); rewrite IHfuel1.
-- reflexivity.
-- exact Hsucc.
-- reflexivity.
-- exact Hsucc.
* destruct st as ([|], SA); rewrite IHfuel1.
-- reflexivity.
-- exact Hsucc.
-- reflexivity.
-- exact Hsucc.
Qed.
Lemma eval_deterministic_success_both {self_address self} fuel1 fuel2 {A B} (i : instruction self_address A B) S :
success (eval self_address self i fuel1 S) ->
success (eval self_address self i fuel2 S) ->
eval self_address self i fuel1 S = eval self_address self i fuel2 S.
Proof.
case (le_ge_dec fuel1 fuel2).
- intros Hle Hsucc _.
apply eval_deterministic_le; assumption.
- unfold ge.
intros Hle _ Hsucc.
symmetry.
apply eval_deterministic_le; assumption.
Qed.
Definition eval_precond_body
(eval_precond_n : forall {param_ty}
(self : self_address param_ty),
forall {A B}, instruction param_ty A B ->
(stack B -> Prop) -> stack A -> Prop)
{param_ty self} A B
(i : instruction param_ty A B) :
(stack B -> Prop) -> (stack A -> Prop) :=
match i in instruction param_ty A B return
self_address param_ty ->
(stack B -> Prop) -> (stack A -> Prop) with
| FAILWITH => fun _ _ _ => false
| NOOP => fun self psi st => psi st
| SEQ B C => fun self psi =>
eval_precond_n self B (eval_precond_n self C psi)
| IF_ bt bf =>
fun self psi '(b, SA) => if b then eval_precond_n self bt psi SA
else eval_precond_n self bf psi SA
| LOOP body =>
fun self psi '(b, SA) => if b then eval_precond_n self (body;; (LOOP body)) psi SA
else psi SA
| LOOP_LEFT body =>
fun self psi '(ab, SA) =>
match ab with
| inl x => eval_precond_n self (body;; LOOP_LEFT body) psi (x, SA)
| inr y => psi (y, SA)
end
| DIP i =>
fun self psi '(y, SA) => eval_precond_n self i (fun SB => psi (y, SB)) SA
| @EXEC st _ _ =>
fun self psi '(x, (f, SA)) =>
@eval_precond_n None tt _ _ f (fun '(y, tt) => psi (y, SA)) (x, tt)
| DROP => fun self psi '(_, SA) => psi SA
| DUP => fun self psi '(x, SA) => psi (x, (x, SA))
| SWAP => fun self psi '(x, (y, SA)) => psi (y, (x, SA))
| PUSH a x => fun self psi SA => psi (concrete_data_to_data _ x, SA)
| UNIT => fun self psi SA => psi (tt, SA)
| LAMBDA a b code => fun self psi SA => psi (code, SA)
| EQ => fun self psi '(x, SA) => psi ((x =? 0)%Z, SA)
| NEQ => fun self psi '(x, SA) => psi (negb (x =? 0)%Z, SA)
| LT => fun self psi '(x, SA) => psi ((x <? 0)%Z, SA)
| GT => fun self psi '(x, SA) => psi ((x >? 0)%Z, SA)
| LE => fun self psi '(x, SA) => psi ((x <=? 0)%Z, SA)
| GE => fun self psi '(x, SA) => psi ((x >=? 0)%Z, SA)
| @OR _ _ s =>
fun self psi '(x, (y, SA)) => psi (or_fun _ (bitwise_variant_field _ s) x y, SA)
| @AND _ _ s =>
fun self psi '(x, (y, SA)) => psi (and _ (bitwise_variant_field _ s) x y, SA)
| @XOR _ _ s =>
fun self psi '(x, (y, SA)) => psi (xor _ (bitwise_variant_field _ s) x y, SA)
| @NOT _ _ s =>
fun self psi '(x, SA) => psi (not _ _ (not_variant_field _ s) x, SA)
| @NEG _ _ s =>
fun self psi '(x, SA) => psi (neg _ (neg_variant_field _ s) x, SA)
| ABS => fun self psi '(x, SA) => psi (Z.abs_N x, SA)
| @ADD _ _ _ s =>
fun self psi '(x, (y, SA)) =>
precond (add _ _ _ (add_variant_field _ _ s) x y) (fun z => psi (z, SA))
| @SUB _ _ _ s =>
fun self psi '(x, (y, SA)) =>
precond (sub _ _ _ (sub_variant_field _ _ s) x y) (fun z => psi (z, SA))
| @MUL _ _ _ s =>
fun self psi '(x, (y, SA)) =>
precond (mul _ _ _ (mul_variant_field _ _ s) x y) (fun z => psi (z, SA))
| @EDIV _ _ _ s =>
fun self psi '(x, (y, SA)) =>
psi (ediv _ _ _ _ (ediv_variant_field _ _ s) x y, SA)
| LSL => fun self psi '(x, (y, SA)) => psi (N.shiftl x y, SA)
| LSR => fun self psi '(x, (y, SA)) => psi (N.shiftr x y, SA)
| COMPARE =>
fun self psi '(x, (y, SA)) => psi (comparison_to_int (compare _ x y), SA)
| @CONCAT _ _ s =>
fun self psi '(x, (y, SA)) =>
psi (concat _ (stringlike_variant_field _ s) x y, SA)
| @SLICE _ _ i =>
fun self psi '(n1, (n2, (s, SA))) =>
psi (slice _ (stringlike_variant_field _ i) n1 n2 s, SA)
| PAIR => fun self psi '(x, (y, SA)) => psi ((x, y), SA)
| CAR => fun self psi '((x, y), SA) => psi (x, SA)
| CDR => fun self psi '((x, y), SA) => psi (y, SA)
| EMPTY_SET a => fun self psi SA => psi (set.empty _ (compare a), SA)
| @MEM _ _ _ s =>
fun self psi '(x, (y, SA)) =>
psi (mem _ _ (mem_variant_field _ _ s) x y, SA)
| @UPDATE _ _ _ _ s =>
fun self psi '(x, (y, (z, SA))) =>
psi (update _ _ _ (update_variant_field _ _ _ s) x y z, SA)
| @ITER _ _ s _ body =>
fun self psi '(x, SA) =>
match iter_destruct _ _ (iter_variant_field _ s) x with
| None => psi SA
| Some (a, y) =>
eval_precond_n self body
(fun SB => eval_precond_n self (ITER body) psi (y, SB))
(a, SA)
end
| @SIZE _ _ s =>
fun self psi '(x, SA) => psi (N.of_nat (size _ (size_variant_field _ s) x), SA)
| EMPTY_MAP k val =>
fun self psi SA => psi (map.empty (comparable_data k) (data val) _, SA)
| @GET _ _ _ s =>
fun self psi '(x, (y, SA)) => psi (get _ _ _ (get_variant_field _ _ s) x y, SA)
| @MAP _ _ _ s _ body =>
let v := (map_variant_field _ _ s) in
fun self psi '(x, SA) =>
match map_destruct _ _ _ _ v x with
| None => psi (map_empty _ _ _ _ v, SA)
| Some (a, y) =>
eval_precond_n self body
(fun '(b, SB) =>
eval_precond_n self (MAP body)
(fun '(c, SC) => psi (map_insert _ _ _ _ v a b c, SC))
(y, SB))
(a, SA)
end
| SOME => fun self psi '(x, SA) => psi (Some x, SA)
| NONE _ => fun self psi SA => psi (None, SA)
| IF_NONE bt bf =>
fun self psi '(b, SA) =>
match b with
| None => eval_precond_n self bt psi SA
| Some b => eval_precond_n self bf psi (b, SA)
end
| LEFT _ => fun self psi '(x, SA) => psi (inl x, SA)
| RIGHT _ => fun self psi '(x, SA) => psi (inr x, SA)
| IF_LEFT bt bf =>
fun self psi '(b, SA) =>
match b with
| inl a => eval_precond_n self bt psi (a, SA)
| inr b => eval_precond_n self bf psi (b, SA)
end
| IF_RIGHT bt bf =>
fun self psi '(b, SA) =>
match b with
| inl a => eval_precond_n self bf psi (a, SA)
| inr b => eval_precond_n self bt psi (b, SA)
end
| CONS => fun self psi '(x, (y, SA)) => psi (cons x y, SA)
| NIL _ => fun self psi SA => psi (nil, SA)
| IF_CONS bt bf =>
fun self psi '(l, SA) =>
match l with
| cons a b => eval_precond_n self bt psi (a, (b, SA))
| nil => eval_precond_n self bf psi SA
end
| CREATE_CONTRACT_literal _ _ f =>
fun self psi '(a, (b, (c, (d, (e, (g, SA)))))) =>
let (oper, addr) := create_contract env _ _ a b c d e f g in
psi (oper, (addr, SA))
| CREATE_ACCOUNT =>
fun self psi '(a, (b, (c, (d, SA)))) =>
let (oper, contr) := create_account env a b c d in
psi (oper, (contr, SA))
| TRANSFER_TOKENS =>
fun self psi '(a, (b, (c, SA))) =>
psi (transfer_tokens env _ a b c, SA)
| SET_DELEGATE =>
fun self psi '(x, SA) =>
psi (set_delegate env x, SA)
| BALANCE =>
fun self psi SA => psi (balance env, SA)
| ADDRESS =>
fun self psi '(x, SA) => psi (address_ env _ x, SA)
| CONTRACT p an =>
fun self psi '(x, SA) => psi (contract_ env p an x, SA)
| SOURCE => fun self psi SA => psi (source env, SA)
| SENDER => fun self psi SA => psi (sender env, SA)
| SELF an t H => fun self psi SA => psi (get_entrypoint_in_contract _ self an t H, SA)
| AMOUNT => fun self psi SA => psi (amount env, SA)
| IMPLICIT_ACCOUNT =>
fun self psi '(x, SA) => psi (implicit_account env x, SA)
| STEPS_TO_QUOTA =>
fun self psi SA => psi (steps_to_quota env, SA)
| NOW => fun self psi SA => psi (now env, SA)
| PACK => fun self psi '(x, SA) => psi (pack env _ x, SA)
| UNPACK =>
fun self psi '(x, SA) => psi (unpack env _ x, SA)
| HASH_KEY =>
fun self psi '(x, SA) => psi (hash_key env x, SA)
| BLAKE2B =>
fun self psi '(x, SA) => psi (blake2b env x, SA)
| SHA256 => fun self psi '(x, SA) => psi (sha256 env x, SA)
| SHA512 => fun self psi '(x, SA) => psi (sha512 env x, SA)
| CHECK_SIGNATURE =>
fun self psi '(x, (y, (z, SA))) =>
psi (check_signature env x y z, SA)
end self.
Fixpoint eval_precond (fuel : Datatypes.nat) :
forall {param_ty} self {A B},
instruction param_ty A B ->
(stack B -> Prop) -> (stack A -> Prop) :=
match fuel with
| O => fun _ _ _ _ _ _ _ => false
| S n =>
@eval_precond_body (@eval_precond n)
end.
Lemma eval_precond_correct {sty self A B} (i : instruction sty A B) n st psi :
precond (eval _ self i n st) psi <-> eval_precond n self i psi st.
Proof.
generalize sty self A B i st psi; clear sty self A B i st psi.
induction n; intros sty self A B i st psi; [simpl; intuition|].
destruct i; simpl; fold data stack.
- reflexivity.
- destruct st; reflexivity.
- rewrite precond_bind.
rewrite <- IHn.
apply precond_eqv.
intro SB.
apply IHn.
- destruct st as ([|], st); auto.
- destruct st as ([|], st).
+ apply IHn.
+ simpl. reflexivity.
- destruct st as ([|], st); simpl.
+ apply (IHn _ _ _ _ (i;; LOOP_LEFT i)).
+ reflexivity.
- destruct st as (y, st).
rewrite precond_bind.
apply IHn.
- destruct st as (x, (f, st)).
rewrite precond_bind.
rewrite <- (IHn None tt _ _ f (x, tt) (fun '(y, tt) => psi (y, st))).
apply precond_eqv.
intros (y, []).
simpl.
reflexivity.
- destruct st; reflexivity.
- destruct st; reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
- destruct st; reflexivity.
- destruct st; reflexivity.
- destruct st; reflexivity.
- destruct st; reflexivity.
- destruct st; reflexivity.
- destruct st; reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st; reflexivity.
- destruct st; reflexivity.
- destruct st; reflexivity.
- destruct st as (x, (y, st)); rewrite precond_bind; reflexivity.
- destruct st as (x, (y, st)); rewrite precond_bind; reflexivity.
- destruct st as (x, (y, st)); rewrite precond_bind; reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st; reflexivity.
- destruct st as (x, (y, (z, st))); reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st as ((x, y), st); reflexivity.
- destruct st as ((x, y), st); reflexivity.
- reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st as (x, (y, (z, st))); reflexivity.
- destruct st as (x, st).
destruct (iter_destruct (iter_elt_type collection i) collection
(iter_variant_field collection i) x) as [(hd, tl)|].
+ rewrite precond_bind.
rewrite <- IHn.
apply precond_eqv.
intro SA.
apply IHn.
+ reflexivity.
- reflexivity.
- destruct st as (x, (y, st)); reflexivity.
- destruct st as (x, st).
destruct (map_destruct (map_in_type collection b i) b collection
(map_out_collection_type collection b i)
(map_variant_field collection b i) x) as [(hd, tl)|].
+ rewrite precond_bind.
rewrite <- IHn.
apply precond_eqv.
intros (bb, SA).
rewrite precond_bind.
rewrite <- IHn.
apply precond_eqv.
intros (c, B).
reflexivity.
+ reflexivity.
- destruct st; reflexivity.
- reflexivity.
- destruct st as ([|], st); apply IHn.
- destruct st; reflexivity.
- destruct st; reflexivity.
- destruct st as ([|], st); apply IHn.
- destruct st as ([|], st); apply IHn.
- destruct st as (x, (y, st)); reflexivity.
- reflexivity.
- destruct st as ([|], st); apply IHn.
- destruct st as (a, (b, (c, (d, (e, (g0, SA)))))).
destruct (create_contract env g p a b c d e i g0).
reflexivity.
- destruct st as (a, (b, (c, (d, SA)))).
destruct (create_account env a b c).
reflexivity.
- destruct st as (a, (b, (c, SA))).
reflexivity.
- destruct st as (a, SA).
reflexivity.
- reflexivity.
- destruct st as (a, SA).
reflexivity.
- destruct st as (addr, SA).
reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
- destruct st as (a, SA).
reflexivity.
- reflexivity.
- reflexivity.
- destruct st as (x, SA).
reflexivity.
- destruct st as (x, SA).
reflexivity.
- destruct st as (x, SA).
reflexivity.
- destruct st as (x, SA).
reflexivity.
- destruct st as (x, SA).
reflexivity.
- destruct st as (x, SA).
reflexivity.
- destruct st as (a, (b, (c, SA))).
reflexivity.
Qed.
Lemma fold_eval_precond fuel :
@eval_precond_body (@eval_precond fuel) =
@eval_precond (S fuel).
Proof.
reflexivity.
Qed.
Ltac simplify_instruction :=
match goal with
|- ?g =>
match g with
| context c[eval_precond (S ?n) ?i ?psi] =>
is_var i ||
(let simplified := (eval simpl in (eval_precond (S n) i psi)) in
let full := context c[simplified] in
let final := eval cbv beta zeta iota in full in
change final)
end
end.
(* essentially the same as simplify_instruction but reduces only one step *)
Ltac simplify_instruction_light :=
match goal with
| |- context c[eval_precond (S ?n) ?i ?psi] =>
is_var i ||
( let rem_fuel := fresh "fuel" in
remember n as rem_fuel;
let simplified := (eval simpl in (eval_precond (S rem_fuel) i psi)) in
change (eval_precond (S rem_fuel) i psi) with simplified;
subst rem_fuel)
end.
End Semantics.
