Skip to main content

🍃 Z.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.Int32.
Require TezosOfOCaml.Environment.V7.Proofs.Int64.

Lemma compare_is_valid
  : Proofs.Compare.Valid.t (fun _True) id Z.compare.
Proof.
  exact Compare.z_is_valid.
Qed.

When in bounds, the conversion to [int] is the identity.
Lemma to_int_eq (z : Z.t) :
  Pervasives.Int.Valid.t z
  Z.to_int z = z.
Proof.
  intros.
  unfold Z.to_int.
  do 2 (destruct (_ <=? _) eqn:? in |- *); simpl;
    try reflexivity;
    lia.
Qed.

When in bounds, the conversion to [int32] is the identity.
Lemma to_int32_eq (z : Z.t) :
  Int32.Valid.t z
  Z.to_int32 z = z.
Proof.
  intros.
  unfold Z.to_int32.
  do 2 (destruct (_ <=? _) eqn:? in |- *); simpl;
    try reflexivity;
    lia.
Qed.

When in bounds, the conversion to [int64] is the identity.
Lemma to_int64_eq (z : Z.t) :
  Int64.Valid.t z
  Z.to_int64 z = z.
Proof.
  intros.
  unfold Z.to_int64.
  do 2 (destruct (_ <=? _) eqn:? in |- *); simpl;
    try reflexivity;
    lia.
Qed.

Axiom to_string_of_string_eq : s,
  to_string (of_string s) = s.

[shift_left a b] is positive if [a] is positive
Lemma shift_left_pos (a b : Z.t) :
  0 a 0 shift_left a b.
Proof.
  apply Z.shiftl_nonneg.
Qed.

[shift_right a b] is positive if [a] is positive
Lemma shift_right_pos (a b : Z.t) :
  0 a
  0 shift_right a b.
Proof.
  unfold shift_right, Z.shiftr.
  apply Z.shiftl_nonneg.
Qed.

[logor a b] is positive if [a] and [b] are positive
Lemma logor_pos (a b : Z.t) :
  0 a 0 b
  0 logor a b.
Proof.
  now rewrite Z.lor_nonneg.
Qed.

[logand a b] is positive if either [a] or [b] is positive
Lemma logand_pos (a b : Z.t) :
  0 a 0 b
  0 logand a b.
Proof.
  unfold logand.
  now rewrite Z.land_nonneg.
Qed.

[logxor a b] is positive when a is positive iff b is positive
Lemma logxor_pos (a b : Z.t) :
  (0 a 0 b)
  0 logxor a b.
Proof.
  unfold logxor.
  now rewrite Z.lxor_nonneg.
Qed.

The function [numbits] returns a non-negative [int].
[Z.compare a b <= 0] implies [a <= b]
Lemma compare_le_0_impl (a b : Z.t) :
  Z.compare a b 0 a b.
Proof.
  unfold Z.compare.
  step; [lia|step; lia].
Qed.