Skip to main content

⛽ Gas_input_size.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.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.
 *)