Skip to main content

🖼️ Raw_context.v

Proofs

See code, Gitlab , OCaml

Apply a list of gas consume operations, until it fails. In case of failure, return [None].
  Fixpoint apply_costs ctxt costs : option Raw_context.t :=
    match costs with
    | []Some ctxt
    | cost :: costs
      match Raw_context.consume_gas ctxt cost with
      | Pervasives.Ok ctxtapply_costs ctxt costs
      | Pervasives.Error _None
      end
    end.

Project the fields of the context corresponding to the gas status.
Equality check between two contexts, to compare the gas part.
  Definition eq_on_gas_status (ctxt1 ctxt2 : Raw_context.t) : Prop :=
    extract_gas_status ctxt1 = extract_gas_status ctxt2.

  Definition eq_on_gas_status_option (ctxt1 ctxt2 : option Raw_context.t)
    : Prop :=
    Option.map extract_gas_status ctxt1 = Option.map extract_gas_status ctxt2.

  Fixpoint apply_costs_eq {ctxt1 ctxt2 costs}
    : eq_on_gas_status ctxt1 ctxt2
      eq_on_gas_status_option
        (apply_costs ctxt1 costs) (apply_costs ctxt2 costs).
    destruct costs; simpl; cbv - [apply_costs Gas_limit_repr.Arith.sub_opt];
      try congruence.
    intro H; inversion H.
    destruct (Gas_limit_repr.Arith.sub_opt _ _).
    { apply apply_costs_eq.
      cbv; congruence.
    }
    { match goal with
      | [|- context[if ?e then _ else _]] ⇒
        destruct e eqn:H_eq; rewrite <- H_eq in *; clear H_eq
      end; trivial.
      apply apply_costs_eq; cbv; congruence.
    }
  Qed.

  Module Valid.
We consider a gas consumption to be valid when it can be deduced from the application of a list of gas consumptions.
    Definition t initial_ctxt final_ctxt costs : Prop :=
      eq_on_gas_status_option
        (apply_costs initial_ctxt costs) (Some final_ctxt).

Not changing the context is a valid gas consumption.
    Lemma refl ctxt : t ctxt ctxt [].
      reflexivity.
    Qed.

