Skip to main content

🥷 Sapling_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Module COMMITMENTS.
  Record signature : Set := {
    init_value : Raw_context.t Storage.Sapling.id Raw_context.t;
    default_root : Sapling.Hash.t;
    get_root :
      Raw_context.t Storage.Sapling.id M? (Raw_context.t × Sapling.Hash.t);
    add :
      Raw_context.t Storage.Sapling.id list Sapling.Commitment.t
      int64 M? (Raw_context.t × int);
    get_from :
      Raw_context.t Storage.Sapling.id int64
      M? (list Sapling.Commitment.t);
  }.
End COMMITMENTS.
Definition COMMITMENTS := COMMITMENTS.signature.

Module Commitments.
  Module H := Sapling.Hash.

  Definition pow2 (h_value : int) : int64 := Int64.shift_left 1 h_value.

  Definition max_height : int := 32.

  Definition max_size : int64 := pow2 max_height.

  Definition assert_node (node_value : int64) (height : int) : unit :=
    (* ❌ Assert instruction is not handled. *)
    assert unit
      (let first_of_height := pow2 (max_height -i height) in
      let first_of_next_height := Int64.shift_left first_of_height 1 in
      (node_value i64 first_of_height) &&
      (node_value <i64 first_of_next_height)).

  Definition assert_height (height : int) : unit :=
    (* ❌ Assert instruction is not handled. *)
    assert unit ((height i 0) && (height i max_height)).

  Definition assert_pos (pos : int64) (height : int) : unit :=
    (* ❌ Assert instruction is not handled. *)
    assert unit ((pos i64 0) && (pos i64 (pow2 height))).

  Definition default_root : H.t := H.uncommitted max_height.

  Definition init_value
    : Raw_context.t Storage.Sapling.id Raw_context.t :=
    Storage.Sapling.commitments_init.

  Definition get_root_height
    (ctx : Raw_context.t) (id : Storage.Sapling.id) (node_value : int64)
    (height : int) : M? (Raw_context.t × H.t) :=
    let '_ := assert_node node_value height in
    let '_ := assert_height height in
    let? function_parameter :=
      Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
        (ctx, id) node_value in
    match function_parameter with
    | (ctx, None)
      let hash_value := H.uncommitted height in
      return? (ctx, hash_value)
    | (ctx, Some hash_value)return? (ctx, hash_value)
    end.

  Definition _left (node_value : int64) : int64 := node_value ×i64 2.

  Definition _right (node_value : int64) : int64 := (node_value ×i64 2) +i64 1.

  Fixpoint split_at {A : Set} (n_value : int64) (l_value : list A)
    : list A × list A :=
    if n_value =i64 0 then
      (nil, l_value)
    else
      match l_value with
      | [](nil, l_value)
      | cons x_value xs
        let '(l1, l2) := split_at (Int64.pred n_value) xs in
        ((cons x_value l1), l2)
      end.

  #[bypass_check(guard)]
  Fixpoint insert
    (ctx : Raw_context.t) (id : Storage.Sapling.id) (node_value : int64)
    (height : int) (pos : int64) (cms : list Sapling.Commitment.t)
    {struct height} : M? (Raw_context.t × int × H.t) :=
    let '_ := assert_node node_value height in
    let '_ := assert_height height in
    let '_ := assert_pos pos height in
    match (height, cms) with
    | (_, [])
      let? '(ctx, h_value) := get_root_height ctx id node_value height in
      return? (ctx, 0, h_value)
    | (0, cons cm [])
      let h_value := H.of_commitment cm in
      let? '(ctx, size_value) :=
        Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
          (ctx, id) node_value h_value in
      return? (ctx, size_value, h_value)
    | _
      let height := height -i 1 in
      let? '(ctx, size_children, hl, hr) :=
        if pos <i64 (pow2 height) then
          let _at := (pow2 height) -i64 pos in
          let '(cml, cmr) := split_at _at cms in
          let? '(ctx, size_l, hl) :=
            insert ctx id (_left node_value) height pos cml in
          let? '(ctx, size_r, hr) :=
            insert ctx id (_right node_value) height 0 cmr in
          return? (ctx, (size_l +i size_r), hl, hr)
        else
          let? '(ctx, hl) := get_root_height ctx id (_left node_value) height in
          let pos := pos -i64 (pow2 height) in
          let? '(ctx, size_r, hr) :=
            insert ctx id (_right node_value) height pos cms in
          return? (ctx, size_r, hl, hr) in
      let h_value := H.merkle_hash height hl hr in
      let? '(ctx, size_value, _existing) :=
        Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
          (ctx, id) node_value h_value in
      return? (ctx, (size_value +i size_children), h_value)
    end.

  #[bypass_check(guard)]
  Fixpoint fold_from_height {A : Set}
    (ctx : Raw_context.t) (id : Storage.Sapling.id) (node_value : int64)
    (pos : int64) (f_value : A Sapling.Hash.t A) (acc_value : A)
    (height : int) {struct height} : M? A :=
    let '_ := assert_node node_value height in
    let '_ := assert_height height in
    let '_ := assert_pos pos height in
    let? function_parameter :=
      Storage.Sapling.Commitments.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
        (ctx, id) node_value in
    match function_parameter with
    | (_ctx, None)return? acc_value
    | (_ctx, Some h_value)
      if height =i 0 then
        return? (f_value acc_value h_value)
      else
        let full_value := pow2 (height -i 1) in
        if pos <i64 full_value then
          let? acc_value :=
            fold_from_height ctx id (_left node_value) pos f_value acc_value
              (height -i 1) in
          fold_from_height ctx id (_right node_value) 0 f_value acc_value
            (height -i 1)
        else
          let pos := pos -i64 full_value in
          fold_from_height ctx id (_right node_value) pos f_value acc_value
            (height -i 1)
    end.

  Definition root_node : int64 := 1.

  Definition get_root (ctx : Raw_context.t) (id : Storage.Sapling.id)
    : M? (Raw_context.t × H.t) := get_root_height ctx id root_node max_height.

  Definition add
    (ctx : Raw_context.t) (id : Storage.Sapling.id)
    (cms : list Sapling.Commitment.t) (pos : int64)
    : M? (Raw_context.t × int) :=
    let l_value := List.length cms in
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit (l_value i 1000) in
    let n' := pos +i64 (Int64.of_int l_value) in
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit (n' i64 max_size) in
    let? '(ctx, size_value, _h) := insert ctx id root_node max_height pos cms in
    return? (ctx, size_value).

  Definition get_from
    (ctx : Raw_context.t) (id : Storage.Sapling.id) (pos : int64)
    : M? (list Sapling.Commitment.t) :=
    let? l_value :=
      fold_from_height ctx id root_node pos
        (fun (acc_value : list Sapling.Commitment.t) ⇒
          fun (c_value : Sapling.Hash.t) ⇒
            cons (H.to_commitment c_value) acc_value) nil max_height in
    return? (List.rev l_value).

  (* Commitments *)
  Definition module :=
    {|
      COMMITMENTS.init_value := init_value;
      COMMITMENTS.default_root := default_root;
      COMMITMENTS.get_root := get_root;
      COMMITMENTS.add := add;
      COMMITMENTS.get_from := get_from
    |}.
End Commitments.
Definition Commitments : COMMITMENTS := Commitments.module.

Module Ciphertexts.
  Definition init_value (ctx : Raw_context.t) (id : Storage.Sapling.id)
    : Raw_context.t := Storage.Sapling.ciphertexts_init ctx id.

  Definition add
    (ctx : Raw_context.t) (id : Storage.Sapling.id)
    (c_value : Sapling.Ciphertext.t) (pos : int64) : M? (Raw_context.t × int) :=
    Storage.Sapling.Ciphertexts.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      (ctx, id) pos c_value.

  #[bypass_check(guard)]
  Definition get_from
    (ctx : Raw_context.t) (id : Storage.Sapling.id) (offset : int64)
    : M? (Raw_context.t × list Sapling.Ciphertext.t) :=
    let fix aux (function_parameter : Raw_context.t × list Sapling.Ciphertext.t)
      {struct function_parameter}
      : int64 M? (Raw_context.t × list Sapling.Ciphertext.t) :=
      let '(ctx, acc_value) := function_parameter in
      fun (pos : int64) ⇒
        let? '(ctx, c_value) :=
          Storage.Sapling.Ciphertexts.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
            (ctx, id) pos in
        match c_value with
        | Nonereturn? (ctx, (List.rev acc_value))
        | Some c_valueaux (ctx, (cons c_value acc_value)) (Int64.succ pos)
        end in
    aux (ctx, nil) offset.
End Ciphertexts.

Module Nullifiers.
  Definition init_value
    : Raw_context.t Storage.Sapling.id Raw_context.t :=
    Storage.Sapling.nullifiers_init.

  Definition size_value (ctx : Raw_context.t) (id : Storage.Sapling.id)
    : M? int64 :=
    Storage.Sapling.Nullifiers_size.(Storage_sigs.Single_data_storage.get)
      (ctx, id).

  Definition mem
    (ctx : Raw_context.t) (id : Storage.Sapling.id) (nf : Sapling.Nullifier.t)
    : M? (Raw_context.t × bool) :=
    Storage.Sapling.Nullifiers_hashed.(Storage_sigs.Carbonated_data_set_storage.mem)
      (ctx, id) nf.

  Definition add
    (ctx : Raw_context.t) (id : Storage.Sapling.id)
    (nfs : list Sapling.Nullifier.t) : M? (Raw_context.t × Z.t) :=
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit ((List.compare_length_with nfs 1000) i 0) in
    let? nf_start_pos := size_value ctx id in
    let? '(ctx, nf_end_pos, size_value) :=
      List.fold_right_es
        (fun (nf : Sapling.Nullifier.t) ⇒
          fun (function_parameter : Raw_context.t × int64 × Z.t) ⇒
            let '(ctx, pos, acc_size) := function_parameter in
            let? '(ctx, size_value) :=
              Storage.Sapling.Nullifiers_hashed.(Storage_sigs.Carbonated_data_set_storage.init_value)
                (ctx, id) nf in
            let? ctx :=
              Storage.Sapling.Nullifiers_ordered.(Storage_sigs.Non_iterable_indexed_data_storage.init_value)
                (ctx, id) pos nf in
            return? (ctx, (Int64.succ pos), (acc_size +Z (Z.of_int size_value))))
        nfs (ctx, nf_start_pos, Z.zero) in
    let? ctx :=
      Storage.Sapling.Nullifiers_size.(Storage_sigs.Single_data_storage.update)
        (ctx, id) nf_end_pos in
    return? (ctx, size_value).

  #[bypass_check(guard)]
  Definition get_from
    (ctx : Raw_context.t) (id : Storage.Sapling.id) (offset : int64)
    : M? (list Sapling.Nullifier.t) :=
    let fix aux (acc_value : list Sapling.Nullifier.t) (pos : int64)
      {struct pos} : M? (list Sapling.Nullifier.t) :=
      let? function_parameter :=
        Storage.Sapling.Nullifiers_ordered.(Storage_sigs.Non_iterable_indexed_data_storage.find)
          (ctx, id) pos in
      match function_parameter with
      | Nonereturn? (List.rev acc_value)
      | Some c_valueaux (cons c_value acc_value) (Int64.succ pos)
      end in
    aux nil offset.
End Nullifiers.

Bounded queue of roots. The full size is initialized with the default uncommitted root, that's why roots storage doesn't need to be carbonated. A maximum of one new root is added per protocol level. If multiple transactions for the same shielded pool are processed during the same contract call or several calls in the same block, only the last root will be stored. This property prevents transactions in the same block from depending on each other and guarantees that a transaction will be valid for a least two hours (hence the 120 size) after being forged.
Module Roots.
  Definition size_value : int32 := 120.

  Definition get (ctx : Raw_context.t) (id : Storage.Sapling.id)
    : M? Sapling.Hash.t :=
    let? pos :=
      Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.get) (ctx, id)
      in
    Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.get)
      (ctx, id) pos.

  #[bypass_check(guard)]
  Definition init_value (ctx : Raw_context.t) (id : Storage.Sapling.id)
    : 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.

  #[bypass_check(guard)]
  Definition mem
    (ctx : Raw_context.t) (id : Storage.Sapling.id)
    (root_value : Sapling.Hash.t) : M? bool :=
    let? start_pos :=
      Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.get) (ctx, id)
      in
    let fix aux (pos : int32) {struct pos} : M? bool :=
      let? hash_value :=
        Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.get)
          (ctx, id) pos in
      if (Sapling.Hash.compare hash_value root_value) =i 0 then
        return? true
      else
        let pos := Int32.pred pos in
        let pos :=
          if pos <i32 0 then
            Int32.pred size_value
          else
            pos in
        if pos =i32 start_pos then
          return? false
        else
          aux pos in
    aux start_pos.

  Definition add
    (ctx : Raw_context.t) (id : Storage.Sapling.id)
    (root_value : Sapling.Hash.t) : M? Raw_context.t :=
    let? pos :=
      Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.get) (ctx, id)
      in
    let level := (Raw_context.current_level ctx).(Level_repr.t.level) in
    let? stored_level :=
      Storage.Sapling.Roots_level.(Storage_sigs.Single_data_storage.get)
        (ctx, id) in
    if Raw_level_repr.op_eq stored_level level then
      Error_monad.op_gtpipeeq
        (Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.add)
          (ctx, id) pos root_value) Error_monad.ok
    else
      let? ctx :=
        Storage.Sapling.Roots_level.(Storage_sigs.Single_data_storage.update)
          (ctx, id) level in
      let pos := Int32.rem (Int32.succ pos) size_value in
      let? ctx :=
        Storage.Sapling.Roots_pos.(Storage_sigs.Single_data_storage.update)
          (ctx, id) pos in
      Error_monad.op_gtpipeeq
        (Storage.Sapling.Roots.(Storage_sigs.Non_iterable_indexed_data_storage.add)
          (ctx, id) pos root_value) Error_monad.ok.
