⛽ Gas_monad.v

Proofs

See code, See simulations, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Gas_monad.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Gas_monad.

The equality on the gas monad, given a custom equality on values.

Module Eq.
  Definition t {a b trace : Set} (eq : a → b → Prop)
    (x1 : Gas_monad.t a trace) (x2 : Gas_monad.t b trace) : Prop :=
    ∀ g,
    match x1 g, x2 g with
    | Some (Pervasives.Ok x1, g1), Some (Pervasives.Ok x2, g2) ⇒
      eq x1 x2 ∧ g1 = g2
    | Some (Pervasives.Error error1, g1), Some (Pervasives.Error error2, g2) ⇒
      error1 = error2 ∧ g1 = g2
    | None, None ⇒ True
    | _, _ ⇒ False
    end.
End Eq.

(* @TODO depends on dep_record_trace_eval *)
Lemma dep_record_trace_eval_eq {a : Set} {error_trace}
  (error_details : Script_tc_errors.dep_error_details error_trace
    Script_tc_errors.Error_trace_family.Error_trace)
  (f_value : error_trace → _error)
  (m_value : t a (Script_tc_errors.Error_trace_family.to_Set
    Script_tc_errors.Error_trace_family.Error_trace)) :
  dep_record_trace_eval error_details f_value m_value =
    record_trace_eval (Script_tc_errors.to_error_details error_details)
      f_value m_value.
Proof.
  (*
  unfold dep_record_trace_eval, record_trace_eval.
  simpl. dep_destruct error_details; simpl; rewrite !cast_eval; reflexivity.
  *)
Admitted.

The [run] and [map] operators can commute.

Lemma run_map {a b trace : Set} (f : a → b) (x : Gas_monad.t a trace) ctxt :
  Gas_monad.run ctxt (Gas_monad.map f x) =
  (let? '(y, ctxt) := Gas_monad.run ctxt x in
  return? (Result.map f y, ctxt)).
Proof.
  unfold
    Gas_monad.run,
    Gas_monad.map,
    Gas_monad.op_gtgtquestionquestion.
  hauto q: on.
Qed.