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.Environment.V7.
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)) :=
  if
    ((List.compare_length_with transaction.(Sapling.UTXO.transaction.inputs)
      5208) i 0) &&
    ((List.compare_length_with transaction.(Sapling.UTXO.transaction.outputs)
      2019) i 0)
  then
    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
  else
    Error_monad.error_value (Build_extensible "Asserted" unit tt).