⛽ Gas_input_size.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Gas_input_size.
Module Pervasives.
Lemma abs_valid (x : int) :
Pervasives.Int.Valid.t x → Pervasives.Int.Valid.t (Z.abs x).
Proof.
intros.
unfold Z.abs.
assert (Hx : x ≥ 0 ∨ x < 0) by lia.
destruct Hx as [Hx | Hx];
[now replace (BinInt.Z.abs x) with x by lia|].
replace (BinInt.Z.abs x) with (-x) by lia.
autounfold with tezos_z in ×.
apply axiom.
(* @TODO don't see why this do not hold
x : int
H : -4611686018427387904 <= x <= 4611686018427387903
Hx : x < 0
============================
-4611686018427387904 <= - x <= 4611686018427387903
*)
Qed.
End Pervasives.
(* How to state these lemmas? *)
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Gas_input_size.
Module Pervasives.
Lemma abs_valid (x : int) :
Pervasives.Int.Valid.t x → Pervasives.Int.Valid.t (Z.abs x).
Proof.
intros.
unfold Z.abs.
assert (Hx : x ≥ 0 ∨ x < 0) by lia.
destruct Hx as [Hx | Hx];
[now replace (BinInt.Z.abs x) with x by lia|].
replace (BinInt.Z.abs x) with (-x) by lia.
autounfold with tezos_z in ×.
apply axiom.
(* @TODO don't see why this do not hold
x : int
H : -4611686018427387904 <= x <= 4611686018427387903
Hx : x < 0
============================
-4611686018427387904 <= - x <= 4611686018427387903
*)
Qed.
End Pervasives.
(* How to state these lemmas? *)
[assert false] is unreachable in [Gas_input_size.set]
Lemma set_assert_unreachable {a : Set} (set : Script_typed_ir.set a) :
(* Pervasives.Int.Valid.t (Script_typed_ir.Boxed_set.size_value set) -> *)
Gas_input_size.set set = axiom.
Proof.
unfold Gas_input_size.set.
unfold Script_set.size_value.
unfold Script_int.to_int.
simpl. unfold Z.of_int.
destruct set eqn:?, s.
unfold Z.to_int.
cbn.
Abort.
(* I need Option.catch definition or axiom, also
I need to show that Z.to_
a, x : Set
b : Script_typed_ir.Boxed_set
============================
match Option.catch None (fun _ : unit => Z.to_int (abs b.(Script_typed_ir.Boxed_set.size_value))) with
| Some x_value => x_value
| None => assert t false
end = axiom
unfold Z.to_int.
*)
(* Pervasives.Int.Valid.t (Script_typed_ir.Boxed_set.size_value set) -> *)
Gas_input_size.set set = axiom.
Proof.
unfold Gas_input_size.set.
unfold Script_set.size_value.
unfold Script_int.to_int.
simpl. unfold Z.of_int.
destruct set eqn:?, s.
unfold Z.to_int.
cbn.
Abort.
(* I need Option.catch definition or axiom, also
I need to show that Z.to_
a, x : Set
b : Script_typed_ir.Boxed_set
============================
match Option.catch None (fun _ : unit => Z.to_int (abs b.(Script_typed_ir.Boxed_set.size_value))) with
| Some x_value => x_value
| None => assert t false
end = axiom
unfold Z.to_int.
*)