🐆 Tx_rollup_gas.v

Simulations

See code, See proofs, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_gas.

Simulation version of Tx_rollup_gas.check_path_cost

Definition check_path_cost (element_size : int) (n : nat) : M? Saturation_repr.t :=
  let op_plus := Saturation_repr.add in
   let? '_ :=
    Error_monad.error_unless (0 ≤i Z.of_nat n)
      (Build_extensible "Tx_rollup_negative_input_size" unit tt) in
  let? element_hash_cost := Tx_rollup_gas.hash_cost element_size in
  let? hash_cost := Tx_rollup_gas.hash_cost 64 in
  let fix acc_hash_cost (acc_value : Saturation_repr.t) (i : nat) {struct i}
    : Saturation_repr.t :=
    match i with
    | 0%nat ⇒ acc_value
    | Datatypes.S j ⇒ acc_hash_cost (op_plus hash_cost acc_value) j
    end in
  return?
    (op_plus element_hash_cost (acc_hash_cost Tx_rollup_gas.compare_blake2b_hash n)).