Skip to main content

🥷 Sapling_validator.v

Translated OCaml

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.Raw_context.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.

Fixpoint check_and_update_nullifiers
  (ctxt : Raw_context.t) (state_value : Sapling_storage.state)
  (inputs : list Sapling.UTXO.input)
  : M? (Raw_context.t × option Sapling_storage.state) :=
  match inputs with
  | []return? (ctxt, (Some state_value))
  | cons input inputs
    let? function_parameter :=
      Sapling_storage.nullifiers_mem ctxt state_value
        input.(Sapling.UTXO.input.nf) in
    match function_parameter with
    | (ctxt, true)return? (ctxt, None)
    | (ctxt, false)
      let state_value :=
        Sapling_storage.nullifiers_add state_value input.(Sapling.UTXO.input.nf)
        in
      check_and_update_nullifiers ctxt state_value inputs
    end
  end.

Definition verify_update
  (ctxt : Raw_context.t) (state_value : Sapling_storage.state)
  (transaction : Sapling_repr.transaction) (key_value : string)
  : M? (Raw_context.t × option (Int64.t × Sapling_storage.state)) :=
  let '_ :=
    (* ❌ Assert instruction is not handled. *)
    assert unit
      ((List.compare_length_with transaction.(Sapling.UTXO.transaction.inputs)
        5208) i 0) in
  let '_ :=
    (* ❌ Assert instruction is not handled. *)
    assert unit
      ((List.compare_length_with transaction.(Sapling.UTXO.transaction.outputs)
        2019) i 0) in
  let pass :=
    List.for_all
      (fun (output : Sapling.UTXO.output) ⇒
        (Sapling.Ciphertext.get_memo_size
          output.(Sapling.UTXO.output.ciphertext)) =i
        state_value.(Sapling_storage.state.memo_size))
      transaction.(Sapling.UTXO.transaction.outputs) in
  if Pervasives.not pass then
    return? (ctxt, None)
  else
    let? pass :=
      Sapling_storage.root_mem ctxt state_value
        transaction.(Sapling.UTXO.transaction.root) in
    if Pervasives.not pass then
      return? (ctxt, None)
    else
      let? function_parameter :=
        check_and_update_nullifiers ctxt state_value
          transaction.(Sapling.UTXO.transaction.inputs) in
      match function_parameter with
      | (ctxt, None)return? (ctxt, None)
      | (ctxt, Some state_value)
        return?
          (Sapling.Verification.with_verification_ctx
            (fun (vctx : Sapling.Verification.t) ⇒
              let pass :=
                List.for_all
                  (fun (output : Sapling.UTXO.output) ⇒
                    Sapling.Verification.check_output vctx output)
                  transaction.(Sapling.UTXO.transaction.outputs) in
              if Pervasives.not pass then
                (ctxt, None)
              else
                let pass :=
                  List.for_all
                    (fun (input : Sapling.UTXO.input) ⇒
                      Sapling.Verification.check_spend vctx input
                        transaction.(Sapling.UTXO.transaction.root) key_value)
                    transaction.(Sapling.UTXO.transaction.inputs) in
                if Pervasives.not pass then
                  (ctxt, None)
                else
                  let pass :=
                    Sapling.Verification.final_check vctx transaction key_value
                    in
                  if Pervasives.not pass then
                    (ctxt, None)
                  else
                    let list_to_add :=
                      List.map
                        (fun (output : Sapling.UTXO.output) ⇒
                          (output.(Sapling.UTXO.output.cm),
                            output.(Sapling.UTXO.output.ciphertext)))
                        transaction.(Sapling.UTXO.transaction.outputs) in
                    let state_value :=
                      Sapling_storage.add state_value list_to_add in
                    (ctxt,
                      (Some
                        (transaction.(Sapling.UTXO.transaction.balance),
                          state_value)))))
      end.