https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 59419d479a164559c73ceed92ab2785f2ef55107 authored by Raphaël Cauderlier on 03 October 2019, 14:10:15 UTC
Remove unused module dependencies
Remove unused module dependencies
Tip revision: 59419d4
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 Import comparable error.
Module EnvDef(C:ContractContext).
Export C.
Module macros := Macros(C). Export macros.
Fixpoint data (a : type) {struct a} : Set :=
match a with
| Comparable_type b => comparable_data b
| signature => signature_constant
| operation => operation_constant
| key => key_constant
| unit => Datatypes.unit
| 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 : contract_constant | get_contract_type s = Return _ a }
end.
Definition self_data (self_ty : Datatypes.option type) : Set :=
match self_ty with
| Some self_ty => data (contract self_ty)
| None => Datatypes.unit
end.
Record proto_env {self_ty : Datatypes.option type} : 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 ->
syntax.instruction (Some p)
(pair 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, data address -> data (option (contract p));
source : data address;
sender : data address;
self : self_data self_ty;
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 SelfType.
Parameter self_type : Datatypes.option type.
End SelfType.
Module Type Env(ST : SelfType)(C:ContractContext).
Include EnvDef C.
Parameter env:(@proto_env ST.self_type).
End Env.
Module Semantics(ST : SelfType)(C:ContractContext)(E:Env ST C).
Export E.
Definition no_self_data : self_data None := tt.
Definition no_self {param_ty} (env : @proto_env param_ty) : @proto_env None :=
{|
create_contract := create_contract env;
create_account := create_account env;
transfer_tokens := transfer_tokens env;
set_delegate := set_delegate env;
balance := balance env;
address_ := address_ env;
contract_ := contract_ env;
source := source env;
sender := sender env;
self := no_self_data;
amount := amount env;
implicit_account := implicit_account env;
steps_to_quota := steps_to_quota env;
now := now env;
hash_key := hash_key env;
pack := pack env;
unpack := unpack env;
blake2b := blake2b env;
sha256 := sha256 env;
sha512 := sha512 env;
check_signature := check_signature env;
|}.
Fixpoint stack (t : stack_type) : Set :=
match t with
| nil => Datatypes.unit
| cons a A => data a * stack A
end.
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 a x H => exist _ x 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.
(* 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_ty : Datatypes.option type} (env : @proto_env param_ty) {A : stack_type} {B : stack_type}
(i : instruction param_ty 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_ty A B return @proto_env param_ty -> 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 env SA => bind (eval env C n) (eval env B n SA)
| IF_ bt bf =>
fun env '(b, SA) => if b then eval env bt n SA else eval env bf n SA
| LOOP body =>
fun env '(b, SA) => if b then eval env (body;; (LOOP body)) n SA else Return _ SA
| LOOP_LEFT body =>
fun env '(ab, SA) =>
match ab return M (stack (_ ::: _)) with
| inl x => eval env (body;; LOOP_LEFT body) n (x, SA)
| inr y => Return _ (y, SA)
end
| DIP i =>
fun env '(y, SA) => bind (fun SC => Return _ (y, SC)) (eval env i n SA)
| EXEC =>
fun env '(x, (f, SA)) =>
bind (fun '(y, tt) => Return _ (y, SA)) (eval (no_self env) f n (x, tt))
| DROP => fun env '(_, SA) => Return _ SA
| DUP => fun env '(x, SA) => Return _ (x, (x, SA))
| SWAP => fun env '(x, (y, SA)) => Return _ (y, (x, SA))
| PUSH a x => fun env SA => Return _ (concrete_data_to_data _ x, SA)
| UNIT => fun env SA => Return _ (tt, SA)
| LAMBDA a b code => fun env SA => Return _ (code, SA)
| EQ => fun env '(x, SA) => Return _ ((x =? 0)%Z, SA)
| NEQ => fun env '(x, SA) => Return _ (negb (x =? 0)%Z, SA)
| LT => fun env '(x, SA) => Return _ ((x <? 0)%Z, SA)
| GT => fun env '(x, SA) => Return _ ((x >? 0)%Z, SA)
| LE => fun env '(x, SA) => Return _ ((x <=? 0)%Z, SA)
| GE => fun env '(x, SA) => Return _ ((x >=? 0)%Z, SA)
| @OR _ _ s =>
fun env '(x, (y, SA)) => Return _ (or_fun _ (bitwise_variant_field _ s) x y, SA)
| @AND _ _ s =>
fun env '(x, (y, SA)) => Return _ (and _ (bitwise_variant_field _ s) x y, SA)
| @XOR _ _ s =>
fun env '(x, (y, SA)) => Return _ (xor _ (bitwise_variant_field _ s) x y, SA)
| @NOT _ _ s =>
fun env '(x, SA) => Return _ (not _ _ (not_variant_field _ s) x, SA)
| @NEG _ _ s =>
fun env '(x, SA) => Return _ (neg _ (neg_variant_field _ s) x, SA)
| ABS => fun env '(x, SA) => Return _ (Z.abs_N x, SA)
| ISNAT => fun env '(x, SA) => Return _ (if (x >=? 0)%Z then (Some (Z.to_N x), SA) else (None, SA))
| INT => fun env '(x, SA) => Return _ (Z.of_N x, SA)
| @ADD _ _ _ s =>
fun env '(x, (y, SA)) =>
bind (fun r => Return _ (r, SA))
(add _ _ _ (add_variant_field _ _ s) x y)
| @SUB _ _ _ s =>
fun env '(x, (y, SA)) =>
bind (fun r => Return _ (r, SA))
(sub _ _ _ (sub_variant_field _ _ s) x y)
| @MUL _ _ _ s =>
fun env '(x, (y, SA)) =>
bind (fun r => Return _ (r, SA))
(mul _ _ _ (mul_variant_field _ _ s) x y)
| @EDIV _ _ _ s =>
fun env '(x, (y, SA)) =>
Return _ (ediv _ _ _ _ (ediv_variant_field _ _ s) x y, SA)
| LSL => fun env '(x, (y, SA)) => Return _ (N.shiftl x y, SA)
| LSR => fun env '(x, (y, SA)) => Return _ (N.shiftr x y, SA)
| COMPARE =>
fun env '(x, (y, SA)) => Return _ (comparison_to_int (compare _ x y), SA)
| @CONCAT _ _ s =>
fun env '(x, (y, SA)) =>
Return _ (concat _ (stringlike_variant_field _ s) x y, SA)
| @SLICE _ _ i =>
fun env '(n1, (n2, (s, SA))) =>
Return _ (slice _ (stringlike_variant_field _ i) n1 n2 s, SA)
| PAIR => fun env '(x, (y, SA)) => Return _ ((x, y), SA)
| CAR => fun env '((x, y), SA) => Return _ (x, SA)
| CDR => fun env '((x, y), SA) => Return _ (y, SA)
| EMPTY_SET a => fun env SA => Return _ (set.empty _ (compare a), SA)
| @MEM _ _ _ s =>
fun env '(x, (y, SA)) =>
Return _ (mem _ _ (mem_variant_field _ _ s) x y, SA)
| @UPDATE _ _ _ _ s =>
fun env '(x, (y, (z, SA))) =>
Return _ (update _ _ _ (update_variant_field _ _ _ s) x y z, SA)
| @ITER _ _ s _ body =>
fun env '(x, SA) =>
match iter_destruct _ _ (iter_variant_field _ s) x with
| None => Return _ SA
| Some (a, y) =>
bind (fun SB =>
eval env (ITER body) n (y, SB))
(eval env body n (a, SA))
end
| @SIZE _ _ s =>
fun env '(x, SA) => Return _ (N.of_nat (size _ (size_variant_field _ s) x), SA)
| EMPTY_MAP k val =>
fun env SA => Return _ (map.empty (comparable_data k) (data val) _, SA)
| @GET _ _ _ s =>
fun env '(x, (y, SA)) =>
Return _ (get _ _ _ (get_variant_field _ _ s) x y, SA)
| @MAP _ _ _ s _ body =>
let v := (map_variant_field _ _ s) in
fun env '(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 env (MAP body) n (y, SB)))
(eval env body n (a, SA))
end
| SOME => fun env '(x, SA) => Return _ (Some x, SA)
| NONE _ => fun env SA => Return _ (None, SA)
| IF_NONE bt bf =>
fun env '(b, SA) =>
match b with
| None => eval env bt n SA
| Some b => eval env bf n (b, SA)
end
| LEFT _ => fun env '(x, SA) => Return _ (inl x, SA)
| RIGHT _ => fun env '(x, SA) => Return _ (inr x, SA)
| IF_LEFT bt bf =>
fun env '(b, SA) =>
match b with
| inl a => eval env bt n (a, SA)
| inr b => eval env bf n (b, SA)
end
| IF_RIGHT bt bf =>
fun env '(b, SA) =>
match b with
| inl a => eval env bf n (a, SA)
| inr b => eval env bt n (b, SA)
end
| CONS => fun env '(x, (y, SA)) => Return _ (cons x y, SA)
| NIL _ => fun env SA => Return _ (nil, SA)
| IF_CONS bt bf =>
fun env '(l, SA) =>
match l with
| cons a b => eval env bt n (a, (b, SA))
| nil => eval env bf n SA
end
| CREATE_CONTRACT_literal _ _ f =>
fun env '(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 env '(a, (b, (c, (d, SA)))) =>
let (oper, contract) := create_account env a b c d in
Return _ (oper, (contract, SA))
| TRANSFER_TOKENS =>
fun env '(a, (b, (c, SA))) => Return _ (transfer_tokens env _ a b c, SA)
| SET_DELEGATE => fun env '(x, SA) => Return _ (set_delegate env x, SA)
| BALANCE => fun env SA => Return _ (balance env, SA)
| ADDRESS =>
fun env '(x, SA) => Return _ (address_ env _ x, SA)
| CONTRACT _ =>
fun env '(x, SA) => Return _ (contract_ env _ x, SA)
| SOURCE => fun env SA => Return _ (source env, SA)
| SENDER => fun env SA => Return _ (sender env, SA)
| SELF => fun env SA => Return _ (self env, SA)
| AMOUNT => fun env SA => Return _ (amount env, SA)
| IMPLICIT_ACCOUNT =>
fun env '(x, SA) => Return _ (implicit_account env x, SA)
| STEPS_TO_QUOTA =>
fun env SA => Return _ (steps_to_quota env, SA)
| NOW => fun env SA => Return _ (now env, SA)
| PACK => fun env '(x, SA) => Return _ (pack env _ x, SA)
| UNPACK => fun env '(x, SA) => Return _ (unpack env _ x, SA)
| HASH_KEY => fun env '(x, SA) => Return _ (hash_key env x, SA)
| BLAKE2B => fun env '(x, SA) => Return _ (blake2b env x, SA)
| SHA256 => fun env '(x, SA) => Return _ (sha256 env x, SA)
| SHA512 => fun env '(x, SA) => Return _ (sha512 env x, SA)
| CHECK_SIGNATURE =>
fun env '(x, (y, (z, SA))) =>
Return _ (check_signature env x y z, SA)
end env
end.
(* The evaluator does not depend on the amount of fuel provided *)
Lemma eval_deterministic_le :
forall fuel1 fuel2,
fuel1 <= fuel2 ->
forall {self_type env} {A B} (i : instruction self_type A B) st,
success (eval env i fuel1 st) ->
eval env i fuel1 st = eval env i fuel2 st.
Proof.
induction fuel1; intros fuel2 Hle self_type env 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_type env} fuel1 fuel2 {A B} (i : instruction self_type A B) S :
success (eval env i fuel1 S) ->
success (eval env i fuel2 S) ->
eval env i fuel1 S = eval env 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 {self_type},
@proto_env self_type -> forall {A B}, instruction self_type A B ->
(stack B -> Prop) -> stack A -> Prop)
{self_type} env A B
(i : instruction self_type A B) :
(stack B -> Prop) -> (stack A -> Prop) :=
match i in instruction self_type A B return @proto_env self_type -> (stack B -> Prop) -> (stack A -> Prop) with
| FAILWITH => fun _ _ _ => false
| NOOP => fun env psi st => psi st
| SEQ B C => fun env psi =>
eval_precond_n env B (eval_precond_n env C psi)
| IF_ bt bf =>
fun env psi '(b, SA) => if b then eval_precond_n env bt psi SA
else eval_precond_n env bf psi SA
| LOOP body =>
fun env psi '(b, SA) => if b then eval_precond_n env (body;; (LOOP body)) psi SA
else psi SA
| LOOP_LEFT body =>
fun env psi '(ab, SA) =>
match ab with
| inl x => eval_precond_n env (body;; LOOP_LEFT body) psi (x, SA)
| inr y => psi (y, SA)
end
| DIP i =>
fun env psi '(y, SA) => eval_precond_n env i (fun SB => psi (y, SB)) SA
| @EXEC st _ _ =>
fun (env : @proto_env st) psi '(x, (f, SA)) =>
eval_precond_n (no_self env) f (fun '(y, tt) => psi (y, SA)) (x, tt)
| DROP => fun env psi '(_, SA) => psi SA
| DUP => fun env psi '(x, SA) => psi (x, (x, SA))
| SWAP => fun env psi '(x, (y, SA)) => psi (y, (x, SA))
| PUSH a x => fun env psi SA => psi (concrete_data_to_data _ x, SA)
| UNIT => fun env psi SA => psi (tt, SA)
| LAMBDA a b code => fun env psi SA => psi (code, SA)
| EQ => fun env psi '(x, SA) => psi ((x =? 0)%Z, SA)
| NEQ => fun env psi '(x, SA) => psi (negb (x =? 0)%Z, SA)
| LT => fun env psi '(x, SA) => psi ((x <? 0)%Z, SA)
| GT => fun env psi '(x, SA) => psi ((x >? 0)%Z, SA)
| LE => fun env psi '(x, SA) => psi ((x <=? 0)%Z, SA)
| GE => fun env psi '(x, SA) => psi ((x >=? 0)%Z, SA)
| @OR _ _ s =>
fun env psi '(x, (y, SA)) => psi (or_fun _ (bitwise_variant_field _ s) x y, SA)
| @AND _ _ s =>
fun env psi '(x, (y, SA)) => psi (and _ (bitwise_variant_field _ s) x y, SA)
| @XOR _ _ s =>
fun env psi '(x, (y, SA)) => psi (xor _ (bitwise_variant_field _ s) x y, SA)
| @NOT _ _ s =>
fun env psi '(x, SA) => psi (not _ _ (not_variant_field _ s) x, SA)
| @NEG _ _ s =>
fun env psi '(x, SA) => psi (neg _ (neg_variant_field _ s) x, SA)
| ABS => fun env psi '(x, SA) => psi (Z.abs_N x, SA)
| ISNAT => fun env psi '(x, SA) => psi (if (x >=? 0)%Z then (Some (Z.to_N x), SA) else (None, SA))
| INT => fun env psi '(x, SA) => psi (Z.of_N x, SA)
| @ADD _ _ _ s =>
fun env psi '(x, (y, SA)) =>
precond (add _ _ _ (add_variant_field _ _ s) x y) (fun z => psi (z, SA))
| @SUB _ _ _ s =>
fun env psi '(x, (y, SA)) =>
precond (sub _ _ _ (sub_variant_field _ _ s) x y) (fun z => psi (z, SA))
| @MUL _ _ _ s =>
fun env psi '(x, (y, SA)) =>
precond (mul _ _ _ (mul_variant_field _ _ s) x y) (fun z => psi (z, SA))
| @EDIV _ _ _ s =>
fun env psi '(x, (y, SA)) =>
psi (ediv _ _ _ _ (ediv_variant_field _ _ s) x y, SA)
| LSL => fun env psi '(x, (y, SA)) => psi (N.shiftl x y, SA)
| LSR => fun env psi '(x, (y, SA)) => psi (N.shiftr x y, SA)
| COMPARE =>
fun env psi '(x, (y, SA)) => psi (comparison_to_int (compare _ x y), SA)
| @CONCAT _ _ s =>
fun env psi '(x, (y, SA)) =>
psi (concat _ (stringlike_variant_field _ s) x y, SA)
| @SLICE _ _ i =>
fun env psi '(n1, (n2, (s, SA))) =>
psi (slice _ (stringlike_variant_field _ i) n1 n2 s, SA)
| PAIR => fun env psi '(x, (y, SA)) => psi ((x, y), SA)
| CAR => fun env psi '((x, y), SA) => psi (x, SA)
| CDR => fun env psi '((x, y), SA) => psi (y, SA)
| EMPTY_SET a => fun env psi SA => psi (set.empty _ (compare a), SA)
| @MEM _ _ _ s =>
fun env psi '(x, (y, SA)) =>
psi (mem _ _ (mem_variant_field _ _ s) x y, SA)
| @UPDATE _ _ _ _ s =>
fun env psi '(x, (y, (z, SA))) =>
psi (update _ _ _ (update_variant_field _ _ _ s) x y z, SA)
| @ITER _ _ s _ body =>
fun env psi '(x, SA) =>
match iter_destruct _ _ (iter_variant_field _ s) x with
| None => psi SA
| Some (a, y) =>
eval_precond_n env body
(fun SB => eval_precond_n env (ITER body) psi (y, SB))
(a, SA)
end
| @SIZE _ _ s =>
fun env psi '(x, SA) => psi (N.of_nat (size _ (size_variant_field _ s) x), SA)
| EMPTY_MAP k val =>
fun env psi SA => psi (map.empty (comparable_data k) (data val) _, SA)
| @GET _ _ _ s =>
fun env psi '(x, (y, SA)) => psi (get _ _ _ (get_variant_field _ _ s) x y, SA)
| @MAP _ _ _ s _ body =>
let v := (map_variant_field _ _ s) in
fun env psi '(x, SA) =>
match map_destruct _ _ _ _ v x with
| None => psi (map_empty _ _ _ _ v, SA)
| Some (a, y) =>
eval_precond_n env body
(fun '(b, SB) =>
eval_precond_n env (MAP body)
(fun '(c, SC) => psi (map_insert _ _ _ _ v a b c, SC))
(y, SB))
(a, SA)
end
| SOME => fun env psi '(x, SA) => psi (Some x, SA)
| NONE _ => fun env psi SA => psi (None, SA)
| IF_NONE bt bf =>
fun env psi '(b, SA) =>
match b with
| None => eval_precond_n env bt psi SA
| Some b => eval_precond_n env bf psi (b, SA)
end
| LEFT _ => fun env psi '(x, SA) => psi (inl x, SA)
| RIGHT _ => fun env psi '(x, SA) => psi (inr x, SA)
| IF_LEFT bt bf =>
fun env psi '(b, SA) =>
match b with
| inl a => eval_precond_n env bt psi (a, SA)
| inr b => eval_precond_n env bf psi (b, SA)
end
| IF_RIGHT bt bf =>
fun env psi '(b, SA) =>
match b with
| inl a => eval_precond_n env bf psi (a, SA)
| inr b => eval_precond_n env bt psi (b, SA)
end
| CONS => fun env psi '(x, (y, SA)) => psi (cons x y, SA)
| NIL _ => fun env psi SA => psi (nil, SA)
| IF_CONS bt bf =>
fun env psi '(l, SA) =>
match l with
| cons a b => eval_precond_n env bt psi (a, (b, SA))
| nil => eval_precond_n env bf psi SA
end
| CREATE_CONTRACT_literal _ _ f =>
fun env 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 env psi '(a, (b, (c, (d, SA)))) =>
let (oper, contr) := create_account env a b c d in
psi (oper, (contr, SA))
| TRANSFER_TOKENS =>
fun env psi '(a, (b, (c, SA))) =>
psi (transfer_tokens env _ a b c, SA)
| SET_DELEGATE =>
fun env psi '(x, SA) =>
psi (set_delegate env x, SA)
| BALANCE =>
fun env psi SA => psi (balance env, SA)
| ADDRESS =>
fun env psi '(x, SA) => psi (address_ env _ x, SA)
| CONTRACT _ =>
fun env psi '(x, SA) => psi (contract_ env _ x, SA)
| SOURCE => fun env psi SA => psi (source env, SA)
| SENDER => fun env psi SA => psi (sender env, SA)
| SELF => fun env psi SA => psi (self env, SA)
| AMOUNT => fun env psi SA => psi (amount env, SA)
| IMPLICIT_ACCOUNT =>
fun env psi '(x, SA) => psi (implicit_account env x, SA)
| STEPS_TO_QUOTA =>
fun env psi SA => psi (steps_to_quota env, SA)
| NOW => fun env psi SA => psi (now env, SA)
| PACK => fun env psi '(x, SA) => psi (pack env _ x, SA)
| UNPACK =>
fun env psi '(x, SA) => psi (unpack env _ x, SA)
| HASH_KEY =>
fun env psi '(x, SA) => psi (hash_key env x, SA)
| BLAKE2B =>
fun env psi '(x, SA) => psi (blake2b env x, SA)
| SHA256 => fun env psi '(x, SA) => psi (sha256 env x, SA)
| SHA512 => fun env psi '(x, SA) => psi (sha512 env x, SA)
| CHECK_SIGNATURE =>
fun env psi '(x, (y, (z, SA))) =>
psi (check_signature env x y z, SA)
end env.
Fixpoint eval_precond (fuel : Datatypes.nat) :
forall {self_type} env {A B},
instruction self_type 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 env A B} (i : instruction sty A B) n st psi :
precond (eval env i n st) psi <-> eval_precond n env i psi st.
Proof.
generalize sty env A B i st psi; clear sty env A B i st psi.
induction n; intros sty env 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 _ _ _ _ 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; 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 (a, 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.
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.
