🍬 Script_interpreter_defs.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_interpreter_defs.

Require TezosOfOCaml.Proto_alpha.Proofs.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_ir_translator.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

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.

Definition make_transaction_to_tx_rollup_is_valid {t : Set}
  ctxt destination amount parameters_ty parameters :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) := @Script_interpreter_defs.make_transaction_to_tx_rollup t
    ctxt destination amount parameters_ty parameters in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [make_transaction_to_sc_rollup] is valid.

Definition make_transaction_to_sc_rollup_is_valid {a : Set}
  ctxt destination amount entrypoint parameters_ty parameters :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) := @Script_interpreter_defs.make_transaction_to_sc_rollup a
    ctxt destination amount entrypoint parameters_ty parameters in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.

The function [emit_event] is valid.

Definition emit_event_is_valid {a : Set}
  function_parameter gas event_type unparsed_ty tag event_data :
  letP? '(_, _, _) := @Script_interpreter_defs.emit_event a
    function_parameter gas event_type unparsed_ty tag event_data in
  True.
Proof.
Admitted.

The function [transfer] is valid.

Definition transfer_is_valid {a : Set}
  function_parameter gas amount location typed_contract parameters :
  letP? '(_, _, _) := @Script_interpreter_defs.transfer a
    function_parameter gas amount location typed_contract parameters in
  True.
Proof.
Admitted.

The function [create_contract] is valid.

Definition create_contract_is_valid {a : Set}
  function_parameter gas storage_type code delegate credit init_value :
  letP? '(_, _, _, _) := @Script_interpreter_defs.create_contract a
    function_parameter gas storage_type code delegate credit init_value in
  True.
Proof.
Admitted.

The function [apply] returns a valid result.

Lemma apply_is_valid {a c d : Ty.t}
  (ctxt ctxt' : Local_gas_counter.outdated_context)
  (gas gas' : Local_gas_counter.local_gas_counter)
  capture_ty (capture : Ty.to_Set a)
  (lam : Script_typed_ir.lambda)
  (lam' : Script_typed_ir.lambda) :
  Script_typed_ir.ty.Valid.proj_rel a capture_ty →
  Script_typed_ir.Valid.value a capture →
  Script_typed_ir.Valid.lambda [Ty.Pair a c] [d] lam →
  Script_interpreter_defs.apply ctxt gas capture_ty capture lam =
    return? (lam', ctxt', gas') →
  Script_typed_ir.Valid.lambda [c] [d] lam'.
Proof.
Admitted.

The function [unpack] is valid.

Definition unpack_is_valid {a : Set}
  ctxt ty bytes_value :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) := @Script_interpreter_defs.unpack a
    ctxt ty bytes_value in
  Raw_context.Valid.t ctxt.
Proof.
Admitted.