End Roots.

This type links the permanent state stored in the context at the specified id together with the ephemeral diff managed by the Michelson interpreter. After a successful execution the diff can be applied to update the state at id. The first time a state is created its id is None, one will be assigned after the first application.
Module state.
  Record record : Set := Build {
    id : option Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t);
    diff : Sapling_repr.diff;
    memo_size : Sapling_repr.Memo_size.t;
  }.
  Definition with_id id (r : record) :=
    Build id r.(diff) r.(memo_size).
  Definition with_diff diff (r : record) :=
    Build r.(id) diff r.(memo_size).
  Definition with_memo_size memo_size (r : record) :=
    Build r.(id) r.(diff) memo_size.
End state.
Definition state := state.record.

Definition empty_diff : Sapling_repr.diff :=
  {| Sapling_repr.diff.commitments_and_ciphertexts := nil;
    Sapling_repr.diff.nullifiers := nil; |}.

Definition empty_state
  (id : option Lazy_storage_kind.Sapling_state.Id.(Lazy_storage_kind.ID.t))
  (memo_size : Sapling_repr.Memo_size.t) (function_parameter : unit) : state :=
  let '_ := function_parameter in
  {| state.id := id; state.diff := empty_diff; state.memo_size := memo_size; |}.

Returns a state from an existing id.
Definition state_from_id (ctxt : Raw_context.t) (id : Storage.Sapling.id)
  : M? (state × Raw_context.t) :=
  let? memo_size :=
    Storage.Sapling.Memo_size.(Storage_sigs.Single_data_storage.get) (ctxt, id)
    in
  return?
    ({| state.id := Some id; state.diff := empty_diff;
      state.memo_size := memo_size; |}, ctxt).

