🍃 Pervasives.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.

Require Import TezosOfOCaml.Environment.V8.Proofs.Utils.

The [raise] instruction propagates in [let] constructs.

Axiom raise_let : ∀ {a b : Set} (exn : extensible_type) (f : a → b),
  (let x := Pervasives.raise exn in
  f x) =
  Pervasives.raise exn.

Definition is_ok {v : Set} (x : M? v) : Prop :=
  match x with
  | Pervasives.Ok _ ⇒ True
  | Pervasives.Error _ ⇒ False
  end.

normalize preserves values between min and max

Module Int.
  Module Valid.
    Definition t (x : int) : Prop :=
      Pervasives.min_int ≤ x ≤ Pervasives.max_int.
    #[global] Hint Unfold t : tezos_z.

    Definition positive (x : int) : Prop :=
      0 < x ≤ Pervasives.max_int.

    Definition non_negative (x : int) : Prop :=
      0 ≤ x ≤ Pervasives.max_int.

    #[global] Hint Unfold non_negative positive : tezos_z.

    Lemma int_plus_0_r_eq : ∀ {i : int},
        t i → i +i 0 = i.
    Proof.
      lia.
    Qed.

A valid non-negative int is valid

    Lemma valid_non_negative_implies_valid : ∀ (x : int),
      non_negative x → t x.
    Proof.
      lia.
    Qed.
  End Valid.
End Int.

Lemma normalize_identity : ∀ {x : int},
  Int.Valid.t x → Pervasives.normalize_int x = x.
Proof.
  lia.
Qed.

normalize never exceeds its boundaries

Lemma normalize_never_exceeds : ∀ {x : int},
  Int.Valid.t (Pervasives.normalize_int x).
Proof.
  lia.
Qed.

Lemma normalize_int_idemp : ∀ x,
  normalize_int (normalize_int x) = normalize_int x.
Proof.
  lia.
Qed.

Lemma int_mul_valid : ∀ {x y}, Pervasives.Int.Valid.t (x ×i y).
Proof.
  lia.
Qed.

Lemma int_add_valid : ∀ {x y}, Pervasives.Int.Valid.t (x +i y).
Proof.
  lia.
Qed.

Lemma int_add_assoc a b c : a +i b +i c = a +i (b +i c).
Proof.
  lia.
Qed.

Tests to ensure that some operations are well-defined and compatible with

their OCaml counterparts.

Lemma land_test : List.Forall (fun '(n, m, r) ⇒ Pervasives.land n m = r) [
  (0, 0, 0);
  (1, 0, 0);
  (0, 1, 0);
  (1, 1, 1);
  (2, 1, 0);
  (2, 10, 2);
  (-1, 9, 9);
  (-2, 9, 8);
  (-1, -1, -1)
].
  repeat constructor.
Qed.

Lemma lor_test : List.Forall (fun '(n, m, r) ⇒ Pervasives.lor n m = r) [
  (0, 0, 0);
  (1, 0, 1);
  (0, 1, 1);
  (1, 1, 1);
  (2, 1, 3);
  (2, 10, 10);
  (-1, 9, -1);
  (-2, 9, -1);
  (-1, -1, -1)
].
  repeat constructor.
Qed.

Lemma lxor_test : List.Forall (fun '(n, m, r) ⇒ Pervasives.lxor n m = r) [
  (0, 0, 0);
  (1, 0, 1);
  (0, 1, 1);
  (1, 1, 0);
  (2, 1, 3);
  (2, 10, 8);
  (-1, 9, -10);
  (-2, 9, -9);
  (-1, -1, 0)
].
  repeat constructor.
Qed.

Lemma lnot_test : List.Forall (fun '(n, r) ⇒ Pervasives.lnot n = r) [
  (0, -1);
  (1, -2);
  (2, -3);
  (-1, 0);
  (-2, 1)
].
  repeat constructor.
Qed.

Lemma lsl_test : List.Forall (fun '(n, m, r) ⇒ Pervasives.lsl n m = r) [
  (0, 0, 0);
  (9, 0, 9);
  (0, 1, 0);
  (1, 1, 2);
  (2, 2, 8);
  (2, 10, 2048);
  (-1, 9, -512);
  (-2, 9, -1024);
  (Pervasives.max_int, 2, -4)
].
  repeat constructor.
Qed.

Lemma lsr_test : List.Forall (fun '(n, m, r) ⇒ Pervasives.lsr n m = r) [
  (0, 0, 0);
  (9, 0, 9);
  (0, 1, 0);
  (1, 1, 0);
  (2, 2, 0);
  (10, 1, 5);
  (10, 2, 2);
  (2048, 10, 2);
  (-1, 1, 4611686018427387903);
  (-2, 3, 1152921504606846975)
].
  repeat constructor.
Qed.

Lemma asr_test : List.Forall (fun '(n, m, r) ⇒ Pervasives.asr n m = r) [
  (0, 0, 0);
  (9, 0, 9);
  (0, 1, 0);
  (1, 1, 0);
  (2, 2, 0);
  (10, 1, 5);
  (10, 2, 2);
  (2048, 10, 2);
  (-1, 1, -1);
  (-200, 3, -25)
].
  repeat constructor.
Qed.

Validity predicates for other integer types implemented using 'int'

Module Int8.
  Definition min : int := -128.

  Definition max : int := 127.

  Module Valid.
    Definition t (i : int) : Prop :=
      min ≤ i ≤ max.
  End Valid.
End Int8.

Module UInt8.
  Definition min : int := 0.

  Definition max : int := 255.

  Module Valid.
    Definition t (i : int) : Prop :=
      min ≤ i ≤ max.

    Definition positive (i : int) : Prop :=
      min < i ≤ max.
  End Valid.
End UInt8.

Module Int16.
  Definition min : int := -32768.

  Definition max : int := 32767.

  Module Valid.
    Definition t (i : int) : Prop :=
      min ≤ i ≤ max.
  End Valid.
End Int16.

Module UInt16.
  Definition min : int := 0.

  Definition max : int := 65535.

  Module Valid.
    Definition t (i : int) : Prop :=
      min ≤ i ≤ max.
  End Valid.
End UInt16.

Module Int31.
  Definition min : int := -1073741824.

  Definition max : int := 1073741823.

  Module Valid.
    Definition t (i : int) : Prop :=
      min ≤ i ≤ max.

    Definition positive (i : int) : Prop :=
      0 < i ≤ max.

    Definition non_negative (i : int) : Prop :=
      0 ≤ i ≤ max.
  End Valid.
End Int31.

Global Hint Unfold
  Int8.min
  Int8.max
  Int8.Valid.t
  UInt8.min
  UInt8.max
  UInt8.Valid.t
  UInt8.Valid.positive
  Int16.min
  Int16.max
  Int16.Valid.t
  UInt16.min
  UInt16.max
  UInt16.Valid.t
  Int31.min
  Int31.max
  Int31.Valid.t
  Int31.Valid.positive
  Int31.Valid.non_negative
  : tezos_z.

Axiom int_of_string_opt_is_valid : ∀ (s : string),
  match int_of_string_opt s with
  | Some n ⇒ Int.Valid.t n
  | None ⇒ True
  end.

Axiom int_of_string_opt_string_of_int : ∀ (n : int),
  Int.Valid.t n →
  Pervasives.int_of_string_opt (Pervasives.string_of_int n) = Some n.

Axiom string_of_int_int_of_string_opt : ∀ (s : string),
  match Pervasives.int_of_string_opt s with
  | Some n ⇒ Pervasives.string_of_int n = s
  | None ⇒ True
  end.