🍃 V7.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Export TezosOfOCaml.Environment.RecordUpdate.
Require Export TezosOfOCaml.Environment.V7_modules.
Require Export Lia.
Module Notations.
Export Compare.Notations.
Export Int32.Notations.
Export Int64.Notations.
Export Option.Notations.
Export Pervasives.Notations.
Export Z.Notations.
End Notations.
Export Notations.
Require Import CoqOfOCaml.Settings.
Require Export TezosOfOCaml.Environment.RecordUpdate.
Require Export TezosOfOCaml.Environment.V7_modules.
Require Export Lia.
Module Notations.
Export Compare.Notations.
Export Int32.Notations.
Export Int64.Notations.
Export Option.Notations.
Export Pervasives.Notations.
Export Z.Notations.
End Notations.
Export Notations.
Definition wrap_tzerror (error : Error_monad._error) : Error_monad._error :=
error.
Definition wrap_tztrace t :=
List.map wrap_tzerror t.
Definition wrap_tzresult {a : Set} (r : M? a) : M? a :=
Result.map_error wrap_tztrace r.
Module Random.
Module State.
Parameter t : Set.
Parameter make : array int → t.
End State.
End Random.
Ltac Zify.zify_pre_hook ::=
autounfold with tezos_z in *;
unfold
Pervasives.normalize_int,
Pervasives.normalize_int32,
Pervasives.normalize_int64 in *;
unfold
Pervasives.two_pow_31,
Pervasives.two_pow_32,
Pervasives.two_pow_62,
Pervasives.two_pow_63,
Pervasives.two_pow_64 in *;
simpl (Compare.Int.(Compare.S.op_eq)) in *;
simpl (Compare.Int.(Compare.S.op_ltgt)) in *;
simpl (Compare.Int.(Compare.S.op_lt)) in *;
simpl (Compare.Int.(Compare.S.op_gt)) in *;
simpl (Compare.Int.(Compare.S.op_lteq)) in *;
simpl (Compare.Int.(Compare.S.op_gteq)) in *;
simpl (Compare.Int.(Compare.S.compare)) in *;
simpl (Compare.Int.(Compare.S.max)) in *;
simpl (Compare.Int.(Compare.S.min)) in *;
simpl (Compare.Int.(Compare.S.equal)) in *;
simpl (_ =i32 _) in *;
simpl (_ ≠i32 _) in *;
simpl (_ ≤i32 _) in *;
simpl (_ <i32 _) in *;
simpl (_ ≥i32 _) in *;
simpl (_ >i32 _) in *;
simpl (_ =i64 _) in *;
simpl (_ ≠i64 _) in *;
simpl (_ ≤i64 _) in *;
simpl (_ <i64 _) in *;
simpl (_ ≥i64 _) in *;
simpl (_ >i64 _) in *;
simpl (_ =Z _) in *;
simpl (_ ≠Z _) in *;
simpl (_ ≤Z _) in *;
simpl (_ <Z _) in *;
simpl (_ ≥Z _) in *;
simpl (_ >Z _) in *;
autounfold with tezos_z in *;
trivial.
(* This is needed for lia work with rem and mod
https://coq.inria.fr/refman/addendum/micromega.html#coq:tacn.zify *)
Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
From Hammer Require Export Tactics.
From RecordUpdate Require Export RecordSet.
Parameter set_record_field : ∀ {A B : Set}, A → string → B → unit.
Parameter typ_with_with_non_trivial_matching : ∀ {A}, A.
Axiom cast_exists_eval_1 :
∀ {T : Set → Set} {E1 : Set} {x : T E1},
cast_exists T x = existT T E1 x.
Axiom cast_exists_eval_2 :
∀ {T : [Set ** Set] → Set} {E1 E2 : Set} {x : T [E1, E2]},
cast_exists T x = existT T [E1, E2] x.
Axiom cast_exists_eval_3 :
∀ {T : [Set ** Set ** Set] → Set} {E1 E2 E3 : Set} {x : T [E1, E2, E3]},
cast_exists T x = existT T [E1, E2, E3] x.
Axiom cast_exists_eval_4 :
∀ {T : [Set ** Set ** Set ** Set] → Set} {E1 E2 E3 E4 : Set}
{x : T [E1, E2, E3, E4]},
cast_exists T x = existT T [E1, E2, E3, E4] x.
Axiom cast_exists_eval_5 :
∀ {T : [Set ** Set ** Set ** Set ** Set] → Set} {E1 E2 E3 E4 E5 : Set}
{x : T [E1, E2, E3, E4, E5]},
cast_exists T x = existT T [E1, E2, E3, E4, E5] x.
Axiom cast_exists_eval_6 :
∀ {T : [Set ** Set ** Set ** Set ** Set ** Set] → Set}
{E1 E2 E3 E4 E5 E6 : Set} {x : T [E1, E2, E3, E4, E5, E6]},
cast_exists T x = existT T [E1, E2, E3, E4, E5, E6] x.
Ltac rewrite_cast_exists :=
match goal with
| |- context[cast_exists (Es := ?Es) ?T ?x] ⇒
match Es with
| Set ⇒ rewrite (cast_exists_eval_1 (T := T) (x := x))
| [Set ** Set] ⇒ rewrite (cast_exists_eval_2 (T := T) (x := x))
| [Set ** Set ** Set] ⇒ rewrite (cast_exists_eval_3 (T := T) (x := x))
| [Set ** Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_4 (T := T) (x := x))
| [Set ** Set ** Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_5 (T := T) (x := x))
| [Set ** Set ** Set ** Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_6 (T := T) (x := x))
end
end.
Module Error.
∀ {T : Set → Set} {E1 : Set} {x : T E1},
cast_exists T x = existT T E1 x.
Axiom cast_exists_eval_2 :
∀ {T : [Set ** Set] → Set} {E1 E2 : Set} {x : T [E1, E2]},
cast_exists T x = existT T [E1, E2] x.
Axiom cast_exists_eval_3 :
∀ {T : [Set ** Set ** Set] → Set} {E1 E2 E3 : Set} {x : T [E1, E2, E3]},
cast_exists T x = existT T [E1, E2, E3] x.
Axiom cast_exists_eval_4 :
∀ {T : [Set ** Set ** Set ** Set] → Set} {E1 E2 E3 E4 : Set}
{x : T [E1, E2, E3, E4]},
cast_exists T x = existT T [E1, E2, E3, E4] x.
Axiom cast_exists_eval_5 :
∀ {T : [Set ** Set ** Set ** Set ** Set] → Set} {E1 E2 E3 E4 E5 : Set}
{x : T [E1, E2, E3, E4, E5]},
cast_exists T x = existT T [E1, E2, E3, E4, E5] x.
Axiom cast_exists_eval_6 :
∀ {T : [Set ** Set ** Set ** Set ** Set ** Set] → Set}
{E1 E2 E3 E4 E5 E6 : Set} {x : T [E1, E2, E3, E4, E5, E6]},
cast_exists T x = existT T [E1, E2, E3, E4, E5, E6] x.
Ltac rewrite_cast_exists :=
match goal with
| |- context[cast_exists (Es := ?Es) ?T ?x] ⇒
match Es with
| Set ⇒ rewrite (cast_exists_eval_1 (T := T) (x := x))
| [Set ** Set] ⇒ rewrite (cast_exists_eval_2 (T := T) (x := x))
| [Set ** Set ** Set] ⇒ rewrite (cast_exists_eval_3 (T := T) (x := x))
| [Set ** Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_4 (T := T) (x := x))
| [Set ** Set ** Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_5 (T := T) (x := x))
| [Set ** Set ** Set ** Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_6 (T := T) (x := x))
end
end.
Module Error.
Convert an error trace to the list of strings of its constructors.
Fixpoint trace_to_str_list (err : trace _error) : list string :=
match err with
| [] ⇒ []
| Build_extensible err' _ msg :: tl ⇒ err' :: trace_to_str_list tl
end.
match err with
| [] ⇒ []
| Build_extensible err' _ msg :: tl ⇒ err' :: trace_to_str_list tl
end.
Check for the intersection between two lists of strings.
Fixpoint in_quadratic (errs errs' : list string) : bool :=
match errs with
| [] ⇒ false
| hd :: tl ⇒ List.mem String.eqb hd errs' || in_quadratic tl errs'
end.
match errs with
| [] ⇒ false
| hd :: tl ⇒ List.mem String.eqb hd errs' || in_quadratic tl errs'
end.
Check if an error trace has some of its constructors in a given list.
Definition in_ (err : trace _error) (errs : list string) : bool :=
let err_strs := trace_to_str_list err in
in_quadratic err_strs errs.
let err_strs := trace_to_str_list err in
in_quadratic err_strs errs.
The list of error constructors that we consider to be internal errors.
Definition internal_errors : list string := [
"Internal_error";
(* errors from Storage.v *)
"Storage_error";
(* Errors from [Tx_rollup_l2_context.Make] *)
"Key_cannot_be_serialized";
"Value_cannot_be_serialized";
(* Special error for the [assert] in OCaml *)
"Asserted"
].
"Internal_error";
(* errors from Storage.v *)
"Storage_error";
(* Errors from [Tx_rollup_l2_context.Make] *)
"Key_cannot_be_serialized";
"Value_cannot_be_serialized";
(* Special error for the [assert] in OCaml *)
"Asserted"
].
Check if an error trace has no internal errors.
Monadic bind for propositions, checking that there are no internal
errors.
Definition bind_prop {a : Set} (x : M? a) (f : a → Prop) : Prop :=
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error err ⇒ Error.not_internal err
end.
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error err ⇒ Error.not_internal err
end.
Monadic bind for propositions, checking that there are no errors (either
internal or user-related).
Definition bind_prop_strict {a : Set} (x : M? a) (f : a → Prop) : Prop :=
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error err ⇒ False
end.
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error err ⇒ False
end.
Monadic bind for propositions, allowing any kinds of errors (including
internal errors). Ideally, we should not need this combinator. It is
there mainly for historical reasons.
Definition bind_prop_relaxed {a : Set} (x : M? a) (f : a → Prop) : Prop :=
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error err ⇒ True
end.
Notation "'letP?' x ':=' X 'in' Y" :=
(bind_prop X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'letP?' ' x ':=' X 'in' Y" :=
(bind_prop X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
Notation "'letP?!' x ':=' X 'in' Y" :=
(bind_prop_strict X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'letP?!' ' x ':=' X 'in' Y" :=
(bind_prop_strict X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
Notation "'letP?relaxed' x ':=' X 'in' Y" :=
(bind_prop_relaxed X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'letP?relaxed' ' x ':=' X 'in' Y" :=
(bind_prop_relaxed X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
match x with
| Pervasives.Ok x ⇒ f x
| Pervasives.Error err ⇒ True
end.
Notation "'letP?' x ':=' X 'in' Y" :=
(bind_prop X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'letP?' ' x ':=' X 'in' Y" :=
(bind_prop X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
Notation "'letP?!' x ':=' X 'in' Y" :=
(bind_prop_strict X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'letP?!' ' x ':=' X 'in' Y" :=
(bind_prop_strict X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
Notation "'letP?relaxed' x ':=' X 'in' Y" :=
(bind_prop_relaxed X (fun x ⇒ Y))
(at level 200, x name, X at level 100, Y at level 200).
Notation "'letP?relaxed' ' x ':=' X 'in' Y" :=
(bind_prop_relaxed X (fun x ⇒ Y))
(at level 200, x pattern, X at level 100, Y at level 200).
Destruct the matched value in an expression [e].
Ltac destruct_match_in e :=
lazymatch e with
| context[match ?e with | _ ⇒ _ end] ⇒
destruct_match_in e
| context[let? _ := ?e in _] ⇒
destruct_match_in e
| _ ⇒ destruct e eqn:?
end.
lazymatch e with
| context[match ?e with | _ ⇒ _ end] ⇒
destruct_match_in e
| context[let? _ := ?e in _] ⇒
destruct_match_in e
| _ ⇒ destruct e eqn:?
end.
Destruct one matched value in the goal.
Ltac step :=
match goal with
| |- context[match ?e with | _ ⇒ _ end] ⇒
destruct_match_in e
| |- context[let? _ := ?e in _] ⇒
destruct_match_in e
end.
match goal with
| |- context[match ?e with | _ ⇒ _ end] ⇒
destruct_match_in e
| |- context[let? _ := ?e in _] ⇒
destruct_match_in e
end.
Document the proof state by requiring that a certain expression is there,
either in the goal or the hypothesis.
Ltac grep e :=
match goal with
| |- context [e] ⇒ idtac
| _ : context [e] |- _ ⇒ idtac
| _ ⇒ fail "expression not found in the current goal"
end.
match goal with
| |- context [e] ⇒ idtac
| _ : context [e] |- _ ⇒ idtac
| _ ⇒ fail "expression not found in the current goal"
end.
Returns the head of a term, a helper used below
Ltac head f :=
match f with
| ?g _ ⇒ head g
| _ ⇒ f
end.
match f with
| ?g _ ⇒ head g
| _ ⇒ f
end.
Unfolds [t] in [match t with ...]
or [f] in [match f ... with ...]
Ltac unfold_match :=
match goal with
| |- context [match ?e with _ ⇒ _ end] ⇒ let f := head e in unfold f
end.
match goal with
| |- context [match ?e with _ ⇒ _ end] ⇒ let f := head e in unfold f
end.
Destruct [e] in [if e ...]
Ltac step_outer_if :=
match goal with
| |- context [if ?e then _ else _] ⇒ destruct e eqn:?
end.
match goal with
| |- context [if ?e then _ else _] ⇒ destruct e eqn:?
end.
Destruct [e] in [match e ...]
(also works with [if e ...])
Ltac step_outer :=
match goal with
| |- context [match ?e with _ ⇒ _ end] ⇒ destruct e eqn:?
end.
Tactic Notation "step_let?" := unfold op_gtgtquestion; step_outer; [|try easy].
match goal with
| |- context [match ?e with _ ⇒ _ end] ⇒ destruct e eqn:?
end.
Tactic Notation "step_let?" := unfold op_gtgtquestion; step_outer; [|try easy].
Unfold [e] in [P e]
Ltac unfold_after H :=
match goal with
| |- H ?e ⇒ let e := head e in unfold e
end.
match goal with
| |- H ?e ⇒ let e := head e in unfold e
end.
Unfold [e] in [P _ e]
Ltac unfold_after1 H :=
match goal with
| |- H _ ?e ⇒ let e := head e in unfold e
end.
match goal with
| |- H _ ?e ⇒ let e := head e in unfold e
end.
Unfold [e] in [P _ _ e]
Ltac unfold_after2 H :=
match goal with
| |- H _ _ ?e ⇒ let e := head e in unfold e
end.
match goal with
| |- H _ _ ?e ⇒ let e := head e in unfold e
end.
Fails except if there are [n] subgoals remaining.
Tactic Notation "remaining_goals" integer(n) := let m := numgoals in guard n = m.
[ez t] is the same as [t; [simpl|easy..]]
Tactic Notation "ez" tactic(t) := t; [simpl|easy..].
Introduces and apply injection; it expects a goal in the
form [Pervasives.Ok a = Pervasives.Ok b -> _], and
constructs a hypothesis [Hinj : a = b]
Ltac inj := (let H := fresh "Hinj" in
intros H; injection H as H).
intros H; injection H as H).
Borrowed from https://gitlab.mpi-sws.org/iris/stdpp/
Tactic Notation "select" open_constr(pat) tactic(tac) :=
match goal with
| H : pat |- _ ⇒
let T := (type of H) in unify T pat; tac H
end.
match goal with
| H : pat |- _ ⇒
let T := (type of H) in unify T pat; tac H
end.
Destruct by type pattern, [destruct_by_type (Raw_context.Valid.t _)]
Tactic Notation "destruct_by_type" open_constr(pat) :=
select pat (fun H ⇒ destruct H).
select pat (fun H ⇒ destruct H).
Like the above, but with [eqn] argument
Tactic Notation "destruct_by_type_eqn" open_constr(pat) ident(name) :=
let name := fresh name in
select pat (fun H ⇒ destruct H eqn:name).
let name := fresh name in
select pat (fun H ⇒ destruct H eqn:name).
Search for a hypothesis matching the pattern [pat] in the context and
apply it
Tactic Notation "apply_by_type" open_constr(pat) :=
select pat (fun H ⇒ apply H).
select pat (fun H ⇒ apply H).
[rename_by_type pat into Hname] rename the first hypothesis whose
type matches [pat] into [Hname]. Note that the hypothesis are
matched from bottom up.
E.g: [rename_by_type (Int32.Valid.t _) into H_valid_int]
Tactic Notation "rename_by_type" open_constr(pat) "into" ident(Hname) :=
select pat (fun H ⇒ rename H into Hname).
Ltac split_conj :=
repeat match goal with
| |- _ ∧ _ ⇒ split
end.
Module Match_spec.
select pat (fun H ⇒ rename H into Hname).
Ltac split_conj :=
repeat match goal with
| |- _ ∧ _ ⇒ split
end.
Module Match_spec.
The tactics of this module aim at automatizing the instantiation of a lemma.
- Useful for forward reasoning and eliminating [letP?] in a validity lemma
- Say that in the local context, we have
[eq_y : f a b c d = Pervasives.Ok y]
and that we have (in the global context) a validity lemma:
[lem_f a b c d : Valid a -> Valid b -> Valid c -> Valid d ->
letP? y := f a b c d in Valid y]
Then [match_spec4_nona f lem_f na] will automatically retrieve [eq_y] and
use it to instantiate lemma [lem_f] into
[na : Valid a -> Valid b -> Valid c -> Valid d -> Valid y]
In particular, [letP?] is eliminated.
- The parameter [na] is the name given to this instance of [lem_f].
- If, in the local context, we have another hypothesis similar to [eq_y]:
[eq_z : f a0 b0 c0 d0 = z], we can put [eq_z] as a parameter, so that
the tactic matches [eq_z] but not [eq_y] by specifying:
[match_spec4 eq_z f lem_f na]
- [match_spec_tac ?H_na f lem_f t] (with [H_na] optional) does the same
except that:
it choses the name of [na] of the instance of [lem_f]
it applies this instance [na] to the current goal
it solves the resulting subgoals [Valid a], [Valid b],
[Valid c], [Valid d] with tactic [t], e.g.
[match_spec_tac f lem_f assumption] proves the validity of [a], [b], [c]
and [d] by assumption.
@TODO: extend the tactic notation so that it works with 1, 2, 3, 5 or 6
parameters Remark: [simpl in lem_tmp] is crucial. Otherwise, rewrite fails. For some reason, it does not seem to work as well with `hnf in lem_tmp`, which would be quicker and more tractable.
Ltac match_spec4_na H_na f lem_f na :=
match goal with
| H_na : f ?a ?b ?c ?d = _ |- _ ⇒
specialize (lem_f a b c d) as na ; simpl in na ;
rewrite H_na in na
end.
Ltac match_spec4_nona f lem_f na :=
match goal with
| H_tmp : f ?a ?b ?c ?d = _ |- _ ⇒
specialize (lem_f a b c d) as na ; simpl in na ;
rewrite H_tmp in na
end.
Tactic Notation "match_spec" ident(H_na) constr(f) constr(lem_f) ident(na)
:= match_spec4_na H_na f lem_f na.
Tactic Notation "match_spec" constr(f) constr(lem_f) ident(na) :=
match_spec4_nona f lem_f na.
Ltac match_spec4_na_tac H_na f lem_f t :=
match goal with
| H_na : f ?a ?b ?c ?d = _ |- _ ⇒
let lem_tmp := fresh "lem_tmp"
in
specialize (lem_f a b c d) as lem_tmp ; simpl in lem_tmp ;
rewrite H_na in lem_tmp ; apply lem_tmp ; t
end.
Ltac match_spec4_nona_tac f lem_f t :=
match goal with
| H_tmp : f ?a ?b ?c ?d = _ |- _ ⇒
let lem_tmp := fresh "lem_tmp"
in
specialize (lem_f a b c d) as lem_tmp ; simpl in lem_tmp ;
rewrite H_tmp in lem_tmp ; apply lem_tmp ; t
end.
Tactic Notation "match_spec_tac" ident(H_na) constr(f) constr(lem_f)
tactic(t) := match_spec4_na_tac H_na f lem_f t.
Tactic Notation "match_spec_tac" constr(f) constr(lem_f) tactic(t) :=
match_spec4_nona_tac f lem_f t.
End Match_spec.
match goal with
| H_na : f ?a ?b ?c ?d = _ |- _ ⇒
specialize (lem_f a b c d) as na ; simpl in na ;
rewrite H_na in na
end.
Ltac match_spec4_nona f lem_f na :=
match goal with
| H_tmp : f ?a ?b ?c ?d = _ |- _ ⇒
specialize (lem_f a b c d) as na ; simpl in na ;
rewrite H_tmp in na
end.
Tactic Notation "match_spec" ident(H_na) constr(f) constr(lem_f) ident(na)
:= match_spec4_na H_na f lem_f na.
Tactic Notation "match_spec" constr(f) constr(lem_f) ident(na) :=
match_spec4_nona f lem_f na.
Ltac match_spec4_na_tac H_na f lem_f t :=
match goal with
| H_na : f ?a ?b ?c ?d = _ |- _ ⇒
let lem_tmp := fresh "lem_tmp"
in
specialize (lem_f a b c d) as lem_tmp ; simpl in lem_tmp ;
rewrite H_na in lem_tmp ; apply lem_tmp ; t
end.
Ltac match_spec4_nona_tac f lem_f t :=
match goal with
| H_tmp : f ?a ?b ?c ?d = _ |- _ ⇒
let lem_tmp := fresh "lem_tmp"
in
specialize (lem_f a b c d) as lem_tmp ; simpl in lem_tmp ;
rewrite H_tmp in lem_tmp ; apply lem_tmp ; t
end.
Tactic Notation "match_spec_tac" ident(H_na) constr(f) constr(lem_f)
tactic(t) := match_spec4_na_tac H_na f lem_f t.
Tactic Notation "match_spec_tac" constr(f) constr(lem_f) tactic(t) :=
match_spec4_nona_tac f lem_f t.
End Match_spec.