Definition rpc_arg : RPC_arg.t Storage.Sapling.id := Storage.Sapling.rpc_arg.

Definition get_memo_size (ctx : Raw_context.t) (id : Storage.Sapling.id)
  : M? int :=
  Storage.Sapling.Memo_size.(Storage_sigs.Single_data_storage.get) (ctx, id).

Definition init_value
  (ctx : Raw_context.t) (id : Storage.Sapling.id) (memo_size : int)
  : M? Raw_context.t :=
  let ctx :=
    Storage.Sapling.Memo_size.(Storage_sigs.Single_data_storage.add) (ctx, id)
      memo_size in
  let ctx :=
    Storage.Sapling.Commitments_size.(Storage_sigs.Single_data_storage.add)
      (ctx, id) Int64.zero in
  let ctx := Commitments.(COMMITMENTS.init_value) ctx id in
  let ctx := Nullifiers.init_value ctx id in
  let? ctx := Roots.init_value ctx id in
  Error_monad.op_gtpipeeq (Ciphertexts.init_value ctx id) Error_monad.ok.

Definition sapling_apply_diff_cost (inputs : int) (outputs : int)
  : Saturation_repr.t :=
  Saturation_repr.add (Saturation_repr.safe_int 1300000)
    (Saturation_repr.add
      (Saturation_repr.scale_fast (Saturation_repr.mul_safe_of_int_exn 5000)
        (Saturation_repr.safe_int inputs))
      (Saturation_repr.scale_fast (Saturation_repr.mul_safe_of_int_exn 55000)
        (Saturation_repr.safe_int outputs))).