Transitivity rule.
    Fixpoint trans ctxt1 ctxt2 ctxt3 costs12 costs23
      : t ctxt1 ctxt2 costs12 t ctxt2 ctxt3 costs23
        t ctxt1 ctxt3 (List.app costs12 costs23).
      cbv - [apply_costs extract_gas_status List.app].
      destruct costs12; simpl; intros H12 H23.
      { etransitivity;
          try apply (apply_costs_eq (ctxt2 := ctxt2)); try congruence;
          trivial.
      }
      { destruct (Raw_context.consume_gas _ _) as [ctxt1'|]; try congruence.
        now apply trans with (ctxt2 := ctxt2).
      }
    Qed.

Calling the consume gas operation with a valid cost does a valid gas consumption.
    Lemma consume_gas ctxt cost
      : Error_monad.post_when_success
          (Raw_context.consume_gas ctxt cost)
          (fun ctxt't ctxt ctxt' [cost]).
      destruct (Raw_context.consume_gas _ _) eqn:H_eq; unfold t; simpl; trivial.
      now rewrite H_eq.
    Qed.
  End Valid.
End Consume_gas.

Properties on the [Raw_context.T] signature.
Module T.
Helper to unfold [Raw_context] primitives on the storage.
  Module Unfold.
    Import Raw_context.

    Ltac all :=
      unfold
        mem, mem_tree,
        get, get_tree,
        find, find_tree,
        add, add_tree,
        init_value, init_tree,
        update, update_tree,
        remove_existing, remove_existing_tree,
        remove,
        add_or_remove, add_or_remove_tree,
        list_value, fold,
        project, absolute_key.
  End Unfold.

A [Raw_context] is valid when the fold operator respect the functional extentionality axiom.
  Module Valid.
    Import Raw_context_intf.T.

    Record t {t} {C : Raw_context.T (t := t)} : Prop := {
      fold {a : Set} depth ctxt k order (acc : a) f1 f2 :
        ( k v acc, f1 k v acc = f2 k v acc)
        C.(fold) depth ctxt k order acc f1 =
        C.(fold) depth ctxt k order acc f2;
    }.
    Arguments t {_}.
  End Valid.

The equality between two [Raw_context.T].
  Module Eq.
    Import Raw_context_intf.T.

    Record t {t} {C1 C2 : Raw_context.T (t := t)} : Prop := {
      mem ctxt k : C1.(mem) ctxt k = C2.(mem) ctxt k;
      mem_tree ctxt k : C1.(mem_tree) ctxt k = C2.(mem_tree) ctxt k;
      get ctxt k : C1.(get) ctxt k = C2.(get) ctxt k;
      get_tree ctxt k : C1.(get_tree) ctxt k = C2.(get_tree) ctxt k;
      find ctxt k : C1.(find) ctxt k = C2.(find) ctxt k;
      find_tree ctxt k : C1.(find_tree) ctxt k = C2.(find_tree) ctxt k;
      list_value ctxt offset length k :
        C1.(list_value) ctxt offset length k =
        C2.(list_value) ctxt offset length k;
      init_value ctxt k v : C1.(init_value) ctxt k v = C2.(init_value) ctxt k v;
      init_tree ctxt k v : C1.(init_tree) ctxt k v = C2.(init_tree) ctxt k v;
      update ctxt k v : C1.(update) ctxt k v = C2.(update) ctxt k v;
      update_tree ctxt k v : C1.(update_tree) ctxt k v = C2.(update_tree) ctxt k v;
      add ctxt k v : C1.(add) ctxt k v = C2.(add) ctxt k v;
      add_tree ctxt k v : C1.(add_tree) ctxt k v = C2.(add_tree) ctxt k v;
      remove ctxt k : C1.(remove) ctxt k = C2.(remove) ctxt k;
      remove_existing ctxt k :
        C1.(remove_existing) ctxt k = C2.(remove_existing) ctxt k;
      remove_existing_tree ctxt k :
        C1.(remove_existing_tree) ctxt k = C2.(remove_existing_tree) ctxt k;
      add_or_remove ctxt k v :
        C1.(add_or_remove) ctxt k v = C2.(add_or_remove) ctxt k v;
      add_or_remove_tree ctxt k v :
        C1.(add_or_remove_tree) ctxt k v = C2.(add_or_remove_tree) ctxt k v;
      fold {a : Set} depth ctxt k order (acc : a) f :
        C1.(fold) depth ctxt k order acc f =
        C2.(fold) depth ctxt k order acc f;
      Tree : Raw_context_intf.TREE.Eq.t C1.(Tree) C2.(Tree);
      project ctxt : C1.(project) ctxt = C2.(project) ctxt;
      absolute_key ctxt k : C1.(absolute_key) ctxt k = C2.(absolute_key) ctxt k;
      (* We do not check [consume_gas], [check_enough_gas] and [description]. *)
    }.
    Arguments t {_}.
  End Eq.

A [Kernel] of primitive operations which are enough to describe a whole [Raw_context.T].
  Module Kernel.
    Record signature {t : Set} : Set := {
      
The path from the root of the context store. It may depend on the value of the context for indexed raw contexts.
      absolute_key : t Context.key;
      
Extract the root raw context.
      project : t Raw_context.t;
      
Update the root raw context part of the context, and keep everything else (typically, keeps the index for indexed raw contexts).
      update : t Raw_context.t t;
    }.
  End Kernel.
  Definition Kernel := @Kernel.signature.
  Arguments Kernel {_}.

The equality between two raw kernels.
  Module Kernel_eq.
    Import Kernel.

    Record t {t} {K1 K2 : Kernel (t := t)} : Prop := {
      absolute_key ctxt : K1.(absolute_key) ctxt = K2.(absolute_key) ctxt;
      project ctxt : K1.(project) ctxt = K2.(project) ctxt;
      update ctxt root_ctxt :
        K1.(update) ctxt root_ctxt = K2.(update) ctxt root_ctxt;
    }.
    Arguments t {_}.
  End Kernel_eq.

Define a whole raw context from its kernel.
  Definition of_kernel {t} (K : Kernel (t := t)) : Raw_context.T (t := t) :=
    let '{|
      Kernel.absolute_key := absolute_key;
      Kernel.project := project;
      Kernel.update := update
    |} := K in
    let to_key ctxt k :=
      absolute_key ctxt ++ k in
    {|
      Raw_context_intf.T.mem ctxt k :=
        Raw_context.mem (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.mem_tree ctxt k :=
        Raw_context.mem_tree (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.get ctxt k :=
        Raw_context.get (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.get_tree ctxt k :=
        Raw_context.get_tree (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.find ctxt k :=
        Raw_context.find (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.find_tree ctxt k :=
        Raw_context.find_tree (project ctxt) (to_key ctxt k);
      Raw_context_intf.T.list_value ctxt offset length k :=
        Raw_context.list_value (project ctxt) offset length (to_key ctxt k);
      Raw_context_intf.T.init_value ctxt k v :=
        let? root := Raw_context.init_value (project ctxt) (to_key ctxt k) v in
        return? update ctxt root;
      Raw_context_intf.T.init_tree ctxt k v :=
        let? root := Raw_context.init_tree (project ctxt) (to_key ctxt k) v in
        return? update ctxt root;
      Raw_context_intf.T.update ctxt k v :=
        let? root := Raw_context.update (project ctxt) (to_key ctxt k) v in
        return? update ctxt root;
      Raw_context_intf.T.update_tree ctxt k v :=
        let? root := Raw_context.update_tree (project ctxt) (to_key ctxt k) v in
        return? update ctxt root;
      Raw_context_intf.T.add ctxt k v :=
        let root := Raw_context.add (project ctxt) (to_key ctxt k) v in
        update ctxt root;
      Raw_context_intf.T.add_tree ctxt k v :=
        let root := Raw_context.add_tree (project ctxt) (to_key ctxt k) v in
        update ctxt root;
      Raw_context_intf.T.remove ctxt k :=
        let root := Raw_context.remove (project ctxt) (to_key ctxt k) in
        update ctxt root;
      Raw_context_intf.T.remove_existing ctxt k :=
        let? root :=
          Raw_context.remove_existing (project ctxt) (to_key ctxt k) in
        return? update ctxt root;
      Raw_context_intf.T.remove_existing_tree ctxt k :=
        let? root :=
          Raw_context.remove_existing_tree (project ctxt) (to_key ctxt k) in
        return? update ctxt root;
      Raw_context_intf.T.add_or_remove ctxt k v :=
        let root :=
          Raw_context.add_or_remove (project ctxt) (to_key ctxt k) v in
        update ctxt root;
      Raw_context_intf.T.add_or_remove_tree ctxt k v :=
        let root :=
          Raw_context.add_or_remove_tree (project ctxt) (to_key ctxt k) v in
        update ctxt root;
      Raw_context_intf.T.fold _ depth ctxt k order acc f :=
        Raw_context.fold depth (project ctxt) (to_key ctxt k) order acc f;
      Raw_context_intf.T.config_value :=
        axiom "config_value";
      Raw_context_intf.T.Tree :=
        {|
          Raw_context_intf.TREE.mem :=
            Raw_context.Tree.(Raw_context_intf.TREE.mem);
          Raw_context_intf.TREE.mem_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.mem_tree);
          Raw_context_intf.TREE.get :=
            Raw_context.Tree.(Raw_context_intf.TREE.get);
          Raw_context_intf.TREE.get_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.get_tree);
          Raw_context_intf.TREE.find :=
            Raw_context.Tree.(Raw_context_intf.TREE.find);
          Raw_context_intf.TREE.find_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.find_tree);
          Raw_context_intf.TREE.list_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.list_value);
          Raw_context_intf.TREE.init_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.init_value);
          Raw_context_intf.TREE.init_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.init_tree);
          Raw_context_intf.TREE.update :=
            Raw_context.Tree.(Raw_context_intf.TREE.update);
          Raw_context_intf.TREE.update_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.update_tree);
          Raw_context_intf.TREE.add :=
            Raw_context.Tree.(Raw_context_intf.TREE.add);
          Raw_context_intf.TREE.add_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.add_tree);
          Raw_context_intf.TREE.remove :=
            Raw_context.Tree.(Raw_context_intf.TREE.remove);
          Raw_context_intf.TREE.remove_existing :=
            Raw_context.Tree.(Raw_context_intf.TREE.remove_existing);
          Raw_context_intf.TREE.remove_existing_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.remove_existing_tree);
          Raw_context_intf.TREE.add_or_remove :=
            Raw_context.Tree.(Raw_context_intf.TREE.add_or_remove);
          Raw_context_intf.TREE.add_or_remove_tree :=
            Raw_context.Tree.(Raw_context_intf.TREE.add_or_remove_tree);
          Raw_context_intf.TREE.fold _ :=
            Raw_context.Tree.(Raw_context_intf.TREE.fold);
          Raw_context_intf.TREE.config_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.config_value);
          (* The definition of the [Tree] is very long and differs only on this
             field. *)

          Raw_context_intf.TREE.empty ctxt :=
            Raw_context.Tree.empty (project ctxt);
          Raw_context_intf.TREE.is_empty :=
            Raw_context.Tree.(Raw_context_intf.TREE.is_empty);
          Raw_context_intf.TREE.kind_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.kind_value);
          Raw_context_intf.TREE.to_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.to_value);
          Raw_context_intf.TREE.hash_value :=
            Raw_context.Tree.(Raw_context_intf.TREE.hash_value);
          Raw_context_intf.TREE.equal :=
            Raw_context.Tree.(Raw_context_intf.TREE.equal);
          Raw_context_intf.TREE.clear :=
            Raw_context.Tree.(Raw_context_intf.TREE.clear);
        |};
      Raw_context_intf.T.verify_tree_proof ctxt :=
        axiom "verify_tree_proof";
      Raw_context_intf.T.verify_stream_proof ctxt :=
        axiom "verify_stream_proof";
      Raw_context_intf.T.equal_config :=
        axiom "equal_config";
      Raw_context_intf.T.project ctxt :=
        project ctxt;
      Raw_context_intf.T.absolute_key ctxt k :=
        to_key ctxt k;
      Raw_context_intf.T.consume_gas :=
        axiom "consume_gas";
      Raw_context_intf.T.check_enough_gas :=
        axiom "check_enough_gas";
      Raw_context_intf.T.description :=
        axiom "description";
    |}.

