Skip to main content

🍬 Script_interpreter_defs.v

Proofs

See code, Gitlab , OCaml

The cost of an instruction is valid in saturated arithmetic.
Lemma cost_of_instr_is_valid {a s : Set}
  (i : Script_typed_ir.kinstr) (accu : a) (stack : s) :
  Saturation_repr.Valid.t (Script_interpreter_defs.cost_of_instr i accu stack).
Proof.
  Opaque
    Saturation_repr.add
    Saturation_repr.mul
    Gas_limit_repr.atomic_step_cost.
  destruct i eqn:?; unfold Script_interpreter_defs.cost_of_instr; simpl.
  all: repeat step.
  all: try (apply Saturation_repr.Valid.decide; reflexivity).
  all: try apply Michelson_v1_gas.Cost_of.Interpreter.compare_is_valid.
  all:
    try (grep Script_typed_ir.INever; admit).
  all: repeat (
    match goal with
    | |- Saturation_repr.Valid.t ?e
      let f := head e in
      unfold f
    end;
    try step;
    repeat (
      apply Gas_limit_repr.atomic_step_cost_is_valid ||
      apply Saturation_repr.safe_int_is_valid ||
      apply Saturation_repr.add_is_valid ||
      apply Saturation_repr.mul_is_valid ||
      (apply Saturation_repr.Valid.decide; reflexivity)
    )
  ).
  Transparent
    Saturation_repr.add
    Saturation_repr.mul
    Gas_limit_repr.atomic_step_cost.
Admitted.

The cost of an instruction is not zero, except for a few instructions.
Lemma cost_of_instr_is_not_zero
  (i : Script_typed_ir.kinstr)
  (accu stack : Stack_ty.t) :
  Script_interpreter_defs.cost_of_instr i accu stack 0.
Proof.
  destruct i.
  1 - 18 : sauto.
  admit. admit.
  sauto. sauto.
  (* most of cases can be solved by sauto.
     recursive cases should be solved the other way.  *)

Admitted.

The function [make_transaction_to_tx_rollup] is valid.
The function [make_transaction_to_sc_rollup] is valid.
The function [emit_event] is valid.
The function [transfer] is valid.
The function [create_contract] is valid.
The function [apply] returns a valid result.
The function [unpack] is valid.