Applies a diff to a state id stored in the context. Updates Commitments, Ciphertexts and Nullifiers using the diff and updates the Roots using the new Commitments tree.
Definition apply_diff
  (ctx : Raw_context.t) (id : Storage.Sapling.id)
  (diff_value : Sapling_repr.diff) : M? (Raw_context.t × Z.t) :=
  let nb_commitments :=
    List.length diff_value.(Sapling_repr.diff.commitments_and_ciphertexts) in
  let nb_nullifiers := List.length diff_value.(Sapling_repr.diff.nullifiers) in
  let sapling_cost := sapling_apply_diff_cost nb_nullifiers nb_commitments in
  let? ctx := Raw_context.consume_gas ctx sapling_cost in
  let? cm_start_pos :=
    Storage.Sapling.Commitments_size.(Storage_sigs.Single_data_storage.get)
      (ctx, id) in
  let cms :=
    List.rev_map Pervasives.fst
      diff_value.(Sapling_repr.diff.commitments_and_ciphertexts) in
  let? '(ctx, size_value) :=
    Commitments.(COMMITMENTS.add) ctx id cms cm_start_pos in
  let? ctx :=
    Storage.Sapling.Commitments_size.(Storage_sigs.Single_data_storage.update)
      (ctx, id) (cm_start_pos +i64 (Int64.of_int nb_commitments)) in
  let? '(ctx, _ct_end_pos, size_value) :=
    List.fold_right_es
      (fun (function_parameter : Sapling.Commitment.t × Sapling.Ciphertext.t) ⇒
        let '(_cm, cp) := function_parameter in
        fun (function_parameter : Raw_context.t × int64 × Z.t) ⇒
          let '(ctx, pos, acc_size) := function_parameter in
          let? '(ctx, size_value) := Ciphertexts.add ctx id cp pos in
          return? (ctx, (Int64.succ pos), (acc_size +Z (Z.of_int size_value))))
      diff_value.(Sapling_repr.diff.commitments_and_ciphertexts)
      (ctx, cm_start_pos, (Z.of_int size_value)) in
  let? '(ctx, size_nf) :=
    Nullifiers.add ctx id diff_value.(Sapling_repr.diff.nullifiers) in
  let size_value := size_value +Z size_nf in
  match diff_value.(Sapling_repr.diff.commitments_and_ciphertexts) with
  | []return? (ctx, size_value)
  | cons _ _
    let? '(ctx, root_value) := Commitments.(COMMITMENTS.get_root) ctx id in
    let? ctx := Roots.add ctx id root_value in
    return? (ctx, size_value)
  end.