Generating contexts from two equal kernels yields two equal raw contexts.
  Lemma from_kernel_implies_eq {t : Set} (K1 K2 : Kernel (t := t)) :
    Kernel_eq.t K1 K2
    Eq.t (of_kernel K1) (of_kernel K2).
  Proof.
    intros []; repeat constructor; intros; simpl;
      repeat match goal with
      | |- context [let? _ := ?e in _] ⇒
        destruct e eqn:?;
        simpl
      end;
      repeat match goal with
      | H : _ |- _rewrite H in ×
      end;
      congruence.
  Qed.

If a raw context is described by a given kernel.
  Definition is_from_kernel {t} (C : Raw_context.T (t := t))
    (K : Kernel (t := t)) : Prop :=
    Eq.t C (of_kernel K).

The kernel of the root raw context.
  Definition M_kernel : Kernel (t := Raw_context.t) := {|
    Kernel.absolute_key _ := [];
    Kernel.project ctxt := ctxt;
    Kernel.update _ root := root;
  |}.

The main raw context can be expressed from a kernel.
  Lemma M_is_from_kernel : is_from_kernel Raw_context.M M_kernel.
  Proof.
    repeat constructor; intros; simpl; try reflexivity;
      match goal with
      | |- context [let? _ := ?e in _] ⇒
        destruct e eqn:?;
        simpl
      end;
      sfirstorder.
  Qed.
