# 🍬 Script_interpreter_defs.v

Proofs

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.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:
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.mul_is_valid ||
(apply Saturation_repr.Valid.decide; reflexivity)
)
).
Transparent
Saturation_repr.mul
Gas_limit_repr.atomic_step_cost.

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.
sauto. sauto.
(* most of cases can be solved by sauto.
recursive cases should be solved the other way.  *)

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.