⛽ 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.
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.
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.
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.