https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 927aa341eb25d2ce36bf4dcc5a599f43a33c05b0 authored by Raphaël Cauderlier on 17 March 2021, 09:24:12 UTC
Dexter proof: delay computation of the typed scripts and use vm_compute
Dexter proof: delay computation of the typed scripts and use vm_compute
Tip revision: 927aa34
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. *)
(* Operational semantics of the Michelson language *)
Require Import ZArith Lia.
Require Import String.
Require Import syntax macros.
Require NPeano.
Require Import comparable error.
Import error.Notations.
Module Type ContractContext.
Parameter get_contract_type :
smart_contract_address_constant -> Datatypes.option type.
End ContractContext.
Definition ediv_Z x y :=
(if y =? 0 then None else
let d := x / y in
let r := x mod y in
if y >? 0 then Some (d, Z.to_N r)
else if r =? 0 then Some (d, 0%N)
else Some (d + 1, Z.to_N (r - y)))%Z.
Lemma ediv_Z_correct_pos x y (Hy : (y > 0)%Z) d r :
(Some (x / y, Z.to_N (x mod y)) = Some (d, r) <-> (y * d + Z.of_N r = x /\ 0 <= Z.of_N r < Z.abs y))%Z.
Proof.
rewrite Z.abs_eq; [|lia].
split.
- intro H; injection H; clear H.
intros; subst.
assert (0 <= x mod y < y)%Z as Hbound by (apply Z.mod_pos_bound; lia).
rewrite Z2N.id; [|apply Hbound].
split; [|assumption].
symmetry.
apply Z_div_mod_eq.
assumption.
- intros (He, Hbound).
f_equal.
assert (d = x / y)%Z.
+ subst x.
rewrite Z.mul_comm.
rewrite Z_div_plus_full_l; [|lia].
assert (Z.of_N r / y = 0)%Z as Hr by (apply Z.div_small_iff; lia).
lia.
+ subst d.
f_equal.
rewrite Zmod_eq; [|lia].
assert (x - x / y * y = Z.of_N r)%Z as Hr by lia.
rewrite Hr.
apply N2Z.id.
Qed.
Lemma ediv_Z_correct x y d r :
ediv_Z x y = Some (d, r) <-> (y * d + Z.of_N r = x /\ 0 <= Z.of_N r < Z.abs y)%Z.
Proof.
unfold ediv_Z.
case_eq (y =? 0)%Z.
- intro Hy.
apply Z.eqb_eq in Hy.
subst y.
simpl.
split.
+ discriminate.
+ intros (_, Habs).
exfalso.
lia.
- intro Hy.
apply Z.eqb_neq in Hy.
case_eq (y >? 0)%Z.
+ intro Hy2.
apply Z.gtb_lt in Hy2.
apply ediv_Z_correct_pos; lia.
+ intro Hy2.
rewrite Z.gtb_ltb in Hy2.
rewrite Z.ltb_ge in Hy2.
assert (- y > 0)%Z as Hym by lia.
specialize (ediv_Z_correct_pos x (- y) Hym (- d) r); intro Hm.
rewrite Z.abs_opp in Hm.
case_eq (x mod y =? 0)%Z.
* intro Hr.
apply Z.eqb_eq in Hr.
assert (x mod - y = 0)%Z as Hmodm by (apply Z_mod_zero_opp_r; assumption).
rewrite Hmodm in Hm.
rewrite Z2N.inj_0 in Hm.
rewrite Z.mul_opp_opp in Hm.
rewrite <- Hm.
apply Z_div_zero_opp_r in Hr.
rewrite Hr.
split.
-- intuition congruence.
-- intro H; injection H; clear H.
intros.
f_equal.
f_equal; lia.
* intro Hr.
apply Z.eqb_neq in Hr.
assert (x mod - y = x mod y - y)%Z as Hmodm by (apply Z_mod_nz_opp_r; congruence).
rewrite Hmodm in Hm.
rewrite Z.mul_opp_opp in Hm.
rewrite <- Hm.
apply Z_div_nz_opp_r in Hr.
rewrite Hr.
split.
-- intro H; injection H; clear H.
intros.
f_equal.
f_equal; lia.
-- intro H; injection H; clear H.
intros.
f_equal.
f_equal; lia.
Qed.
Definition ediv_N x y :=
if (y =? 0)%N then None else Some (x / y, x mod y)%N.
Lemma ediv_N_correct x y (Hy : (y <> 0)%N) d r :
(Some (x / y, x mod y) = Some (d, r) <-> (y * d + r = x /\ r < y))%N.
Proof.
split.
- intro H; injection H; clear H.
intros; subst.
assert (x mod y < y)%N as Hbound by (apply N.mod_upper_bound; lia).
split; [|assumption].
symmetry.
apply N.div_mod.
assumption.
- intros (He, Hbound).
f_equal.
symmetry in He.
f_equal.
+ symmetry.
apply N.div_unique with (r := r); assumption.
+ symmetry.
apply N.mod_unique with (q := d); assumption.
Qed.
Module Semantics(C : ContractContext).
(* more_fuel replaces
* Hfuel : S n <= fuel with Hfuel : n <= fuel
* and fuel in the goal with S fuel
*)
Ltac more_fuel :=
match goal with
| Hfuel : (_ <= ?fuel) |- _ =>
destruct fuel as [|fuel];
[inversion Hfuel; fail
| apply le_S_n in Hfuel]
end.
(* Test *)
Goal forall fuel (Hfuel : 42 <= fuel) (F : Datatypes.nat -> Prop), F fuel.
Proof.
intros.
more_fuel.
Abort.
(* Like more_fuel, but attempts to keep Peano numbers in
* the decimal representation *)
Ltac more_fuel' :=
match goal with
| Hfuel: (S ?x) + _ <= ?fuel |- _ =>
change (S x) with (1 + x) in Hfuel;
rewrite <- plus_assoc in Hfuel; more_fuel
end.
Lemma more_fuel_add_lemma a b fuel fuel' :
fuel' = fuel - a ->
a + b <= fuel ->
(b <= fuel' /\ fuel = a + fuel').
Proof.
intros H Hfuel; subst fuel'.
split.
- apply (NPeano.Nat.sub_le_mono_r (a + b) fuel a) in Hfuel.
rewrite minus_plus in Hfuel.
assumption.
- apply le_plus_minus.
transitivity (a + b).
+ apply Nat.le_add_r.
+ assumption.
Qed.
(* fuel replace n replaces
* Hfuel : a <= fuel with Hfuel : n <= fuel
* if lia cannot prove n <= a, a subgoal is generated.
*)
Ltac fuel_replace n :=
match goal with
| Hfuel : ?a <= ?fuel |- _ =>
apply (le_trans n a fuel) in Hfuel; [|try lia]
end.
(* Test *)
Goal forall fuel a b (Hfuel : a + b <= fuel), b + a <= fuel.
Proof.
intros.
fuel_replace (b + a).
Abort.
(* more_fuel_add replaces
* Hfuel : a + b <= fuel with Hfuel : b <= fuel
* and fuel in the goal with a + fuel
*)
Ltac more_fuel_add :=
match goal with
| Hfuel : (?a + ?b <= ?fuel) |- _ =>
remember (fuel - a) as fuel' eqn:Heqfuel';
apply (more_fuel_add_lemma a b fuel fuel' Heqfuel') in Hfuel;
destruct Hfuel as (Hfuel, Heqfuel);
subst fuel; rename fuel' into fuel; clear Heqfuel'
end.
(* Test *)
Goal forall a b fuel (Hfuel : a + b <= fuel) F, F fuel.
Proof.
intros.
more_fuel_add.
Abort.
Lemma extract_fuel_lemma n fuel f (Hfuel : n <= fuel) (Hf : f <= n) :
f + (n - f) <= fuel.
Proof.
rewrite <- le_plus_minus; assumption.
Qed.
(* extract_fuel f replaces
* Hfuel : n <= fuel with Hfuel : n - f <= fuel
* and fuel in the goal with f + fuel
* if lia cannot prove f <= fuel, a subgoal is generated.
*)
Ltac extract_fuel f :=
match goal with
| Hfuel : ?n <= ?fuel |- _ =>
apply (extract_fuel_lemma n fuel f) in Hfuel; [more_fuel_add|try lia]
end.
(* Test *)
Goal forall x fuel (Hfuel : x + 4 <= fuel) F, F fuel.
Proof.
intros.
extract_fuel 2.
Abort.
Export C.
Definition get_address_type (sao : comparable_data address * annot_o)
: Datatypes.option type :=
let '(addr, ao) := sao in
opt_bind
(match addr with
| Implicit _ => Some unit
| Originated addr => get_contract_type addr
end)
(fun ty =>
get_entrypoint_opt ao ty None).
Fixpoint data (a : type) {struct a} : Set :=
match a with
| Comparable_type b => comparable_data b
| operation => operation_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)
| contract a => sig (fun sao : (address_constant * annot_o) => get_address_type sao = Some a )
end.
Record proto_env {self_ty : self_info} : Type :=
mk_proto_env
{
transfer_tokens : forall p,
data p -> tez.mutez -> data (contract p) ->
data operation;
set_delegate : Datatypes.option (comparable_data key_hash) ->
data operation;
source : data address;
sender : data address;
self :
match self_ty with
| None => Datatypes.unit
| Some (ty, self_annot) =>
forall annot_opt H,
data (contract (get_opt (get_entrypoint_opt annot_opt ty self_annot) H))
end;
amount : tez.mutez;
now : comparable_data timestamp;
}.
Definition no_self
{self_type}
(e : proto_env (self_ty := self_type)) :
proto_env (self_ty := None) :=
mk_proto_env None
(transfer_tokens e)
(set_delegate e)
(source e)
(sender e)
tt
(amount e)
(now 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.
(* Dig stuff *)
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.
Defined.
Definition stack_split {l1 l2} (S : stack (l1 +++ l2)) : (stack l1 * stack l2).
Proof.
induction l1; simpl.
- exact (tt, S).
- simpl in S.
destruct S as (x, S).
apply IHl1 in S.
destruct S as (S1, S2).
repeat (split; try assumption).
Defined.
Definition stack_dig {l1 l2 t} (SA : stack (l1+++t:::l2)) : stack (t:::l1+++l2).
Proof.
simpl.
apply stack_split in SA.
simpl in SA.
destruct SA as (S1, (x, S2)).
refine (x, _).
apply stack_app; assumption.
Defined.
Definition stack_dug {l1 l2 t} (SA : stack (t:::l1+++l2)) : stack (l1+++t:::l2).
Proof.
simpl in SA.
destruct SA as (x, S12).
apply stack_split in S12.
destruct S12 as (S1, S2).
apply stack_app.
- exact S1.
- exact (x, S2).
Defined.
Fixpoint comparable_data_to_data (a : comparable_type) (x : comparable_data a) : data a :=
match a, x with
| Cpair a b, (x, y) => (x, comparable_data_to_data _ y)
| Comparable_type_simple _, x => x
end.
Fixpoint data_to_comparable_data (a : comparable_type) (x : data a) : comparable_data a :=
match a, x with
| Cpair a b, (x, y) => (x, data_to_comparable_data _ y)
| Comparable_type_simple _, x => x
end.
Fixpoint concrete_data_to_data (a : type) (d : concrete_data a) {struct d} : data a :=
match d in concrete_data a return data a with
| Comparable_constant _ x => x
| Unit => tt
| 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
end.
Fixpoint comparable_data_to_concrete_data (a : comparable_type) {struct a} :
comparable_data a -> concrete_data a :=
match a with
| Comparable_type_simple _ => fun x => Comparable_constant _ x
| Cpair _ _ => fun '(x, y) => Pair x (comparable_data_to_concrete_data _ y)
end.
Fixpoint data_to_concrete_data (a : type) (H : Is_true (is_packable a)) (x : data a) :
concrete_data a :=
match a, H, x with
| Comparable_type b, _, x => Comparable_constant b x
| unit, _, tt => Unit
| option _, _, None => None_
| option a, H, Some y => Some_ (data_to_concrete_data a H y)
| list a, H, l =>
Concrete_list (List.map (data_to_concrete_data a H) l)
| contract _, H, _ => match H with end
| operation, H, _ => match H with end
| pair a b, H, (x, y) =>
Pair (data_to_concrete_data a (Is_true_and_left _ _ H) x)
(data_to_concrete_data b (Is_true_and_right _ _ H) y)
| or a an b bn, H, inl x =>
Left (data_to_concrete_data a (Is_true_and_left _ _ H) x) an bn
| or a an b bn, H, inr x =>
Right (data_to_concrete_data b (Is_true_and_right _ _ H) x) an bn
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 b c (v : and_variant a b c) : data a -> data b -> data c :=
match v with
| And_variant_bool => andb
| And_variant_nat => N.land
| And_variant_int =>
fun x y => Z.to_N (Z.land x (Z.of_N y))
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 add_variant_rev a b c (v : add_variant a b c) : add_variant b a c :=
match v with
| Add_variant_nat_int => Add_variant_int_nat
| Add_variant_int_nat => Add_variant_nat_int
| Add_variant_timestamp_int => Add_variant_int_timestamp
| Add_variant_int_timestamp => Add_variant_timestamp_int
| v => v
end.
Lemma add_comm a b c v x y :
@add a b c v x y = @add b a c (add_variant_rev a b c v) y x.
Proof.
destruct v; simpl; f_equal.
- apply N.add_comm.
- apply Z.add_comm.
- apply Z.add_comm.
- apply Z.add_comm.
- apply Z.add_comm.
- apply Z.add_comm.
- apply Z.add_comm.
Qed.
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 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 contract_ (an : annot_o) (p : type) (x : data address) : data (option (contract p)).
Proof.
case_eq (get_address_type (x, an)).
- intros p' H.
simpl.
case (type_dec p p').
+ intro; subst p'.
apply Some.
eexists.
eassumption.
+ intro; apply None.
- intro; apply None.
Defined.
Definition implicit_account (x : data key_hash) : data (contract unit).
Proof.
simpl.
exists (Implicit x, None).
reflexivity.
Defined.
Definition address_ a (x : data (contract a)) : data address :=
match x with exist _ (addr, _) _ => addr end.
Definition eval_opcode param_ty (env : @proto_env param_ty) {A B : stack_type}
(o : @opcode param_ty A B) (SA : stack A) : M (stack B) :=
match o, SA with
| DUP, (x, SA) => Return (x, (x, SA))
| SWAP, (x, (y, SA)) => Return (y, (x, SA))
| UNIT, SA => Return (tt, SA)
| EQ, (x, SA) => Return ((x =? 0)%Z, SA)
| NEQ, (x, SA) => Return (negb (x =? 0)%Z, SA)
| LT, (x, SA) => Return ((x <? 0)%Z, SA)
| GT, (x, SA) => Return ((x >? 0)%Z, SA)
| LE, (x, SA) => Return ((x <=? 0)%Z, SA)
| GE, (x, SA) => Return ((x >=? 0)%Z, SA)
| @OR _ _ s, (x, (y, SA)) =>
Return (or_fun _ (bitwise_variant_field _ s) x y, SA)
| @AND _ _ _ s, (x, (y, SA)) =>
Return (and _ _ _ (and_variant_field _ _ s) x y, SA)
| @XOR _ _ s, (x, (y, SA)) =>
Return (xor _ (bitwise_variant_field _ s) x y, SA)
| @NOT _ _ s, (x, SA) => Return (not _ _ (not_variant_field _ s) x, SA)
| @NEG _ _ s, (x, SA) => Return (neg _ (neg_variant_field _ s) x, SA)
| ABS, (x, SA) => Return (Z.abs_N x, SA)
| ISNAT, (x, SA) =>
Return (if (x >=? 0)%Z then (Some (Z.to_N x), SA) else (None, SA))
| INT, (x, SA) => Return (Z.of_N x, SA)
| @ADD _ _ _ s, (x, (y, SA)) =>
let! r := add _ _ _ (add_variant_field _ _ s) x y in
Return (r, SA)
| @SUB _ _ _ s, (x, (y, SA)) =>
let! r := sub _ _ _ (sub_variant_field _ _ s) x y in
Return (r, SA)
| @MUL _ _ _ s, (x, (y, SA)) =>
let! r := mul _ _ _ (mul_variant_field _ _ s) x y in
Return (r, SA)
| @EDIV _ _ _ s, (x, (y, SA)) =>
Return (ediv _ _ _ _ (ediv_variant_field _ _ s) x y, SA)
| COMPARE, (x, (y, SA)) =>
Return (comparison_to_int
(compare _
(data_to_comparable_data _ x)
(data_to_comparable_data _ y)), SA)
| PAIR, (x, (y, SA)) => Return ((x, y), SA)
| CAR, ((x, y), SA) => Return (x, SA)
| CDR, ((x, y), SA) => Return (y, SA)
| SOME, (x, SA) => Return (Some x, SA)
| NONE _, SA => Return (None, SA)
| LEFT _, (x, SA) => Return (inl x, SA)
| RIGHT _, (x, SA) => Return (inr x, SA)
| CONS, (x, (y, SA)) => Return (cons x y, SA)
| NIL _, SA => Return (nil, SA)
| TRANSFER_TOKENS, (a, (b, (c, SA))) =>
Return (transfer_tokens env _ a b c, SA)
| SET_DELEGATE, (x, SA) => Return (set_delegate env x, SA)
| ADDRESS, (x, SA) => Return (address_ _ x, SA)
| CONTRACT ao p, (x, SA) => Return (contract_ ao p x, SA)
| SOURCE, SA => Return (source env, SA)
| SENDER, SA => Return (sender env, SA)
| AMOUNT, SA => Return (amount env, SA)
| IMPLICIT_ACCOUNT, (x, SA) => Return (implicit_account x, SA)
| NOW, SA => Return (now env, SA)
| DIG n Hlen, SA => Return (stack_dig SA)
| DUG n Hlen, SA => Return (stack_dug SA)
| DROP n Hlen, SA =>
let (S1, S2) := stack_split SA in Return S2
end.
Definition if_family_destruct {A B t} (i : if_family A B t) (x : data t) : stack A + stack B :=
match i, x with
| IF_bool, true => inl tt
| IF_bool, false => inr tt
| IF_or _ _ _ _, inl x => inl (x, tt)
| IF_or _ _ _ _, inr x => inr (x, tt)
| IF_option a, None => inl tt
| IF_option a, Some x => inr (x, tt)
| IF_list a, cons x l => inl (x, (l, tt))
| IF_list a, nil => inr tt
end.
Fixpoint eval_seq
{param_ty : self_info} {tff0} (env : @proto_env param_ty) {A : stack_type} {B : stack_type}
(i : instruction_seq param_ty tff0 A B) (SA : stack A) {struct i} : M (stack B) :=
match i, SA, env with
| NOOP, SA, _ => Return SA
| Tail_fail i, SA, env => eval env i SA
| SEQ B C, SA, env =>
let! r := eval env B SA in
eval_seq env C r
end
with eval {param_ty : self_info} {tff0} (env : @proto_env param_ty) {A : stack_type} {B : stack_type}
(i : instruction param_ty tff0 A B) (SA : stack A) {struct i} : M (stack B) :=
match i, SA, env with
| Instruction_seq i, SA, env =>
eval_seq env i SA
| FAILWITH, (x, _), _ =>
Failed _ (Assertion_Failure _ 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. *)
| IF_ f bt bf, (x, SA), env =>
match if_family_destruct f x with
| inl SB => eval_seq env bt (stack_app SB SA)
| inr SB => eval_seq env bf (stack_app SB SA)
end
| PUSH a x, SA, _ => Return (concrete_data_to_data _ x, SA)
| SELF ao H, SA, env => Return (self env ao H, SA)
| Instruction_opcode o, SA, env =>
eval_opcode _ env o SA
end.
Definition eval_precond_opcode {self_type} (env : @proto_env self_type)
A B (o : @opcode self_type A B) (psi : stack B -> Prop) (SA : stack A) : Prop :=
match o, env, psi, SA with
| DUP, env, psi, (x, SA) => psi (x, (x, SA))
| SWAP, env, psi, (x, (y, SA)) => psi (y, (x, SA))
| UNIT, env, psi, SA => psi (tt, SA)
| EQ, env, psi, (x, SA) => psi ((x =? 0)%Z, SA)
| NEQ, env, psi, (x, SA) => psi (negb (x =? 0)%Z, SA)
| LT, env, psi, (x, SA) => psi ((x <? 0)%Z, SA)
| GT, env, psi, (x, SA) => psi ((x >? 0)%Z, SA)
| LE, env, psi, (x, SA) => psi ((x <=? 0)%Z, SA)
| GE, env, psi, (x, SA) => psi ((x >=? 0)%Z, SA)
| @OR _ _ s _, env, psi, (x, (y, SA)) => psi (or_fun _ (bitwise_variant_field _ s) x y, SA)
| @AND _ _ _ s _, env, psi, (x, (y, SA)) => psi (and _ _ _ (and_variant_field _ _ s) x y, SA)
| @XOR _ _ s _, env, psi, (x, (y, SA)) => psi (xor _ (bitwise_variant_field _ s) x y, SA)
| @NOT _ _ s _, env, psi, (x, SA) => psi (not _ _ (not_variant_field _ s) x, SA)
| @NEG _ _ s _, env, psi, (x, SA) => psi (neg _ (neg_variant_field _ s) x, SA)
| ABS, env, psi, (x, SA) => psi (Z.abs_N x, SA)
| ISNAT, env, psi, (x, SA) => psi (if (x >=? 0)%Z then (Some (Z.to_N x), SA) else (None, SA))
| INT, env, psi, (x, SA) => psi (Z.of_N x, SA)
| @ADD _ _ _ s _, env, psi, (x, (y, SA)) =>
precond (add _ _ _ (add_variant_field _ _ s) x y) (fun z => psi (z, SA))
| @SUB _ _ _ s _, env, psi, (x, (y, SA)) =>
precond (sub _ _ _ (sub_variant_field _ _ s) x y) (fun z => psi (z, SA))
| @MUL _ _ _ s _, env, psi, (x, (y, SA)) =>
precond (mul _ _ _ (mul_variant_field _ _ s) x y) (fun z => psi (z, SA))
| @EDIV _ _ _ s _, env, psi, (x, (y, SA)) =>
psi (ediv _ _ _ _ (ediv_variant_field _ _ s) x y, SA)
| COMPARE, env, psi, (x, (y, SA)) => psi (comparison_to_int (compare _ (data_to_comparable_data _ x) (data_to_comparable_data _ y)), SA)
| PAIR, env, psi, (x, (y, SA)) => psi ((x, y), SA)
| CAR, env, psi, ((x, y), SA) => psi (x, SA)
| CDR, env, psi, ((x, y), SA) => psi (y, SA)
| SOME, env, psi, (x, SA) => psi (Some x, SA)
| NONE _, env, psi, SA => psi (None, SA)
| LEFT _, env, psi, (x, SA) => psi (inl x, SA)
| RIGHT _, env, psi, (x, SA) => psi (inr x, SA)
| CONS, env, psi, (x, (y, SA)) => psi (cons x y, SA)
| NIL _, env, psi, SA => psi (nil, SA)
| TRANSFER_TOKENS, env, psi, (a, (b, (c, SA))) =>
psi (transfer_tokens env _ a b c, SA)
| SET_DELEGATE, env, psi, (x, SA) =>
psi (set_delegate env x, SA)
| ADDRESS, env, psi, (x, SA) => psi (address_ _ x, SA)
| CONTRACT ao p, env, psi, (x, SA) => psi (contract_ ao p x, SA)
| SOURCE, env, psi, SA => psi (source env, SA)
| SENDER, env, psi, SA => psi (sender env, SA)
| AMOUNT, env, psi, SA => psi (amount env, SA)
| IMPLICIT_ACCOUNT, env, psi, (x, SA) => psi (implicit_account x, SA)
| NOW, env, psi, SA => psi (now env, SA)
| DIG n Hlen, env, psi, st => psi (stack_dig st)
| DUG n Hlen, env, psi, st => psi (stack_dug st)
| DROP n Hlen, env, psi, SA =>
let (S1, S2) := stack_split SA in psi S2
end.
Fixpoint eval_seq_precond
{self_type} (env : @proto_env self_type) {tff0 A B}
(i : instruction_seq self_type tff0 A B)
(psi : stack B -> Prop)
(SA : stack A) : Prop :=
if tff0 then false else
match i, env, psi, SA with
| NOOP, env, psi, st => psi st
| SEQ B C, env, psi, st =>
eval_precond env B (eval_seq_precond env C psi) st
| Tail_fail i, env, psi, st =>
eval_precond env i psi st
end
with eval_precond {self_type} (env : @proto_env self_type) {tff0 A B}
(i : instruction self_type tff0 A B)
(psi : stack B -> Prop) (SA : stack A) : Prop :=
match i, env, psi, SA with
| Instruction_seq i, env, psi, SA =>
eval_seq_precond env i psi SA
| FAILWITH, _, _, _ => false
| @IF_ _ _ _ tffa tffb _ _ _ IF_bool bt bf, env, psi, (x, SA) =>
match tffa, tffb with
| false, true =>
x = true /\ eval_seq_precond env bt psi SA
| true, false =>
x = false /\ eval_seq_precond env bf psi SA
| true, true =>
false
| false, false =>
if x then eval_seq_precond env bt psi SA
else eval_seq_precond env bf psi SA
end
| @IF_ _ _ _ tffa tffb _ _ _ (IF_or a an b bn) bt bf, env, psi, (x, SA) =>
match tffa, tffb with
| false, true =>
exists y : data _,
x = inl y /\
eval_seq_precond env bt psi (y, SA)
| true, false =>
exists y : data _,
x = inr y /\ eval_seq_precond env bf psi (y, SA)
| true, true =>
false
| false, false =>
match x with
| inl y => eval_seq_precond env bt psi (y, SA)
| inr y => eval_seq_precond env bf psi (y, SA)
end
end
| @IF_ _ _ _ tffa tffb _ _ _ (IF_option a) bt bf, env, psi, (x, SA) =>
match tffa, tffb with
| false, true =>
x = None /\ eval_seq_precond env bt psi SA
| true, false =>
exists y : data _,
x = Some y /\ eval_seq_precond env bf psi (y, SA)
| true, true =>
false
| false, false =>
match x with
| None => eval_seq_precond env bt psi SA
| Some y => eval_seq_precond env bf psi (y, SA)
end
end
| @IF_ _ _ _ tffa tffb _ _ _ (IF_list a) bt bf, env, psi, (x, SA) =>
match tffa, tffb with
| false, true =>
exists (hd : data a) (tl : data (list a)),
x = cons hd tl /\ eval_seq_precond env bt psi (hd, (tl, SA))
| true, false =>
x = nil /\ eval_seq_precond env bf psi SA
| true, true =>
false
| false, false =>
match x with
| cons hd tl => eval_seq_precond env bt psi (hd, (tl, SA))
| nil => eval_seq_precond env bf psi SA
end
end
| PUSH a x, env, psi, SA => psi (concrete_data_to_data _ x, SA)
| SELF ao H, env, psi, SA => psi (self env ao H, SA)
| Instruction_opcode o, env, psi, SA =>
eval_precond_opcode env _ _ o psi SA
end.
Lemma eval_precond_opcode_correct {sty env A B} (o : opcode A B) st psi :
precond (eval_opcode sty env o st) psi <-> eval_precond_opcode env _ _ o psi st.
Proof.
destruct o; simpl;
try reflexivity;
try (destruct st; reflexivity);
try (destruct st as (x, (y, st)); reflexivity);
try (destruct st as (x, (y, st)); rewrite precond_bind; reflexivity);
try (destruct st as (x, (y, (z, SA))); reflexivity);
try (destruct st as ((x, y), st); reflexivity).
- destruct (stack_split st); reflexivity.
Qed.
Lemma precond_eval_tf_both :
(forall sty A B (i : instruction sty true A B) env psi stA, precond (eval env i stA) psi = false) *
(forall sty A B (i : instruction_seq sty true A B) env psi stA, precond (eval_seq env i stA) psi = false).
Proof.
apply tail_fail_induction_and_seq; intros; simpl.
- destruct stA; simpl.
reflexivity.
- destruct stA as (x, stA); simpl.
destruct (if_family_destruct f x); [apply H|apply H0].
- change (eval_seq env (SEQ i1 i2) stA) with
(let! r := eval env i1 stA in eval_seq env i2 r).
rewrite precond_bind.
destruct (eval env i1 stA); simpl.
+ reflexivity.
+ apply H.
- apply H.
- apply H.
Qed.
Lemma precond_eval_tf : forall sty A B (i : instruction sty true A B) env psi stA, precond (eval env i stA) psi = false.
Proof.
apply precond_eval_tf_both.
Qed.
Lemma precond_eval_seq_tf : forall sty A B (i : instruction_seq sty true A B) env psi stA, precond (eval_seq env i stA) psi = false.
Proof.
apply precond_eval_tf_both.
Qed.
Lemma eval_seq_precond_tf_aux sty A B tff (H : tff = true)
(i : instruction_seq sty tff A B) env psi stA :
eval_seq_precond env i psi stA = false.
Proof.
destruct i; simpl.
- discriminate.
- reflexivity.
- subst tff; reflexivity.
Qed.
Lemma eval_precond_tf_aux sty A B tff (H : tff = true)
(i : instruction sty tff A B) env psi stA :
eval_precond env i psi stA = false.
Proof.
destruct i; try discriminate; simpl.
- apply eval_seq_precond_tf_aux.
assumption.
- reflexivity.
- destruct i; destruct stA; destruct tffa; destruct tffb; try discriminate;
reflexivity.
Qed.
Lemma eval_seq_precond_correct_aux
(eval_precond_correct : forall sty env tff0 A B (i : instruction sty tff0 A B) st psi,
precond (eval env i st) psi <-> eval_precond env i psi st)
{sty env tff0 A B} (i : instruction_seq sty tff0 A B) st psi :
precond (eval_seq env i st) psi <-> eval_seq_precond env i psi st.
Proof.
induction i; fold data stack.
- reflexivity.
- simpl.
rewrite precond_eval_tf.
reflexivity.
- destruct tff.
+ rewrite precond_eval_seq_tf.
reflexivity.
+ simpl.
rewrite precond_bind.
rewrite <- eval_precond_correct.
apply precond_eqv.
intro SB.
apply IHi.
Defined.
Lemma ex_inj_iff {A B : Set} {P : A -> Prop} {f : A -> B} a :
(forall a1 a2 : A, f a1 = f a2 -> a1 = a2) ->
P a <-> (exists x : A, f a = f x /\ P x).
Proof.
intro Hinj.
split; intro H.
- exists a; intuition.
- destruct H as (x, (H1, H2)).
apply Hinj in H1.
congruence.
Qed.
Lemma ex_inj_iff_2 {A B C : Set} {P : A -> B -> Prop} {f : A -> B -> C} a b :
(forall (a1 a2 : A) (b1 b2 : B), f a1 b1 = f a2 b2 -> (a1 = a2 /\ b1 = b2)) ->
P a b <-> (exists (x : A) (y : B), f a b = f x y /\ P x y).
Proof.
intros Hinj.
split; intro H.
- exists a; exists b; intuition.
- destruct H as (x, (y, (H1, H2))).
apply Hinj in H1.
intuition congruence.
Qed.
Fixpoint eval_precond_correct {sty env tff0 A B} (i : instruction sty tff0 A B) st psi {struct i}:
precond (eval env i st) psi <-> eval_precond env i psi st.
Proof.
generalize (@eval_seq_precond_correct_aux eval_precond_correct);
intro eval_seq_precond_correct.
destruct i; simpl.
- apply eval_seq_precond_correct.
- destruct st; reflexivity.
- destruct st as (x, st).
destruct i; simpl.
+ destruct x; destruct tffa; destruct tffb; simpl;
try (rewrite precond_eval_seq_tf);
try (rewrite eval_seq_precond_correct); simpl; intuition congruence.
+ destruct x; destruct tffa; destruct tffb; simpl;
try (rewrite precond_eval_seq_tf);
try (rewrite eval_seq_precond_correct); simpl;
try intuition congruence.
* intuition; destruct H; intuition congruence.
* refine (ex_inj_iff d _).
intros; congruence.
* refine (ex_inj_iff d _).
intros; congruence.
* intuition; destruct H; intuition congruence.
+ destruct x; destruct tffa; destruct tffb; simpl;
try (rewrite precond_eval_seq_tf);
try (rewrite eval_seq_precond_correct); simpl;
try intuition congruence.
* refine (ex_inj_iff d _).
intros; congruence.
* intuition; destruct H; intuition congruence.
+ destruct x; destruct tffa; destruct tffb; simpl;
try (rewrite precond_eval_seq_tf);
try (rewrite eval_seq_precond_correct); simpl;
try intuition congruence.
* intuition; destruct H as (hd, (tl, (H1, H2))); intuition congruence.
* refine (ex_inj_iff_2 d x _).
intros; intuition congruence.
- reflexivity.
- reflexivity.
- apply eval_precond_opcode_correct.
Qed.
Lemma eval_precond_eqv self_type env tff A B (i : instruction self_type tff A B) st phi psi :
(forall st, phi st <-> psi st) ->
eval_precond env i phi st <-> eval_precond env i psi st.
Proof.
intro H.
do 2 rewrite <- eval_precond_correct.
apply precond_eqv.
assumption.
Qed.
Lemma eval_seq_precond_correct {sty env tff0 A B} (i : instruction_seq sty tff0 A B) st psi :
precond (eval_seq env i st) psi <-> eval_seq_precond env i psi st.
Proof.
apply eval_seq_precond_correct_aux.
intros; apply eval_precond_correct.
Qed.
Lemma eval_seq_precond_eqv self_type env tff A B (i : instruction_seq self_type tff A B) st phi psi :
(forall st, phi st <-> psi st) ->
eval_seq_precond env i phi st <-> eval_seq_precond env i psi st.
Proof.
intro H.
do 2 rewrite <- eval_seq_precond_correct.
apply precond_eqv.
assumption.
Qed.
Lemma eval_seq_assoc_aux {sty env tffa tffb A B C}
(i1 : instruction_seq sty tffa A B)
(i2 : instruction_seq sty tffb B C) H psi st :
eval_seq_precond env (instruction_app_aux i1 H i2) psi st <->
eval_seq_precond env i1 (eval_seq_precond env i2 psi) st.
Proof.
do 2 rewrite <- eval_seq_precond_correct.
induction i1; simpl.
- apply eval_seq_precond_correct.
- discriminate.
- case_eq (eval env i st); simpl.
+ intros; reflexivity.
+ intros; apply IHi1.
Qed.
Lemma eval_seq_assoc {sty env tff0 A B C}
(i1 : instruction_seq sty Datatypes.false A B)
(i2 : instruction_seq sty tff0 B C) st psi :
eval_seq_precond env (instruction_app i1 i2) psi st <->
eval_seq_precond env i1 (eval_seq_precond env i2 psi) st.
Proof.
apply eval_seq_assoc_aux.
Qed.
Lemma precond_eval_iff :
forall sf tff env
(A B : stack_type)
(lam : instruction sf tff A B)
psi psi',
(forall st', psi st' <-> psi' st') ->
forall st,
eval_precond env lam psi st <->
eval_precond env lam psi' st.
Proof.
intros sf tff env0 A B lam psi psi' H st.
do 2 rewrite <- eval_precond_correct.
apply precond_eqv. assumption.
Qed.
End Semantics.