End T.

Module Valid.
  Module back.
    Module Valid.
      Import Raw_context.back.
      Record t (back : Raw_context.back) : Prop := {
        constants :
          Constants_repr.Parametric.Valid.t back.(constants);
        round_durations : Round_repr.Durations.Valid.t back.(round_durations);
        cycle_eras :
          List.Forall Level_repr.Cycle_era.Valid.t back.(cycle_eras);
        level : Level_repr.Valid.t back.(level);
        (* Do we have a notion of a valid Time.t ?
          predecessor_timestamp : ???;
          timestamp : ???;
        *)

        fees : Tez_repr.Valid.t back.(fees);
        origination_nonce :
          Option.Forall Origination_nonce.Valid.t back.(origination_nonce);
        (* Do we have a notion of valid Lazy_storage_kind.Temp_ids.t
          temporary_lazy_storage_ids : ???
         *)

        internal_nonce : Pervasives.Int.Valid.t back.(internal_nonce);
        internal_nonces_used :
          List.Forall Pervasives.Int.Valid.t (Raw_context.Int_set.(_Set.S.elements) back.(internal_nonces_used));
        (* Int_set.(_Set.S.t); *)
        remaining_block_gas :
          Saturation_repr.Valid.t back.(remaining_block_gas);
        (* Do we have a notion of valid Raw_consensus.t
          consensus : ???
         *)

        (* this doesn't work
        sampler_state :
          let keys := Cycle_repr.Map.(S.fold)
            (fun (k : Seed_repr.t) v acc => k :: acc)
            back.(sampler_state) [] in
          List.Forall Seed_repr.Seed.Valid.t keys;
            (*
            Cycle_repr.Map.(Map.S.t)
            (Seed_repr.seed *
                  Sampler.t (Signature.public_key * Signature.public_key_hash)); *)

       *)

        stake_distribution_for_current_cycle :
          back.(stake_distribution_for_current_cycle) None;
        }.
      End Valid.
  End back.

  Record t (ctxt : Raw_context.t) : Prop := {
    back : back.Valid.t ctxt.(Raw_context.t.back);
  }.
End Valid.

Context contains an origination nonce
The context has one [Level_repr.cycle_era] and [level] is greather than this era
Module Has_one_era.
  Definition t (ctxt : Raw_context.t)
             (era : Level_repr.cycle_era) : Prop :=
    Raw_context.cycle_eras ctxt = [era].
End Has_one_era.

The encoding [storage_error_encoding] is valid.
Lemma storage_error_encoding_is_valid :
  Data_encoding.Valid.t (fun _True)
    Raw_context.storage_error_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto. sauto l: on.
Qed.
#[global] Hint Resolve storage_error_encoding_is_valid : Data_encoding_db.