🥷 Sapling_storage.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.

Require TezosOfOCaml.Environment.V8.Proofs.Sapling.

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.
  Admitted.
End Roots.

[get_mem_size ctx id] and [(state_from_id ctxt id).state.memo_size] forms an identity

Lemma state_from_id_get_memo_size_eq
  (ctxt : Raw_context.t) (id : Storage.Sapling.id) :
  letP? '(state, ctxt') := Sapling_storage.state_from_id ctxt id in
  letP? siz := Sapling_storage.get_memo_size ctxt id in
  state.(Sapling_storage.state.memo_size) = siz.
Proof.
  unfold Sapling_storage.state_from_id.
Admitted.

[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.
Admitted.

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.