Definition add (function_parameter : state)
  : list (Sapling.Commitment.t × Sapling.Ciphertext.t) state :=
  let '{|
    state.id := id;
      state.diff := diff_value;
      state.memo_size := memo_size
      |} := function_parameter in
  fun (cm_cipher_list : list (Sapling.Commitment.t × Sapling.Ciphertext.t)) ⇒
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit
        (List.for_all
          (fun (function_parameter :
            Sapling.Commitment.t × Sapling.Ciphertext.t) ⇒
            let '(_cm, cipher) := function_parameter in
            (Sapling.Ciphertext.get_memo_size cipher) =i memo_size)
          cm_cipher_list) in
    {| state.id := id;
      state.diff :=
        Sapling_repr.diff.with_commitments_and_ciphertexts
          (Pervasives.op_at (List.rev cm_cipher_list)
            diff_value.(Sapling_repr.diff.commitments_and_ciphertexts))
          diff_value; state.memo_size := memo_size; |}.

Definition root_mem (ctx : Raw_context.t) (function_parameter : state)
  : Sapling.Hash.t M? bool :=
  let '{| state.id := id |} := function_parameter in
  fun (tested_root : Sapling.Hash.t) ⇒
    match id with
    | Some idRoots.mem ctx id tested_root
    | None
      return?
        ((Sapling.Hash.compare tested_root
          Commitments.(COMMITMENTS.default_root)) =i 0)
    end.

