Skip to main content

🥷 Sapling_storage.v


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
  Definition init_value' (ctx : Raw_context.t) (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
        let? ctx :=
            (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 :=
        (ctx, id) 0 in
    let level := (Raw_context.current_level ctx).(Level_repr.t.level) in
      (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 : :
    Roots.init_value ctxt id = init_value' ctxt id 120.
    hauto lq:on.

[Roots.get] after [init_value'] returns [Pervasives.Ok]. I had to disable guard checking because [aux] in init_value is not trivialy recursive
  Lemma init_value_get_is_ok
    (ctxt : Raw_context.t) (id : (pos : int32) :
    letP? ctxt' := init_value' ctxt id 10 in
    Pervasives.is_ok (Roots.get ctxt' id).
    unfold init_value'.
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 : (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.

Lemma root_encoding_is_valid :
  Data_encoding.Valid.t (fun _True) Sapling_storage.root_encoding.
#[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) : nf nf = 0
  let state' := Sapling_storage.nullifiers_add state nf in
  letP? '(_, result) := Sapling_storage.nullifiers_mem ctxt state' nf in
    result = true.
  intros. simpl.
  unfold Sapling_storage.nullifiers_mem,
    Sapling_storage.nullifiers_add; simpl.
  now rewrite H.