Skip to main content

🍃 V7.v

Environment

Gitlab

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.

Additional environment definitions, sometimes used by the tests.


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.

Axioms and tactics about the existential casts generated by

coq-of-ocaml.
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
    | Setrewrite (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 :: tlerr' :: 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 :: tlList.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.

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"
  ].

Check if an error trace has no internal errors.
  Definition not_internal (err : trace _error) : Prop :=
    in_ err internal_errors = false.
End Error.

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 xf x
  | Pervasives.Error errError.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 xf x
  | Pervasives.Error errFalse
  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 xf x
  | Pervasives.Error errTrue
  end.

Notation "'letP?' x ':=' X 'in' Y" :=
  (bind_prop X (fun xY))
  (at level 200, x name, X at level 100, Y at level 200).

Notation "'letP?' ' x ':=' X 'in' Y" :=
  (bind_prop X (fun xY))
  (at level 200, x pattern, X at level 100, Y at level 200).

Notation "'letP?!' x ':=' X 'in' Y" :=
  (bind_prop_strict X (fun xY))
  (at level 200, x name, X at level 100, Y at level 200).

Notation "'letP?!' ' x ':=' X 'in' Y" :=
  (bind_prop_strict X (fun xY))
  (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 xY))
  (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 xY))
  (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.

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.

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.

Returns the head of a term, a helper used below
Ltac head f :=
  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.

Destruct [e] in [if e ...]
Ltac step_outer_if :=
  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].

Unfold [e] in [P e]
Ltac unfold_after H :=
  match goal with
  | |- H ?elet e := head e in unfold e
  end.

Unfold [e] in [P _ e]
Ltac unfold_after1 H :=
  match goal with
  | |- H _ ?elet e := head e in unfold e
  end.

Unfold [e] in [P _ _ e]
Ltac unfold_after2 H :=
  match goal with
  | |- H _ _ ?elet 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).

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.

Destruct by type pattern, [destruct_by_type (Raw_context.Valid.t _)]
Tactic Notation "destruct_by_type" open_constr(pat) :=
  select pat (fun Hdestruct 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 Hdestruct 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 Happly 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 Hrename 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.