Definition nullifiers_mem (ctx : Raw_context.t) (function_parameter : state)
  : Sapling.Nullifier.t M? (Raw_context.t × bool) :=
  let '{| state.id := id; state.diff := diff_value |} := function_parameter in
  fun (nf : Sapling.Nullifier.t) ⇒
    let exists_in_diff :=
      List._exists
        (fun (v_value : Sapling.Nullifier.t) ⇒
          (Sapling.Nullifier.compare nf v_value) =i 0)
        diff_value.(Sapling_repr.diff.nullifiers) in
    if exists_in_diff then
      return? (ctx, true)
    else
      match id with
      | Nonereturn? (ctx, false)
      | Some idNullifiers.mem ctx id nf
      end.

Definition nullifiers_add (function_parameter : state)
  : Sapling.Nullifier.t state :=
  let '{|
    state.id := id;
      state.diff := diff_value;
      state.memo_size := memo_size
      |} := function_parameter in
  fun (nf : Sapling.Nullifier.t) ⇒
    {| state.id := id;
      state.diff :=
        Sapling_repr.diff.with_nullifiers
          (cons nf diff_value.(Sapling_repr.diff.nullifiers)) diff_value;
      state.memo_size := memo_size; |}.

Definition root : Set := Sapling.Hash.t.

Definition root_encoding : Data_encoding.t Sapling.Hash.t :=
  Sapling.Hash.encoding.

Definition get_diff
  (ctx : Raw_context.t) (id : Storage.Sapling.id)
  (op_staroptstar : option int64)
  : option int64 unit M? (Sapling.Hash.t × Sapling_repr.diff) :=
  let offset_commitment :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | None ⇒ 0
    end in
  fun (op_staroptstar : option int64) ⇒
    let offset_nullifier :=
      match op_staroptstar with
      | Some op_starsthstarop_starsthstar
      | None ⇒ 0
      end in
    fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      if
        Pervasives.not
          ((Sapling.Commitment.valid_position offset_commitment) &&
          (Sapling.Commitment.valid_position offset_nullifier))
      then
        Pervasives.failwith "Invalid argument."
      else
        let? commitments :=
          Commitments.(COMMITMENTS.get_from) ctx id offset_commitment in
        let? root_value := Roots.get ctx id in
        let? nullifiers := Nullifiers.get_from ctx id offset_nullifier in
        let? '(_ctx, ciphertexts) :=
          Ciphertexts.get_from ctx id offset_commitment in
        match List.combine tt commitments ciphertexts with
        | Pervasives.Error _
          return? (Pervasives.failwith "Invalid argument.")
        | Pervasives.Ok commitments_and_ciphertexts
          return?
            (root_value,
              {|
                Sapling_repr.diff.commitments_and_ciphertexts :=
                  commitments_and_ciphertexts;
                Sapling_repr.diff.nullifiers := nullifiers; |})
        end.