Skip to main content

🥷 Sapling_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Sapling.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.

Module Roots.
  Import Sapling_storage.

The same as [Roots.init_value] but which accepts [size_value] as parameter. This is needed to make proof term smaller so that the proof type checking does not take minutes
  #[bypass_check(guard)]
  Definition init_value' (ctx : Raw_context.t) (id : Storage.Sapling.id)
  (size_value : int32)
    : M? Raw_context.t :=
    let fix aux (ctx : Raw_context.t) (pos : int32) {struct pos}
      : M? Raw_context.t :=
      if pos <i32 0 then
        return? ctx
      else
        let? ctx :=
          Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.init_value)
            (ctx, id) pos Commitments.(COMMITMENTS.default_root) in
        aux ctx (Int32.pred pos) in
    let? ctx := aux ctx (Int32.pred size_value) in
    let? ctx :=
      Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.init_value)
        (ctx, id) 0 in
    let level := (Raw_context.current_level ctx).(Level_repr.t.level) in
    Storage.Sapling.Roots_level.(Storage_sigs.Single_data_storage.init_value)
      (ctx, id) level.

Proof that [init_value'] with [size_value = 120] is equal to [Roots.init_value]
  Lemma init_value'_eq (ctxt : Raw_context.t) (id : Storage.Sapling.id) :
    Roots.init_value ctxt id = init_value' ctxt id 120.
  Proof.
    hauto lq:on.
  Qed.

[Roots.get] after [init_value'] returns [Pervasives.Ok]. I had to disable guard checking because [aux] in init_value is not trivialy recursive
  #[bypass_check(guard)]
  Lemma init_value_get_is_ok
    (ctxt : Raw_context.t) (id : Storage.Sapling.id) (pos : int32) :
    letP? ctxt' := init_value' ctxt id 10 in
    Pervasives.is_ok (Roots.get ctxt' id).
  Proof.
    intros.
    unfold init_value'.
    simpl.
    repeat (
        rewrite Storage.Eq.Sapling.Roots.eq
          .(Storage_sigs.Non_iterable_indexed_data_storage
            .Eq.init_value);
        simpl;
        Storage_sigs.Non_iterable_indexed_data_storage.Op.Unfold.all;
        destruct (Map.Make _).(S.mem); [easy|]; simpl).
    Storage.auto_parse_apply.
    set (ctxt'' := Storage.apply _).
    rewrite Storage.Eq.Sapling.Roots_pos.eq
          .(Storage_sigs.Single_data_storage.Eq.init_value); simpl.
    Storage_sigs.Single_data_storage.Op.unfold_all.
    Storage.auto_parse_apply.
    match goal with
    | |- context [match ?e with __ end] ⇒ destruct e; simpl
    end; try easy.
    rewrite Storage.Eq.Sapling.Roots_level.eq
      .(Storage_sigs.Single_data_storage.Eq.init_value); simpl.
    Storage_sigs.Single_data_storage.Op.unfold_all.
    match goal with
    | |- context [match ?e with __ end] ⇒ destruct e; simpl
    end; try easy.
    unfold Roots.get.
    rewrite Storage.Eq.Sapling.Roots_pos.eq
      .(Storage_sigs.Single_data_storage.Eq.get); simpl.
    Storage_sigs.Single_data_storage.Op.unfold_all.
    repeat Storage.auto_parse_apply.
    rewrite Storage.Eq.Sapling.Roots.eq
      .(Storage_sigs.Non_iterable_indexed_data_storage.Eq.get); simpl.
    Storage_sigs.Non_iterable_indexed_data_storage.Op.Unfold.all.
    subst ctxt''.
    repeat Storage.auto_parse_apply.
    Storage_sigs.Indexed_data_storage.Op.Unfold.all.
    rewrite Map.find_add_eq_some; [easy|].
    apply Storage.generic_Path_encoding_Valid.
  Qed.
End Roots.

[get_mem_size ctx id] and [(state_from_id ctxt id).state.memo_size] forms an identity
[Nullifiers.size_value] and [Storage.Sapling.Nullifiers_size.add] forms an identity
Lemma nullifiers_size_value_eq
  (ctxt : Raw_context.t) (id : Storage.Sapling.id) (v : int64) :
  let ctxt' := Storage.Sapling.Nullifiers_size.(Storage_sigs.Single_data_storage.add)
     (ctxt, id) v in
  Sapling_storage.Nullifiers.size_value ctxt' id = Pervasives.Ok v.
Proof.
  simpl.
  rewrite Storage.Eq.Sapling.Nullifiers_size.eq
    .(Storage_sigs.Single_data_storage.Eq.add); simpl.
  unfold Sapling_storage.Nullifiers.size_value.
  rewrite Storage.Eq.Sapling.Nullifiers_size.eq
    .(Storage_sigs.Single_data_storage.Eq.get); simpl.
  Storage_sigs.Single_data_storage.Op.unfold_all.
  Storage.auto_parse_apply.
  now rewrite Storage.parse_apply.
Qed.

Lemma root_encoding_is_valid :
  Data_encoding.Valid.t (fun _True) Sapling_storage.root_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve root_encoding_is_valid : Data_encoding_db.

Lemma nullifiers_add_nullifiers_mem_eq
      (ctxt : Raw_context.t) (state : Sapling_storage.state)
      (nf : Sapling.Nullifier.t) :
  Nullifier.compare nf nf = 0
  let state' := Sapling_storage.nullifiers_add state nf in
  letP? '(_, result) := Sapling_storage.nullifiers_mem ctxt state' nf in
    result = true.
Proof.
  intros. simpl.
  unfold Sapling_storage.nullifiers_mem,
    Sapling_storage.nullifiers_add; simpl.
  now rewrite H.
Qed.