Require Import Eqdep_dec Zquot Zwf.
Require Import Coqlib Zbits Axioms.
Require Archi.
Require Import Lia.

Fixpoint positive_power2 (x : positive) :=
  match x with
  | xH | xI _ => O
  | xO z => S (positive_power2 z)
  end.

Definition Z_power2 (x : Z) : option nat :=
  match x with
  | Z0 => None
  | Zpos x | Zneg x => Some (positive_power2 x)
  end.

Lemma positive_power2_div: forall x,
    (two_power_nat (positive_power2 x) | Zpos x).
  
Lemma Z_power2_div: forall x n (EQ: Z_power2 x = Some n),
    (two_power_nat n | x).

Lemma Z_power2_none: forall x (EQ: Z_power2 x = None), x = 0.

Definition Z_power2_max m x :=
  match Z_power2 x with
  | Some n => n
  | None => m
  end.

Lemma Z_power2_max_div : forall m x, (two_power_nat (Z_power2_max m x) | x).

Definition Z_power2_min m x :=
  match Z_power2 x with
  | Some n => (min m n)%nat
  | None => m
  end.

Lemma Z_power2_min_min : forall m x, (Z_power2_min m x <= m)%nat.

Lemma power2_less: forall m n (LESS : (m <= n)%nat),
    (two_power_nat m | two_power_nat n).

Lemma Z_power2_min_div : forall m x, (two_power_nat (Z_power2_min m x) | x).
    
Definition multiplicative_inverse (n x : Z) :=
  match euclid n x with
  | Euclid_intro _ _ u v d EQ GCD =>
      if zlt d 0
      then -v
      else v
  end.

Lemma multiplicative_inverse_correct :
  forall n x (INVERTIBLE : rel_prime n x),
    (eqmod n (x * (multiplicative_inverse n x)) 1).

Fixpoint Pmax_two_power_rec (x : positive) (p0 : nat) :=
  match x with
  | xH | xI _ => (p0, x)
  | xO x' => Pmax_two_power_rec x' (S p0)
  end.

Lemma Pmax_two_power_rec_less:
  forall x n p0 (LESS : (x < shift_nat n 1)%positive),
    (fst (Pmax_two_power_rec x p0) < p0 + n)%nat.

Definition pos_odd x :=
  match x with
  | xH | xI _ => true
  | xO _ => false
  end.

Lemma Pmax_two_power_rec_spec: forall x p0,
    let (p1, x1) := Pmax_two_power_rec x p0 in
    exists p2,
      pos_odd x1 = true /\
      x = shift_nat p2 x1 /\ (p1 = p0 + p2)%nat.

Definition Pmax_two_power x := Pmax_two_power_rec x 0.

Lemma Pmax_two_power_less:
  forall x n (LESS : (x < shift_nat n 1)%positive),
    (fst (Pmax_two_power x) < n)%nat.

Lemma Pmax_two_power_spec: forall x,
    let (p1, x1) := Pmax_two_power x in
    pos_odd x1 = true /\ x = shift_nat p1 x1.

Definition Zmax_two_power x :=
  match x with
  | Z0 => (1, 0)
  | Zpos x => let (p, x') := Pmax_two_power x in (Z.of_nat p, Zpos x')
  | Zneg x => let (p, x') := Pmax_two_power x in (Z.of_nat p, Zneg x')
  end.

Definition z_odd x :=
  match x with
  | Z0 => false
  | Zpos x' | Zneg x' => pos_odd x'
  end.

Lemma Zmax_two_power_range:
  forall x n
    (NONZERO : x <> 0)
    (LESS : -two_power_nat n < x < two_power_nat n),
    0 <= fst (Zmax_two_power x) < (Z.of_nat n).
  
Lemma Zmax_two_power_spec: forall x (NONZERO: x <> 0),
    let (p1, x1) := Zmax_two_power x in
    z_odd x1 = true /\ x = Z.shiftl x1 p1 /\ p1 >= 0.

Lemma div2_not_odd: forall x, (2 | x) -> z_odd x = false.

Lemma odd_is_rel_prime_2: forall x,
    z_odd x = true -> rel_prime x 2.

Lemma odd_is_rel_prime_2pow: forall x n,
    z_odd x = true -> rel_prime x (two_power_nat n).

Lemma eqmod_inverse_mul :
  forall m a b c, b <> 0 -> (b | c) ->
    eqmod m (a * b) 1 -> eqmod m (c / b) (c * a).

Theorem divexact_to_mul_inverse: forall n x y
     (NONZERO: y <> 0) (EXACT: (y | x)%Z),
    let (py, oy) := Zmax_two_power y in
    eqmod (two_power_nat n) (x/y)
          ((Z.shiftr x py) * (multiplicative_inverse (two_power_nat n) oy)).
    
Set Warnings "-unsupported-attributes".

Comparisons

Inductive comparison : Type :=
  | Ceq : comparison (* same *)
  | Cne : comparison (* different *)
  | Clt : comparison (* less than *)
  | Cle : comparison (* less than or equal *)
  | Cgt : comparison (* greater than *)
  | Cge : comparison. (* greater than or equal *)

Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}.

Definition negate_comparison (c: comparison): comparison :=
  match c with
  | Ceq => Cne
  | Cne => Ceq
  | Clt => Cge
  | Cle => Cgt
  | Cgt => Cle
  | Cge => Clt
  end.

Definition swap_comparison (c: comparison): comparison :=
  match c with
  | Ceq => Ceq
  | Cne => Cne
  | Clt => Cgt
  | Cle => Cge
  | Cgt => Clt
  | Cge => Cle
  end.

Parameterization by the word size, in bits.

Module Type WORDSIZE.
  Parameter wordsize: nat.
  Axiom wordsize_not_zero: wordsize <> 0%nat.
End WORDSIZE.

Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.

Module Make(WS: WORDSIZE).

Definition wordsize: nat := WS.wordsize.
Definition zwordsize: Z := Z.of_nat wordsize.
Definition modulus : Z := two_power_nat wordsize.
Definition half_modulus : Z := modulus / 2.
Definition max_unsigned : Z := modulus - 1.
Definition max_signed : Z := half_modulus - 1.
Definition min_signed : Z := - half_modulus.

Remark wordsize_pos: zwordsize > 0.

Remark modulus_power: modulus = two_p zwordsize.

Remark modulus_gt_one: modulus > 1.

Remark modulus_pos: modulus > 0.

Global Hint Resolve modulus_pos: ints.

Representation of machine integers

Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }.


Definition Z_mod_modulus (x: Z) : Z :=
  match x with
  | Z0 => 0
  | Zpos p => P_mod_two_p p wordsize
  | Zneg p => let r := P_mod_two_p p wordsize in if zeq r 0 then 0 else modulus - r
  end.

Lemma Z_mod_modulus_range:
  forall x, 0 <= Z_mod_modulus x < modulus.
Proof (Z_mod_two_p_range wordsize).

Lemma Z_mod_modulus_range':
  forall x, -1 < Z_mod_modulus x < modulus.

Lemma Z_mod_modulus_eq:
  forall x, Z_mod_modulus x = x mod modulus.
Proof (Z_mod_two_p_eq wordsize).


Definition unsigned (n: int) : Z := intval n.

Definition signed (n: int) : Z :=
  let x := unsigned n in
  if zlt x half_modulus then x else x - modulus.


Definition repr (x: Z) : int :=
  mkint (Z_mod_modulus x) (Z_mod_modulus_range' x).

Definition zero := repr 0.
Definition one := repr 1.
Definition mone := repr (-1).
Definition iwordsize := repr zwordsize.

Lemma mkint_eq:
  forall x y Px Py, x = y -> mkint x Px = mkint y Py.

Lemma eq_dec: forall (x y: int), {x = y} + {x <> y}.

Arithmetic and logical operations over machine integers

Definition eq (x y: int) : bool :=
  if zeq (unsigned x) (unsigned y) then true else false.
Definition lt (x y: int) : bool :=
  if zlt (signed x) (signed y) then true else false.
Definition ltu (x y: int) : bool :=
  if zlt (unsigned x) (unsigned y) then true else false.

Definition neg (x: int) : int := repr (- unsigned x).

Definition add (x y: int) : int :=
  repr (unsigned x + unsigned y).
Definition sub (x y: int) : int :=
  repr (unsigned x - unsigned y).
Definition mul (x y: int) : int :=
  repr (unsigned x * unsigned y).

Definition divs (x y: int) : int :=
  repr (Z.quot (signed x) (signed y)).
Definition mods (x y: int) : int :=
  repr (Z.rem (signed x) (signed y)).

Definition divu (x y: int) : int :=
  repr (unsigned x / unsigned y).
Definition modu (x y: int) : int :=
  repr ((unsigned x) mod (unsigned y)).


Definition and (x y: int): int := repr (Z.land (unsigned x) (unsigned y)).
Definition or (x y: int): int := repr (Z.lor (unsigned x) (unsigned y)).
Definition xor (x y: int) : int := repr (Z.lxor (unsigned x) (unsigned y)).

Definition not (x: int) : int := xor x mone.


Definition shl (x y: int): int := repr (Z.shiftl (unsigned x) (unsigned y)).
Definition shru (x y: int): int := repr (Z.shiftr (unsigned x) (unsigned y)).
Definition shr (x y: int): int := repr (Z.shiftr (signed x) (unsigned y)).

Definition rol (x y: int) : int :=
  let n := (unsigned y) mod zwordsize in
  repr (Z.lor (Z.shiftl (unsigned x) n) (Z.shiftr (unsigned x) (zwordsize - n))).
Definition ror (x y: int) : int :=
  let n := (unsigned y) mod zwordsize in
  repr (Z.lor (Z.shiftr (unsigned x) n) (Z.shiftl (unsigned x) (zwordsize - n))).

Definition rolm (x a m: int): int := and (rol x a) m.


Definition shrx (x y: int): int :=
  divs x (shl one y).


Definition mulhu (x y: int): int := repr ((unsigned x * unsigned y) / modulus).
Definition mulhs (x y: int): int := repr ((signed x * signed y) / modulus).


Definition negative (x: int): int :=
  if lt x zero then one else zero.

Definition add_carry (x y cin: int): int :=
  if zlt (unsigned x + unsigned y + unsigned cin) modulus then zero else one.

Definition add_overflow (x y cin: int): int :=
  let s := signed x + signed y + signed cin in
  if zle min_signed s && zle s max_signed then zero else one.

Definition sub_borrow (x y bin: int): int :=
  if zlt (unsigned x - unsigned y - unsigned bin) 0 then one else zero.

Definition sub_overflow (x y bin: int): int :=
  let s := signed x - signed y - signed bin in
  if zle min_signed s && zle s max_signed then zero else one.


Definition shr_carry (x y: int) : int :=
  if lt x zero && negb (eq (and x (sub (shl one y) one)) zero)
  then one else zero.


Definition zero_ext (n: Z) (x: int) : int := repr (Zzero_ext n (unsigned x)).
Definition sign_ext (n: Z) (x: int) : int := repr (Zsign_ext n (unsigned x)).


Definition one_bits (x: int) : list int :=
  List.map repr (Z_one_bits wordsize (unsigned x) 0).


Definition is_power2 (x: int) : option int :=
  match Z_is_power2 (unsigned x) with
  | Some i => Some (repr i)
  | None => None
  end.


Definition cmp (c: comparison) (x y: int) : bool :=
  match c with
  | Ceq => eq x y
  | Cne => negb (eq x y)
  | Clt => lt x y
  | Cle => negb (lt y x)
  | Cgt => lt y x
  | Cge => negb (lt x y)
  end.

Definition cmpu (c: comparison) (x y: int) : bool :=
  match c with
  | Ceq => eq x y
  | Cne => negb (eq x y)
  | Clt => ltu x y
  | Cle => negb (ltu y x)
  | Cgt => ltu y x
  | Cge => negb (ltu x y)
  end.

Definition is_false (x: int) : Prop := x = zero.
Definition is_true (x: int) : Prop := x <> zero.
Definition notbool (x: int) : int := if eq x zero then one else zero.


Definition divmodu2 (nhi nlo: int) (d: int) : option (int * int) :=
  if eq_dec d zero then None else
   (let (q, r) := Z.div_eucl (unsigned nhi * modulus + unsigned nlo) (unsigned d) in
    if zle q max_unsigned then Some(repr q, repr r) else None).

Definition divmods2 (nhi nlo: int) (d: int) : option (int * int) :=
  if eq_dec d zero then None else
   (let (q, r) := Z.quotrem (signed nhi * modulus + unsigned nlo) (signed d) in
    if zle min_signed q && zle q max_signed then Some(repr q, repr r) else None).

Properties of integers and integer arithmetic

Properties of modulus, max_unsigned, etc.

Remark half_modulus_power:
  half_modulus = two_p (zwordsize - 1).

Remark half_modulus_modulus: modulus = 2 * half_modulus.


Remark half_modulus_pos: half_modulus > 0.

Remark min_signed_neg: min_signed < 0.

Remark max_signed_pos: max_signed >= 0.

Remark wordsize_max_unsigned: zwordsize <= max_unsigned.

Remark two_wordsize_max_unsigned: 2 * zwordsize - 1 <= max_unsigned.

Remark max_signed_unsigned: max_signed < max_unsigned.

Lemma unsigned_repr_eq:
  forall x, unsigned (repr x) = Z.modulo x modulus.

Lemma signed_repr_eq:
  forall x, signed (repr x) = if zlt (Z.modulo x modulus) half_modulus then Z.modulo x modulus else Z.modulo x modulus - modulus.
  

Modulo arithmetic

Definition eqm := eqmod modulus.

Lemma eqm_refl: forall x, eqm x x.
Proof (eqmod_refl modulus).
Global Hint Resolve eqm_refl: ints.

Lemma eqm_refl2:
  forall x y, x = y -> eqm x y.
Proof (eqmod_refl2 modulus).
Global Hint Resolve eqm_refl2: ints.

Lemma eqm_sym: forall x y, eqm x y -> eqm y x.
Proof (eqmod_sym modulus).
Global Hint Resolve eqm_sym: ints.

Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z.
Proof (eqmod_trans modulus).
Global Hint Resolve eqm_trans: ints.

Lemma eqm_small_eq:
  forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y.
Proof (eqmod_small_eq modulus).
Global Hint Resolve eqm_small_eq: ints.

Lemma eqm_add:
  forall a b c d, eqm a b -> eqm c d -> eqm (a + c) (b + d).
Proof (eqmod_add modulus).
Global Hint Resolve eqm_add: ints.

Lemma eqm_neg:
  forall x y, eqm x y -> eqm (-x) (-y).
Proof (eqmod_neg modulus).
Global Hint Resolve eqm_neg: ints.

Lemma eqm_sub:
  forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d).
Proof (eqmod_sub modulus).
Global Hint Resolve eqm_sub: ints.

Lemma eqm_mult:
  forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d).
Proof (eqmod_mult modulus).
Global Hint Resolve eqm_mult: ints.

Lemma eqm_same_bits:
  forall x y,
  (forall i, 0 <= i < zwordsize -> Z.testbit x i = Z.testbit y i) ->
  eqm x y.
Proof (eqmod_same_bits wordsize).

Lemma same_bits_eqm:
  forall x y i,
  eqm x y ->
  0 <= i < zwordsize ->
  Z.testbit x i = Z.testbit y i.
Proof (same_bits_eqmod wordsize).

Properties of the coercions between Z and int

Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y.

Lemma eqm_unsigned_repr:
  forall z, eqm z (unsigned (repr z)).
Global Hint Resolve eqm_unsigned_repr: ints.

Lemma eqm_unsigned_repr_l:
  forall a b, eqm a b -> eqm (unsigned (repr a)) b.
Global Hint Resolve eqm_unsigned_repr_l: ints.

Lemma eqm_unsigned_repr_r:
  forall a b, eqm a b -> eqm a (unsigned (repr b)).
Global Hint Resolve eqm_unsigned_repr_r: ints.

Lemma eqm_signed_unsigned:
  forall x, eqm (signed x) (unsigned x).

Theorem unsigned_range:
  forall i, 0 <= unsigned i < modulus.
Global Hint Resolve unsigned_range: ints.

Theorem unsigned_range_2:
  forall i, 0 <= unsigned i <= max_unsigned.
Global Hint Resolve unsigned_range_2: ints.

Theorem signed_range:
  forall i, min_signed <= signed i <= max_signed.

Theorem repr_unsigned:
  forall i, repr (unsigned i) = i.
Global Hint Resolve repr_unsigned: ints.

Lemma repr_signed:
  forall i, repr (signed i) = i.
Global Hint Resolve repr_signed: ints.

Opaque repr.

Lemma eqm_repr_eq: forall x y, eqm x (unsigned y) -> repr x = y.

Theorem unsigned_repr:
  forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z.
Global Hint Resolve unsigned_repr: ints.

Theorem signed_repr:
  forall z, min_signed <= z <= max_signed -> signed (repr z) = z.

Theorem signed_eq_unsigned:
  forall x, unsigned x <= max_signed -> signed x = unsigned x.

Theorem signed_positive:
  forall x, signed x >= 0 <-> unsigned x <= max_signed.

Lemma nonneg_signed_is_unsigned: forall n,
    signed n >= 0 -> signed n = unsigned n.

Properties of zero, one, minus one

Theorem unsigned_zero: unsigned zero = 0.

Theorem unsigned_one: unsigned one = 1.

Theorem unsigned_mone: unsigned mone = modulus - 1.

Theorem signed_zero: signed zero = 0.

Theorem signed_one: zwordsize > 1 -> signed one = 1.

Theorem signed_mone: signed mone = -1.

Theorem one_not_zero: one <> zero.

Theorem unsigned_repr_wordsize:
  unsigned iwordsize = zwordsize.



Definition divu_exact (x y : int) : option int :=
  if negb (zeq (unsigned y) 0) && zeq ((unsigned x) mod (unsigned y)) 0
  then Some (repr ((unsigned x) / (unsigned y)))
  else None.

Theorem divu_exact_expand: forall x y,
    match divu_exact x y with
    | None => True
    | Some d =>
      let (py, oy) := Zmax_two_power (unsigned y) in
      d = mul (shru x (repr py)) (repr (multiplicative_inverse modulus oy))
    end.

Definition divs_exact (x y : int) : option int :=
  if negb (zeq (signed y) 0) && zeq ((signed x) mod (signed y)) 0
  then Some (repr ((signed x) / (signed y)))
  else None.

Lemma signed_0_unsigned_0: forall x, signed x = 0 <-> unsigned x = 0.
  
Theorem divs_exact_expand: forall x y,
    match divs_exact x y with
    | None => True
    | Some d =>
      let (py, oy) := Zmax_two_power (signed y) in
      d = mul (shr x (repr py)) (repr (multiplicative_inverse modulus oy))
    end.

Properties of equality

Theorem eq_sym:
  forall x y, eq x y = eq y x.

Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y.

Theorem eq_true: forall x, eq x x = true.

Theorem eq_false: forall x y, x <> y -> eq x y = false.

Theorem lt_false: forall x, lt x x = false.

Theorem ltu_false: forall x, ltu x x = false.

Theorem same_if_eq: forall x y, eq x y = true -> x = y.

Theorem eq_signed:
  forall x y, eq x y = if zeq (signed x) (signed y) then true else false.

Properties of addition

Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y).

Theorem add_signed: forall x y, add x y = repr (signed x + signed y).

Theorem add_commut: forall x y, add x y = add y x.

Theorem add_zero: forall x, add x zero = x.

Theorem add_zero_l: forall x, add zero x = x.

Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).

Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).

Theorem add_neg_zero: forall x, add x (neg x) = zero.

Theorem unsigned_add_carry:
  forall x y,
  unsigned (add x y) = unsigned x + unsigned y - unsigned (add_carry x y zero) * modulus.

Corollary unsigned_add_either:
  forall x y,
  unsigned (add x y) = unsigned x + unsigned y
  \/ unsigned (add x y) = unsigned x + unsigned y - modulus.

Properties of negation

Theorem neg_repr: forall z, neg (repr z) = repr (-z).

Theorem neg_zero: neg zero = zero.

Theorem neg_involutive: forall x, neg (neg x) = x.

Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).

Properties of subtraction

Theorem sub_zero_l: forall x, sub x zero = x.

Theorem sub_zero_r: forall x, sub zero x = neg x.

Theorem sub_add_opp: forall x y, sub x y = add x (neg y).

Theorem sub_idem: forall x, sub x x = zero.

Theorem sub_add_l: forall x y z, sub (add x y) z = add (sub x z) y.

Theorem sub_add_r: forall x y z, sub x (add y z) = add (sub x z) (neg y).

Theorem sub_shifted:
  forall x y z,
  sub (add x z) (add y z) = sub x y.

Theorem sub_signed:
  forall x y, sub x y = repr (signed x - signed y).

Theorem unsigned_sub_borrow:
  forall x y,
  unsigned (sub x y) = unsigned x - unsigned y + unsigned (sub_borrow x y zero) * modulus.

Properties of multiplication

Theorem mul_commut: forall x y, mul x y = mul y x.

Theorem mul_zero: forall x, mul x zero = zero.

Theorem mul_one: forall x, mul x one = x.

Theorem mul_mone: forall x, mul x mone = neg x.

Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).

Theorem mul_add_distr_l:
  forall x y z, mul (add x y) z = add (mul x z) (mul y z).

Theorem mul_add_distr_r:
  forall x y z, mul x (add y z) = add (mul x y) (mul x z).

Theorem neg_mul_distr_l:
  forall x y, neg(mul x y) = mul (neg x) y.

Theorem neg_mul_distr_r:
   forall x y, neg(mul x y) = mul x (neg y).

Theorem mul_signed:
  forall x y, mul x y = repr (signed x * signed y).

Properties of division and modulus

Lemma modu_divu_Euclid:
  forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y).

Theorem modu_divu:
  forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y).

Lemma mods_divs_Euclid:
  forall x y, x = add (mul (divs x y) y) (mods x y).

Theorem mods_divs:
  forall x y, mods x y = sub x (mul (divs x y) y).

Theorem divu_one:
  forall x, divu x one = x.

Theorem divs_one:
  forall x, zwordsize > 1 -> divs x one = x.

Theorem modu_one:
  forall x, modu x one = zero.

Theorem divs_mone:
  forall x, divs x mone = neg x.

Theorem mods_mone:
  forall x, mods x mone = zero.

Theorem divmodu2_divu_modu:
  forall n d,
  d <> zero -> divmodu2 zero n d = Some (divu n d, modu n d).

Lemma unsigned_signed:
  forall n, unsigned n = if lt n zero then signed n + modulus else signed n.

Theorem divmods2_divs_mods:
  forall n d,
  d <> zero -> n <> repr min_signed \/ d <> mone ->
  divmods2 (if lt n zero then mone else zero) n d = Some (divs n d, mods n d).
  

Bit-level properties

Definition testbit (x: int) (i: Z) : bool := Z.testbit (unsigned x) i.

Lemma testbit_repr:
  forall x i,
  0 <= i < zwordsize ->
  testbit (repr x) i = Z.testbit x i.

Lemma same_bits_eq:
  forall x y,
  (forall i, 0 <= i < zwordsize -> testbit x i = testbit y i) ->
  x = y.

Lemma bits_above:
  forall x i, i >= zwordsize -> testbit x i = false.

Lemma bits_below:
  forall x i, i < 0 -> testbit x i = false.

Lemma bits_zero:
  forall i, testbit zero i = false.

Remark bits_one: forall n, testbit one n = zeq n 0.

Lemma bits_mone:
  forall i, 0 <= i < zwordsize -> testbit mone i = true.

#[global]
Hint Rewrite bits_zero bits_mone : ints.

Ltac bit_solve :=
  intros; apply same_bits_eq; intros; autorewrite with ints; auto with bool.

Lemma sign_bit_of_unsigned:
  forall x, testbit x (zwordsize - 1) = if zlt (unsigned x) half_modulus then false else true.

Local Transparent repr.
Lemma sign_bit_of_signed: forall x,
    (testbit x (zwordsize - 1)) = lt x zero.
Local Opaque repr.

Lemma bits_signed:
  forall x i, 0 <= i ->
  Z.testbit (signed x) i = testbit x (if zlt i zwordsize then i else zwordsize - 1).

Lemma bits_le:
  forall x y,
  (forall i, 0 <= i < zwordsize -> testbit x i = true -> testbit y i = true) ->
  unsigned x <= unsigned y.

Properties of bitwise and, or, xor

Lemma bits_and:
  forall x y i, 0 <= i < zwordsize ->
  testbit (and x y) i = testbit x i && testbit y i.

Lemma bits_or:
  forall x y i, 0 <= i < zwordsize ->
  testbit (or x y) i = testbit x i || testbit y i.

Lemma bits_xor:
  forall x y i, 0 <= i < zwordsize ->
  testbit (xor x y) i = xorb (testbit x i) (testbit y i).

Lemma bits_not:
  forall x i, 0 <= i < zwordsize ->
  testbit (not x) i = negb (testbit x i).

#[global]
Hint Rewrite bits_and bits_or bits_xor bits_not: ints.

Theorem and_commut: forall x y, and x y = and y x.

Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).

Theorem and_zero: forall x, and x zero = zero.

Corollary and_zero_l: forall x, and zero x = zero.

Theorem and_mone: forall x, and x mone = x.

Corollary and_mone_l: forall x, and mone x = x.

Theorem and_idem: forall x, and x x = x.

Theorem or_commut: forall x y, or x y = or y x.

Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).

Theorem or_zero: forall x, or x zero = x.

Corollary or_zero_l: forall x, or zero x = x.

Theorem or_mone: forall x, or x mone = mone.

Theorem or_idem: forall x, or x x = x.

Theorem and_or_distrib:
  forall x y z,
  and x (or y z) = or (and x y) (and x z).

Corollary and_or_distrib_l:
  forall x y z,
  and (or x y) z = or (and x z) (and y z).

Theorem or_and_distrib:
  forall x y z,
  or x (and y z) = and (or x y) (or x z).

Corollary or_and_distrib_l:
  forall x y z,
  or (and x y) z = and (or x z) (or y z).

Theorem and_or_absorb: forall x y, and x (or x y) = x.

Theorem or_and_absorb: forall x y, or x (and x y) = x.

Theorem xor_commut: forall x y, xor x y = xor y x.

Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).

Theorem xor_zero: forall x, xor x zero = x.

Corollary xor_zero_l: forall x, xor zero x = x.

Theorem xor_zero_inv: forall x y, xor x y = x -> y = zero.

Theorem xor_idem: forall x, xor x x = zero.

Theorem xor_zero_one: xor zero one = one.

Theorem xor_one_one: xor one one = zero.

Theorem xor_zero_equal: forall x y, xor x y = zero -> x = y.

Theorem xor_is_zero: forall x y, eq (xor x y) zero = eq x y.

Theorem xor_inj_r : forall x y1 y2,
    xor x y1 = xor x y2 ->
    y1 = y2.

Theorem and_xor_distrib:
  forall x y z,
  and x (xor y z) = xor (and x y) (and x z).

Theorem and_le:
  forall x y, unsigned (and x y) <= unsigned x.

Theorem or_le:
  forall x y, unsigned x <= unsigned (or x y).

Properties of bitwise complement.

Theorem not_involutive:
  forall (x: int), not (not x) = x.

Theorem not_zero:
  not zero = mone.

Theorem not_mone:
  not mone = zero.

Theorem not_or_and_not:
  forall x y, not (or x y) = and (not x) (not y).

Theorem not_and_or_not:
  forall x y, not (and x y) = or (not x) (not y).

Theorem and_not_self:
  forall x, and x (not x) = zero.

Theorem or_not_self:
  forall x, or x (not x) = mone.

Theorem xor_not_self:
  forall x, xor x (not x) = mone.

Lemma unsigned_not:
  forall x, unsigned (not x) = max_unsigned - unsigned x.

Theorem not_neg:
  forall x, not x = add (neg x) mone.

Theorem neg_not:
  forall x, neg x = add (not x) one.

Theorem sub_add_not:
  forall x y, sub x y = add (add x (not y)) one.

Theorem sub_add_not_3:
  forall x y b,
  b = zero \/ b = one ->
  sub (sub x y) b = add (add x (not y)) (xor b one).

Theorem sub_borrow_add_carry:
  forall x y b,
  b = zero \/ b = one ->
  sub_borrow x y b = xor (add_carry x (not y) (xor b one)) one.

Connections between add and bitwise logical operations.

Lemma Z_add_is_or:
  forall i, 0 <= i ->
  forall x y,
  (forall j, 0 <= j <= i -> Z.testbit x j && Z.testbit y j = false) ->
  Z.testbit (x + y) i = Z.testbit x i || Z.testbit y i.

Theorem add_is_or:
  forall x y,
  and x y = zero ->
  add x y = or x y.

Theorem xor_is_or:
  forall x y, and x y = zero -> xor x y = or x y.

Theorem add_is_xor:
  forall x y,
  and x y = zero ->
  add x y = xor x y.

Theorem add_and:
  forall x y z,
  and y z = zero ->
  add (and x y) (and x z) = and x (or y z).

Properties of shifts

Lemma bits_shl:
  forall x y i,
  0 <= i < zwordsize ->
  testbit (shl x y) i =
  if zlt i (unsigned y) then false else testbit x (i - unsigned y).

Lemma bits_shru:
  forall x y i,
  0 <= i < zwordsize ->
  testbit (shru x y) i =
  if zlt (i + unsigned y) zwordsize then testbit x (i + unsigned y) else false.

Lemma bits_shr:
  forall x y i,
  0 <= i < zwordsize ->
  testbit (shr x y) i =
  testbit x (if zlt (i + unsigned y) zwordsize then i + unsigned y else zwordsize - 1).

#[global]
Hint Rewrite bits_shl bits_shru bits_shr: ints.

Theorem shl_zero: forall x, shl x zero = x.

Lemma bitwise_binop_shl:
  forall f f' x y n,
  (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) ->
  f' false false = false ->
  f (shl x n) (shl y n) = shl (f x y) n.

Theorem and_shl:
  forall x y n,
  and (shl x n) (shl y n) = shl (and x y) n.

Theorem or_shl:
  forall x y n,
  or (shl x n) (shl y n) = shl (or x y) n.

Theorem xor_shl:
  forall x y n,
  xor (shl x n) (shl y n) = shl (xor x y) n.

Lemma ltu_inv:
  forall x y, ltu x y = true -> 0 <= unsigned x < unsigned y.

Lemma ltu_iwordsize_inv:
  forall x, ltu x iwordsize = true -> 0 <= unsigned x < zwordsize.

Theorem shl_shl:
  forall x y z,
  ltu y iwordsize = true ->
  ltu z iwordsize = true ->
  ltu (add y z) iwordsize = true ->
  shl (shl x y) z = shl x (add y z).

Theorem sub_ltu:
  forall x y,
    ltu x y = true ->
    0 <= unsigned y - unsigned x <= unsigned y.

Theorem shru_zero: forall x, shru x zero = x.

Lemma bitwise_binop_shru:
  forall f f' x y n,
  (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) ->
  f' false false = false ->
  f (shru x n) (shru y n) = shru (f x y) n.

Theorem and_shru:
  forall x y n,
  and (shru x n) (shru y n) = shru (and x y) n.

Theorem or_shru:
  forall x y n,
  or (shru x n) (shru y n) = shru (or x y) n.

Theorem xor_shru:
  forall x y n,
  xor (shru x n) (shru y n) = shru (xor x y) n.

Theorem shru_shru:
  forall x y z,
  ltu y iwordsize = true ->
  ltu z iwordsize = true ->
  ltu (add y z) iwordsize = true ->
  shru (shru x y) z = shru x (add y z).

Theorem shr_zero: forall x, shr x zero = x.

Lemma bitwise_binop_shr:
  forall f f' x y n,
  (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) ->
  f (shr x n) (shr y n) = shr (f x y) n.

Theorem and_shr:
  forall x y n,
  and (shr x n) (shr y n) = shr (and x y) n.

Theorem or_shr:
  forall x y n,
  or (shr x n) (shr y n) = shr (or x y) n.

Theorem xor_shr:
  forall x y n,
  xor (shr x n) (shr y n) = shr (xor x y) n.

Theorem shr_shr:
  forall x y z,
  ltu y iwordsize = true ->
  ltu z iwordsize = true ->
  ltu (add y z) iwordsize = true ->
  shr (shr x y) z = shr x (add y z).

Theorem and_shr_shru:
  forall x y z,
  and (shr x z) (shru y z) = shru (and x y) z.

Theorem shr_and_shru_and:
  forall x y z,
  shru (shl z y) y = z ->
  and (shr x y) z = and (shru x y) z.

Theorem shru_lt_zero:
  forall x,
  shru x (repr (zwordsize - 1)) = if lt x zero then one else zero.

Theorem shr_lt_zero:
  forall x,
  shr x (repr (zwordsize - 1)) = if lt x zero then mone else zero.

Properties of rotations

Lemma bits_rol:
  forall x y i,
  0 <= i < zwordsize ->
  testbit (rol x y) i = testbit x ((i - unsigned y) mod zwordsize).

Lemma bits_ror:
  forall x y i,
  0 <= i < zwordsize ->
  testbit (ror x y) i = testbit x ((i + unsigned y) mod zwordsize).

#[global]
Hint Rewrite bits_rol bits_ror: ints.

Theorem shl_rolm:
  forall x n,
  ltu n iwordsize = true ->
  shl x n = rolm x n (shl mone n).

Theorem shru_rolm:
  forall x n,
  ltu n iwordsize = true ->
  shru x n = rolm x (sub iwordsize n) (shru mone n).

Theorem rol_zero:
  forall x,
  rol x zero = x.

Lemma bitwise_binop_rol:
  forall f f' x y n,
  (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) ->
  rol (f x y) n = f (rol x n) (rol y n).

Theorem rol_and:
  forall x y n,
  rol (and x y) n = and (rol x n) (rol y n).

Theorem rol_or:
  forall x y n,
  rol (or x y) n = or (rol x n) (rol y n).

Theorem rol_xor:
  forall x y n,
  rol (xor x y) n = xor (rol x n) (rol y n).

Theorem rol_rol:
  forall x n m,
  Z.divide zwordsize modulus ->
  rol (rol x n) m = rol x (modu (add n m) iwordsize).

Theorem rolm_zero:
  forall x m,
  rolm x zero m = and x m.

Theorem rolm_rolm:
  forall x n1 m1 n2 m2,
  Z.divide zwordsize modulus ->
  rolm (rolm x n1 m1) n2 m2 =
    rolm x (modu (add n1 n2) iwordsize)
           (and (rol m1 n2) m2).

Theorem or_rolm:
  forall x n m1 m2,
  or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2).

Theorem ror_rol:
  forall x y,
  ltu y iwordsize = true ->
  ror x y = rol x (sub iwordsize y).

Theorem ror_rol_neg:
  forall x y, (zwordsize | modulus) -> ror x y = rol x (neg y).

Theorem or_ror:
  forall x y z,
  ltu y iwordsize = true ->
  ltu z iwordsize = true ->
  add y z = iwordsize ->
  ror x z = or (shl x y) (shru x z).

Properties of is_power2.

Remark is_power2_inv:
  forall n logn,
  is_power2 n = Some logn ->
  Z_is_power2 (unsigned n) = Some (unsigned logn) /\ 0 <= unsigned logn < zwordsize.

Lemma is_power2_rng:
  forall n logn,
  is_power2 n = Some logn ->
  0 <= unsigned logn < zwordsize.

Theorem is_power2_range:
  forall n logn,
  is_power2 n = Some logn -> ltu logn iwordsize = true.

Lemma is_power2_correct:
  forall n logn,
  is_power2 n = Some logn ->
  unsigned n = two_p (unsigned logn).

Remark two_p_range:
  forall n,
  0 <= n < zwordsize ->
  0 <= two_p n <= max_unsigned.

Lemma is_power2_two_p:
  forall n, 0 <= n < zwordsize ->
  is_power2 (repr (two_p n)) = Some (repr n).

Relation between bitwise operations and multiplications / divisions by powers of 2

Lemma shl_mul_two_p:
  forall x y,
  shl x y = mul x (repr (two_p (unsigned y))).

Theorem shl_mul:
  forall x y,
  shl x y = mul x (shl one y).

Theorem mul_pow2:
  forall x n logn,
  is_power2 n = Some logn ->
  mul x n = shl x logn.

Theorem shifted_or_is_add:
  forall x y n,
  0 <= n < zwordsize ->
  unsigned y < two_p n ->
  or (shl x (repr n)) y = repr(unsigned x * two_p n + unsigned y).


Lemma shru_div_two_p:
  forall x y,
  shru x y = repr (unsigned x / two_p (unsigned y)).

Theorem divu_pow2:
  forall x n logn,
  is_power2 n = Some logn ->
  divu x n = shru x logn.


Lemma shr_div_two_p:
  forall x y,
  shr x y = repr (signed x / two_p (unsigned y)).

Theorem divs_pow2:
  forall x n logn,
  is_power2 n = Some logn ->
  divs x n = shrx x logn.


Theorem modu_and:
  forall x n logn,
  is_power2 n = Some logn ->
  modu x n = and x (sub n one).

Properties of shrx (signed division by a power of 2)

Theorem shrx_zero:
  forall x, zwordsize > 1 -> shrx x zero = x.

Theorem shrx_shr:
  forall x y,
  ltu y (repr (zwordsize - 1)) = true ->
  shrx x y = shr (if lt x zero then add x (sub (shl one y) one) else x) y.

Theorem shrx_shr_2:
  forall x y,
  ltu y (repr (zwordsize - 1)) = true ->
  shrx x y = shr (add x (shru (shr x (repr (zwordsize - 1))) (sub iwordsize y))) y.

Theorem shrx1_shr:
  forall x,
  ltu one (repr (zwordsize - 1)) = true ->
  shrx x (repr 1) = shr (add x (shru x (repr (zwordsize - 1)))) (repr 1).

Theorem shrx_carry:
  forall x y,
  ltu y (repr (zwordsize - 1)) = true ->
  shrx x y = add (shr x y) (shr_carry x y).


Lemma shr_shru_positive:
  forall x y,
  signed x >= 0 ->
  shr x y = shru x y.

Lemma and_positive:
  forall x y, signed y >= 0 -> signed (and x y) >= 0.

Theorem shr_and_is_shru_and:
  forall x y z,
  lt y zero = false -> shr (and x y) z = shru (and x y) z.

Properties of mulhu (upper bits of unsigned multiplication)

Lemma mulhu_zero:
  forall x, mulhu x zero = zero.

Lemma mulhu_one:
  forall x, mulhu x one = zero.

Lemma mulhu_commut:
  forall x y, mulhu x y = mulhu y x.

Properties of mulhs (upper bits of signed multiplication)

Lemma mulhs_zero:
  forall x, mulhs x zero = zero.

Lemma mulhs_commut:
  forall x y, mulhs x y = mulhs y x.

Properties of integer zero extension and sign extension.

Lemma bits_zero_ext:
  forall n x i, 0 <= i ->
  testbit (zero_ext n x) i = if zlt i n then testbit x i else false.

Lemma bits_sign_ext:
  forall n x i, 0 <= i < zwordsize ->
  testbit (sign_ext n x) i = testbit x (if zlt i n then i else n - 1).

#[global]
Hint Rewrite bits_zero_ext bits_sign_ext: ints.

Theorem zero_ext_above:
  forall n x, n >= zwordsize -> zero_ext n x = x.

Theorem zero_ext_below:
  forall n x, n <= 0 -> zero_ext n x = zero.

Theorem sign_ext_above:
  forall n x, n >= zwordsize -> sign_ext n x = x.

Theorem sign_ext_below:
  forall n x, n <= 0 -> sign_ext n x = zero.

Theorem zero_ext_and:
  forall n x, 0 <= n -> zero_ext n x = and x (repr (two_p n - 1)).

Theorem zero_ext_mod:
  forall n x, 0 <= n < zwordsize ->
  unsigned (zero_ext n x) = Z.modulo (unsigned x) (two_p n).

Theorem zero_ext_widen:
  forall x n n', 0 <= n <= n' ->
  zero_ext n' (zero_ext n x) = zero_ext n x.

Theorem sign_ext_widen:
  forall x n n', 0 < n <= n' ->
  sign_ext n' (sign_ext n x) = sign_ext n x.

Theorem sign_zero_ext_widen:
  forall x n n', 0 <= n < n' ->
  sign_ext n' (zero_ext n x) = zero_ext n x.

Theorem zero_ext_narrow:
  forall x n n', 0 <= n <= n' ->
  zero_ext n (zero_ext n' x) = zero_ext n x.

Theorem sign_ext_narrow:
  forall x n n', 0 < n <= n' ->
  sign_ext n (sign_ext n' x) = sign_ext n x.

Theorem zero_sign_ext_narrow:
  forall x n n', 0 < n <= n' ->
  zero_ext n (sign_ext n' x) = zero_ext n x.

Theorem zero_ext_idem:
  forall n x, 0 <= n -> zero_ext n (zero_ext n x) = zero_ext n x.

Theorem sign_ext_idem:
  forall n x, 0 < n -> sign_ext n (sign_ext n x) = sign_ext n x.
 
Theorem sign_ext_zero_ext:
  forall n x, 0 < n -> sign_ext n (zero_ext n x) = sign_ext n x.

Theorem zero_ext_sign_ext:
  forall n x, 0 < n -> zero_ext n (sign_ext n x) = zero_ext n x.

Theorem sign_ext_equal_if_zero_equal:
  forall n x y, 0 < n ->
  zero_ext n x = zero_ext n y ->
  sign_ext n x = sign_ext n y.

Theorem shru_shl:
  forall x y z, ltu y iwordsize = true -> ltu z iwordsize = true ->
  shru (shl x y) z =
  if ltu z y then shl (zero_ext (zwordsize - unsigned y) x) (sub y z)
             else zero_ext (zwordsize - unsigned z) (shru x (sub z y)).

Corollary zero_ext_shru_shl:
  forall n x,
  0 < n < zwordsize ->
  let y := repr (zwordsize - n) in
  zero_ext n x = shru (shl x y) y.

Theorem shr_shl:
  forall x y z, ltu y iwordsize = true -> ltu z iwordsize = true ->
  shr (shl x y) z =
  if ltu z y then shl (sign_ext (zwordsize - unsigned y) x) (sub y z)
             else sign_ext (zwordsize - unsigned z) (shr x (sub z y)).

Corollary sign_ext_shr_shl:
  forall n x,
  0 < n <= zwordsize ->
  let y := repr (zwordsize - n) in
  sign_ext n x = shr (shl x y) y.

Theorem shr_shl2:
  forall x y z, ltu y iwordsize = true -> ltu z iwordsize = true ->
  shr (shl x y) z =
  if ltu z y then shl (sign_ext (zwordsize - unsigned y) x) (sub y z)
             else sign_ext (zwordsize - unsigned z) (shru x (sub z y)).


Lemma zero_ext_range:
  forall n x, 0 <= n < zwordsize -> 0 <= unsigned (zero_ext n x) < two_p n.

Lemma eqmod_zero_ext:
  forall n x, 0 <= n < zwordsize -> eqmod (two_p n) (unsigned (zero_ext n x)) (unsigned x).


Lemma sign_ext_range:
  forall n x, 0 < n < zwordsize -> -two_p (n-1) <= signed (sign_ext n x) < two_p (n-1).

Lemma eqmod_sign_ext':
  forall n x, 0 < n < zwordsize ->
  eqmod (two_p n) (unsigned (sign_ext n x)) (unsigned x).

Lemma eqmod_sign_ext:
  forall n x, 0 < n < zwordsize ->
  eqmod (two_p n) (signed (sign_ext n x)) (unsigned x).


Lemma shl_zero_ext:
  forall n m x, 0 <= n ->
  shl (zero_ext n x) m = zero_ext (n + unsigned m) (shl x m).

Lemma shl_sign_ext:
  forall n m x, 0 < n ->
  shl (sign_ext n x) m = sign_ext (n + unsigned m) (shl x m).

Lemma shru_zero_ext:
  forall n m x, 0 <= n ->
  shru (zero_ext (n + unsigned m) x) m = zero_ext n (shru x m).

Lemma shru_zero_ext_0:
  forall n m x, n <= unsigned m ->
  shru (zero_ext n x) m = zero.

Lemma shr_sign_ext:
  forall n m x, 0 < n -> n + unsigned m < zwordsize ->
  shr (sign_ext (n + unsigned m) x) m = sign_ext n (shr x m).

Lemma zero_ext_shru_min:
  forall s x n, ltu n iwordsize = true ->
  zero_ext s (shru x n) = zero_ext (Z.min s (zwordsize - unsigned n)) (shru x n).

Lemma sign_ext_shr_min:
  forall s x n, ltu n iwordsize = true ->
  sign_ext s (shr x n) = sign_ext (Z.min s (zwordsize - unsigned n)) (shr x n).

Lemma shl_zero_ext_min:
  forall s x n, ltu n iwordsize = true ->
  shl (zero_ext s x) n = shl (zero_ext (Z.min s (zwordsize - unsigned n)) x) n.

Lemma shl_sign_ext_min:
  forall s x n, ltu n iwordsize = true ->
  shl (sign_ext s x) n = shl (sign_ext (Z.min s (zwordsize - unsigned n)) x) n.

Properties of one_bits (decomposition in sum of powers of two)

Theorem one_bits_range:
  forall x i, In i (one_bits x) -> ltu i iwordsize = true.

Fixpoint int_of_one_bits (l: list int) : int :=
  match l with
  | nil => zero
  | a :: b => add (shl one a) (int_of_one_bits b)
  end.

Theorem one_bits_decomp:
  forall x, x = int_of_one_bits (one_bits x).

Properties of comparisons

Theorem negate_cmp:
  forall c x y, cmp (negate_comparison c) x y = negb (cmp c x y).

Theorem negate_cmpu:
  forall c x y, cmpu (negate_comparison c) x y = negb (cmpu c x y).

Theorem swap_cmp:
  forall c x y, cmp (swap_comparison c) x y = cmp c y x.

Theorem swap_cmpu:
  forall c x y, cmpu (swap_comparison c) x y = cmpu c y x.

Lemma translate_eq:
  forall x y d,
  eq (add x d) (add y d) = eq x y.

Lemma translate_ltu:
  forall x y d,
  0 <= unsigned x + unsigned d <= max_unsigned ->
  0 <= unsigned y + unsigned d <= max_unsigned ->
  ltu (add x d) (add y d) = ltu x y.

Theorem translate_cmpu:
  forall c x y d,
  0 <= unsigned x + unsigned d <= max_unsigned ->
  0 <= unsigned y + unsigned d <= max_unsigned ->
  cmpu c (add x d) (add y d) = cmpu c x y.

Lemma translate_lt:
  forall x y d,
  min_signed <= signed x + signed d <= max_signed ->
  min_signed <= signed y + signed d <= max_signed ->
  lt (add x d) (add y d) = lt x y.

Theorem translate_cmp:
  forall c x y d,
  min_signed <= signed x + signed d <= max_signed ->
  min_signed <= signed y + signed d <= max_signed ->
  cmp c (add x d) (add y d) = cmp c x y.

Theorem notbool_isfalse_istrue:
  forall x, is_false x -> is_true (notbool x).

Theorem notbool_istrue_isfalse:
  forall x, is_true x -> is_false (notbool x).

Theorem ltu_range_test:
  forall x y,
  ltu x y = true -> unsigned y <= max_signed ->
  0 <= signed x < unsigned y.

Theorem lt_sub_overflow:
  forall x y,
  xor (sub_overflow x y zero) (negative (sub x y)) = if lt x y then one else zero.

Lemma signed_eq:
  forall x y, eq x y = zeq (signed x) (signed y).

Lemma not_lt:
  forall x y, negb (lt y x) = (lt x y || eq x y).

Lemma lt_not:
  forall x y, lt y x = negb (lt x y) && negb (eq x y).

Lemma not_ltu:
  forall x y, negb (ltu y x) = (ltu x y || eq x y).

Lemma ltu_not:
  forall x y, ltu y x = negb (ltu x y) && negb (eq x y).

Non-overlapping test

Definition no_overlap (ofs1: int) (sz1: Z) (ofs2: int) (sz2: Z) : bool :=
  let x1 := unsigned ofs1 in let x2 := unsigned ofs2 in
     zlt (x1 + sz1) modulus && zlt (x2 + sz2) modulus
  && (zle (x1 + sz1) x2 || zle (x2 + sz2) x1).

Lemma no_overlap_sound:
  forall ofs1 sz1 ofs2 sz2 base,
  sz1 > 0 -> sz2 > 0 -> no_overlap ofs1 sz1 ofs2 sz2 = true ->
  unsigned (add base ofs1) + sz1 <= unsigned (add base ofs2)
  \/ unsigned (add base ofs2) + sz2 <= unsigned (add base ofs1).

Size of integers, in bits.

Definition size (x: int) : Z := Zsize (unsigned x).

Theorem size_zero: size zero = 0.

Theorem bits_size_1:
  forall x, x = zero \/ testbit x (Z.pred (size x)) = true.

Theorem bits_size_2:
  forall x i, size x <= i -> testbit x i = false.

Theorem size_range:
  forall x, 0 <= size x <= zwordsize.

Theorem bits_size_3:
  forall x n,
  0 <= n ->
  (forall i, n <= i < zwordsize -> testbit x i = false) ->
  size x <= n.

Theorem bits_size_4:
  forall x n,
  0 <= n ->
  testbit x (Z.pred n) = true ->
  (forall i, n <= i < zwordsize -> testbit x i = false) ->
  size x = n.

Theorem size_interval_1:
  forall x, 0 <= unsigned x < two_p (size x).

Theorem size_interval_2:
  forall x n, 0 <= n -> 0 <= unsigned x < two_p n -> n >= size x.

Theorem size_and:
  forall a b, size (and a b) <= Z.min (size a) (size b).

Corollary and_interval:
  forall a b, 0 <= unsigned (and a b) < two_p (Z.min (size a) (size b)).

Theorem size_or:
  forall a b, size (or a b) = Z.max (size a) (size b).

Corollary or_interval:
  forall a b, 0 <= unsigned (or a b) < two_p (Z.max (size a) (size b)).

Theorem size_xor:
  forall a b, size (xor a b) <= Z.max (size a) (size b).

Corollary xor_interval:
  forall a b, 0 <= unsigned (xor a b) < two_p (Z.max (size a) (size b)).

Accessing bit fields

Definition unsigned_bitfield_extract (pos width: Z) (n: int) : int :=
  zero_ext width (shru n (repr pos)).

Definition signed_bitfield_extract (pos width: Z) (n: int) : int :=
  sign_ext width (shru n (repr pos)).

Definition bitfield_insert (pos width: Z) (n p: int) : int :=
  let mask := shl (repr (two_p width - 1)) (repr pos) in
  or (shl (zero_ext width p) (repr pos))
     (and n (not mask)).

Lemma bits_unsigned_bitfield_extract:
  forall pos width n i,
  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
  0 <= i < zwordsize ->
  testbit (unsigned_bitfield_extract pos width n) i =
  if zlt i width then testbit n (i + pos) else false.

Lemma bits_signed_bitfield_extract:
  forall pos width n i,
  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
  0 <= i < zwordsize ->
  testbit (signed_bitfield_extract pos width n) i =
  testbit n (if zlt i width then i + pos else width - 1 + pos).

Lemma bits_bitfield_insert:
  forall pos width n p i,
  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
  0 <= i < zwordsize ->
  testbit (bitfield_insert pos width n p) i =
  if zle pos i && zlt i (pos + width) then testbit p (i - pos) else testbit n i.

Lemma unsigned_bitfield_extract_by_shifts:
  forall pos width n,
  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
  unsigned_bitfield_extract pos width n =
  shru (shl n (repr (zwordsize - pos - width))) (repr (zwordsize - width)).

Lemma signed_bitfield_extract_by_shifts:
  forall pos width n,
  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
  signed_bitfield_extract pos width n =
  shr (shl n (repr (zwordsize - pos - width))) (repr (zwordsize - width)).

Lemma bitfield_insert_alternative:
  forall pos width n p,
  0 <= width ->
  bitfield_insert pos width n p =
  let mask := shl (repr (two_p width - 1)) (repr pos) in
  or (and (shl p (repr pos)) mask)
     (and n (not mask)).

Lemma unsigned_huge_two_p: forall x,
    (zwordsize <= x) ->
    unsigned (repr (2 ^ x)) = 0.


Remark min_signed_wraps:
  signed (repr (2 ^ (zwordsize - 1))) = - (2 ^ (zwordsize - 1)).

Lemma nonneg_shrx_is_shru:
  forall x (xRANGE : signed x >= 0) n,
    shrx x n = shru x n.

End Make.

Specialization to integers of size 8, 32, and 64 bits

Module Wordsize_32.
  Definition wordsize := 32%nat.
  Remark wordsize_not_zero: wordsize <> 0%nat.
End Wordsize_32.

Strategy opaque [Wordsize_32.wordsize].

Module Int := Make(Wordsize_32).

Strategy 0 [Wordsize_32.wordsize].

Notation int := Int.int.

Remark int_wordsize_divides_modulus:
  Z.divide (Z.of_nat Int.wordsize) Int.modulus.

Module Wordsize_8.
  Definition wordsize := 8%nat.
  Remark wordsize_not_zero: wordsize <> 0%nat.
End Wordsize_8.

Strategy opaque [Wordsize_8.wordsize].

Module Byte := Make(Wordsize_8).

Strategy 0 [Wordsize_8.wordsize].

Notation byte := Byte.int.

Module Wordsize_64.
  Definition wordsize := 64%nat.
  Remark wordsize_not_zero: wordsize <> 0%nat.
End Wordsize_64.

Strategy opaque [Wordsize_64.wordsize].

Module Int64.

Include Make(Wordsize_64).


Definition iwordsize': Int.int := Int.repr zwordsize.

Definition shl' (x: int) (y: Int.int): int :=
  repr (Z.shiftl (unsigned x) (Int.unsigned y)).
Definition shru' (x: int) (y: Int.int): int :=
  repr (Z.shiftr (unsigned x) (Int.unsigned y)).
Definition shr' (x: int) (y: Int.int): int :=
  repr (Z.shiftr (signed x) (Int.unsigned y)).
Definition rol' (x: int) (y: Int.int): int :=
  rol x (repr (Int.unsigned y)).
Definition shrx' (x: int) (y: Int.int): int :=
  divs x (shl' one y).
Definition shr_carry' (x: int) (y: Int.int): int :=
  if lt x zero && negb (eq (and x (sub (shl' one y) one)) zero)
  then one else zero.

Lemma bits_shl':
  forall x y i,
  0 <= i < zwordsize ->
  testbit (shl' x y) i =
  if zlt i (Int.unsigned y) then false else testbit x (i - Int.unsigned y).

Lemma bits_shru':
  forall x y i,
  0 <= i < zwordsize ->
  testbit (shru' x y) i =
  if zlt (i + Int.unsigned y) zwordsize then testbit x (i + Int.unsigned y) else false.

Lemma bits_shr':
  forall x y i,
  0 <= i < zwordsize ->
  testbit (shr' x y) i =
  testbit x (if zlt (i + Int.unsigned y) zwordsize then i + Int.unsigned y else zwordsize - 1).

Lemma shl'_mul_two_p:
  forall x y,
  shl' x y = mul x (repr (two_p (Int.unsigned y))).

Lemma shl'_one_two_p:
  forall y, shl' one y = repr (two_p (Int.unsigned y)).

Theorem shl'_mul:
  forall x y,
  shl' x y = mul x (shl' one y).

Theorem shl'_zero:
  forall x, shl' x Int.zero = x.

Theorem shru'_zero :
  forall x, shru' x Int.zero = x.

Theorem shr'_zero :
  forall x, shr' x Int.zero = x.

Theorem shrx'_zero:
  forall x, shrx' x Int.zero = x.

Theorem shrx'_carry:
  forall x y,
  Int.ltu y (Int.repr 63) = true ->
  shrx' x y = add (shr' x y) (shr_carry' x y).

Theorem shrx'_shr_2:
  forall x y,
  Int.ltu y (Int.repr 63) = true ->
  shrx' x y = shr' (add x (shru' (shr' x (Int.repr 63)) (Int.sub (Int.repr 64) y))) y.

Lemma shr'63:
  forall x, (shr' x (Int.repr 63)) = if lt x zero then mone else zero.

Lemma shru'63:
  forall x, (shru' x (Int.repr 63)) = if lt x zero then one else zero.
  
Theorem shrx'1_shr':
  forall x,
  Int.ltu Int.one (Int.repr (zwordsize - 1)) = true ->
  shrx' x (Int.repr 1) = shr' (add x (shru' x (Int.repr (Int64.zwordsize - 1)))) (Int.repr 1).

Remark int_ltu_2_inv:
  forall y z,
  Int.ltu y iwordsize' = true ->
  Int.ltu z iwordsize' = true ->
  Int.unsigned (Int.add y z) <= Int.unsigned iwordsize' ->
  let y' := repr (Int.unsigned y) in
  let z' := repr (Int.unsigned z) in
     Int.unsigned y = unsigned y'
  /\ Int.unsigned z = unsigned z'
  /\ ltu y' iwordsize = true
  /\ ltu z' iwordsize = true
  /\ Int.unsigned (Int.add y z) = unsigned (add y' z')
  /\ add y' z' = repr (Int.unsigned (Int.add y z)).

Theorem or_ror':
  forall x y z,
  Int.ltu y iwordsize' = true ->
  Int.ltu z iwordsize' = true ->
  Int.add y z = iwordsize' ->
  ror x (repr (Int.unsigned z)) = or (shl' x y) (shru' x z).

Theorem shl'_shl':
  forall x y z,
  Int.ltu y iwordsize' = true ->
  Int.ltu z iwordsize' = true ->
  Int.ltu (Int.add y z) iwordsize' = true ->
  shl' (shl' x y) z = shl' x (Int.add y z).

Theorem shru'_shru':
  forall x y z,
  Int.ltu y iwordsize' = true ->
  Int.ltu z iwordsize' = true ->
  Int.ltu (Int.add y z) iwordsize' = true ->
  shru' (shru' x y) z = shru' x (Int.add y z).

Theorem shr'_shr':
  forall x y z,
  Int.ltu y iwordsize' = true ->
  Int.ltu z iwordsize' = true ->
  Int.ltu (Int.add y z) iwordsize' = true ->
  shr' (shr' x y) z = shr' x (Int.add y z).

Theorem shru'_shl':
  forall x y z, Int.ltu y iwordsize' = true -> Int.ltu z iwordsize' = true ->
  shru' (shl' x y) z =
  if Int.ltu z y then shl' (zero_ext (zwordsize - Int.unsigned y) x) (Int.sub y z)
                 else zero_ext (zwordsize - Int.unsigned z) (shru' x (Int.sub z y)).

Theorem shr'_shl':
  forall x y z, Int.ltu y iwordsize' = true -> Int.ltu z iwordsize' = true ->
  shr' (shl' x y) z =
  if Int.ltu z y then shl' (sign_ext (zwordsize - Int.unsigned y) x) (Int.sub y z)
                 else sign_ext (zwordsize - Int.unsigned z) (shr' x (Int.sub z y)).

Lemma shl'_zero_ext:
  forall n m x, 0 <= n ->
  shl' (zero_ext n x) m = zero_ext (n + Int.unsigned m) (shl' x m).

Lemma shl'_sign_ext:
  forall n m x, 0 < n ->
  shl' (sign_ext n x) m = sign_ext (n + Int.unsigned m) (shl' x m).

Lemma shru'_zero_ext:
  forall n m x, 0 <= n ->
  shru' (zero_ext (n + Int.unsigned m) x) m = zero_ext n (shru' x m).

Lemma shru'_zero_ext_0:
  forall n m x, n <= Int.unsigned m ->
  shru' (zero_ext n x) m = zero.

Lemma shr'_sign_ext:
  forall n m x, 0 < n -> n + Int.unsigned m < zwordsize ->
  shr' (sign_ext (n + Int.unsigned m) x) m = sign_ext n (shr' x m).

Lemma zero_ext_shru'_min:
  forall s x n, Int.ltu n iwordsize' = true ->
  zero_ext s (shru' x n) = zero_ext (Z.min s (zwordsize - Int.unsigned n)) (shru' x n).

Lemma sign_ext_shr'_min:
  forall s x n, Int.ltu n iwordsize' = true ->
  sign_ext s (shr' x n) = sign_ext (Z.min s (zwordsize - Int.unsigned n)) (shr' x n).

Lemma shl'_zero_ext_min:
  forall s x n, Int.ltu n iwordsize' = true ->
  shl' (zero_ext s x) n = shl' (zero_ext (Z.min s (zwordsize - Int.unsigned n)) x) n.

Lemma shl'_sign_ext_min:
  forall s x n, Int.ltu n iwordsize' = true ->
  shl' (sign_ext s x) n = shl' (sign_ext (Z.min s (zwordsize - Int.unsigned n)) x) n.


Lemma nonneg_shrx'_is_shru':
  forall x (xRANGE : signed x >= 0) n,
    shrx' x n = shru' x n.


Definition one_bits' (x: int) : list Int.int :=
  List.map Int.repr (Z_one_bits wordsize (unsigned x) 0).

Definition is_power2' (x: int) : option Int.int :=
  match Z_one_bits wordsize (unsigned x) 0 with
  | i :: nil => Some (Int.repr i)
  | _ => None
  end.

Theorem one_bits'_range:
  forall x i, In i (one_bits' x) -> Int.ltu i iwordsize' = true.

Fixpoint int_of_one_bits' (l: list Int.int) : int :=
  match l with
  | nil => zero
  | a :: b => add (shl' one a) (int_of_one_bits' b)
  end.

Theorem one_bits'_decomp:
  forall x, x = int_of_one_bits' (one_bits' x).

Lemma is_power2'_rng:
  forall n logn,
  is_power2' n = Some logn ->
  0 <= Int.unsigned logn < zwordsize.

Theorem is_power2'_range:
  forall n logn,
  is_power2' n = Some logn -> Int.ltu logn iwordsize' = true.

Lemma is_power2'_correct:
  forall n logn,
  is_power2' n = Some logn ->
  unsigned n = two_p (Int.unsigned logn).

Theorem mul_pow2':
  forall x n logn,
  is_power2' n = Some logn ->
  mul x n = shl' x logn.

Theorem divu_pow2':
  forall x n logn,
  is_power2' n = Some logn ->
  divu x n = shru' x logn.


Definition loword (n: int) : Int.int := Int.repr (unsigned n).

Definition hiword (n: int) : Int.int := Int.repr (unsigned (shru n (repr Int.zwordsize))).

Definition ofwords (hi lo: Int.int) : int :=
  or (shl (repr (Int.unsigned hi)) (repr Int.zwordsize)) (repr (Int.unsigned lo)).

Lemma bits_loword:
  forall n i, 0 <= i < Int.zwordsize -> Int.testbit (loword n) i = testbit n i.

Lemma bits_hiword:
  forall n i, 0 <= i < Int.zwordsize -> Int.testbit (hiword n) i = testbit n (i + Int.zwordsize).

Lemma bits_ofwords:
  forall hi lo i, 0 <= i < zwordsize ->
  testbit (ofwords hi lo) i =
  if zlt i Int.zwordsize then Int.testbit lo i else Int.testbit hi (i - Int.zwordsize).

Lemma lo_ofwords:
  forall hi lo, loword (ofwords hi lo) = lo.

Lemma hi_ofwords:
  forall hi lo, hiword (ofwords hi lo) = hi.

Lemma ofwords_recompose:
  forall n, ofwords (hiword n) (loword n) = n.

Lemma ofwords_add:
  forall lo hi, ofwords hi lo = repr (Int.unsigned hi * two_p 32 + Int.unsigned lo).

Lemma ofwords_add':
  forall lo hi, unsigned (ofwords hi lo) = Int.unsigned hi * two_p 32 + Int.unsigned lo.

Remark eqm_mul_2p32:
  forall x y, Int.eqm x y -> eqm (x * two_p 32) (y * two_p 32).

Lemma ofwords_add'':
  forall lo hi, signed (ofwords hi lo) = Int.signed hi * two_p 32 + Int.unsigned lo.


Lemma decompose_bitwise_binop:
  forall f f64 f32 xh xl yh yl,
  (forall x y i, 0 <= i < zwordsize -> testbit (f64 x y) i = f (testbit x i) (testbit y i)) ->
  (forall x y i, 0 <= i < Int.zwordsize -> Int.testbit (f32 x y) i = f (Int.testbit x i) (Int.testbit y i)) ->
  f64 (ofwords xh xl) (ofwords yh yl) = ofwords (f32 xh yh) (f32 xl yl).

Lemma decompose_and:
  forall xh xl yh yl,
  and (ofwords xh xl) (ofwords yh yl) = ofwords (Int.and xh yh) (Int.and xl yl).

Lemma decompose_or:
  forall xh xl yh yl,
  or (ofwords xh xl) (ofwords yh yl) = ofwords (Int.or xh yh) (Int.or xl yl).

Lemma decompose_xor:
  forall xh xl yh yl,
  xor (ofwords xh xl) (ofwords yh yl) = ofwords (Int.xor xh yh) (Int.xor xl yl).

Lemma decompose_not:
  forall xh xl,
  not (ofwords xh xl) = ofwords (Int.not xh) (Int.not xl).

Lemma decompose_shl_1:
  forall xh xl y,
  0 <= Int.unsigned y < Int.zwordsize ->
  shl' (ofwords xh xl) y =
  ofwords (Int.or (Int.shl xh y) (Int.shru xl (Int.sub Int.iwordsize y)))
          (Int.shl xl y).

Lemma decompose_shl_2:
  forall xh xl y,
  Int.zwordsize <= Int.unsigned y < zwordsize ->
  shl' (ofwords xh xl) y =
  ofwords (Int.shl xl (Int.sub y Int.iwordsize)) Int.zero.

Lemma decompose_shru_1:
  forall xh xl y,
  0 <= Int.unsigned y < Int.zwordsize ->
  shru' (ofwords xh xl) y =
  ofwords (Int.shru xh y)
          (Int.or (Int.shru xl y) (Int.shl xh (Int.sub Int.iwordsize y))).

Lemma decompose_shru_2:
  forall xh xl y,
  Int.zwordsize <= Int.unsigned y < zwordsize ->
  shru' (ofwords xh xl) y =
  ofwords Int.zero (Int.shru xh (Int.sub y Int.iwordsize)).

Lemma decompose_shr_1:
  forall xh xl y,
  0 <= Int.unsigned y < Int.zwordsize ->
  shr' (ofwords xh xl) y =
  ofwords (Int.shr xh y)
          (Int.or (Int.shru xl y) (Int.shl xh (Int.sub Int.iwordsize y))).

Lemma decompose_shr_2:
  forall xh xl y,
  Int.zwordsize <= Int.unsigned y < zwordsize ->
  shr' (ofwords xh xl) y =
  ofwords (Int.shr xh (Int.sub Int.iwordsize Int.one))
          (Int.shr xh (Int.sub y Int.iwordsize)).

Lemma decompose_add:
  forall xh xl yh yl,
  add (ofwords xh xl) (ofwords yh yl) =
  ofwords (Int.add (Int.add xh yh) (Int.add_carry xl yl Int.zero))
          (Int.add xl yl).

Lemma decompose_sub:
  forall xh xl yh yl,
  sub (ofwords xh xl) (ofwords yh yl) =
  ofwords (Int.sub (Int.sub xh yh) (Int.sub_borrow xl yl Int.zero))
          (Int.sub xl yl).

Lemma decompose_sub':
  forall xh xl yh yl,
  sub (ofwords xh xl) (ofwords yh yl) =
  ofwords (Int.add (Int.add xh (Int.not yh)) (Int.add_carry xl (Int.not yl) Int.one))
          (Int.sub xl yl).

Definition mul' (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y).

Lemma mul'_mulhu:
  forall x y, mul' x y = ofwords (Int.mulhu x y) (Int.mul x y).

Lemma decompose_mul:
  forall xh xl yh yl,
  mul (ofwords xh xl) (ofwords yh yl) =
  ofwords (Int.add (Int.add (hiword (mul' xl yl)) (Int.mul xl yh)) (Int.mul xh yl))
          (loword (mul' xl yl)).

Lemma decompose_mul_2:
  forall xh xl yh yl,
  mul (ofwords xh xl) (ofwords yh yl) =
  ofwords (Int.add (Int.add (Int.mulhu xl yl) (Int.mul xl yh)) (Int.mul xh yl))
          (Int.mul xl yl).

Lemma decompose_ltu:
  forall xh xl yh yl,
  ltu (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.ltu xh yh.

Lemma decompose_leu:
  forall xh xl yh yl,
  negb (ltu (ofwords yh yl) (ofwords xh xl)) =
  if Int.eq xh yh then negb (Int.ltu yl xl) else Int.ltu xh yh.

Lemma decompose_lt:
  forall xh xl yh yl,
  lt (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.lt xh yh.

Lemma decompose_le:
  forall xh xl yh yl,
  negb (lt (ofwords yh yl) (ofwords xh xl)) =
  if Int.eq xh yh then negb (Int.ltu yl xl) else Int.lt xh yh.


Remark int_unsigned_range:
  forall x, 0 <= Int.unsigned x <= max_unsigned.

Remark int_unsigned_repr:
  forall x, unsigned (repr (Int.unsigned x)) = Int.unsigned x.

Lemma int_sub_ltu:
  forall x y,
    Int.ltu x y= true ->
    Int.unsigned (Int.sub y x) = unsigned (sub (repr (Int.unsigned y)) (repr (Int.unsigned x))).

End Int64.

Strategy 0 [Wordsize_64.wordsize].

Definition int_eq: forall (i1 i2: int), {i1=i2} + {i1<>i2}.

Notation int64 := Int64.int.

Definition int64_eq: forall (i1 i2: int64), {i1=i2} + {i1<>i2}.

Global Opaque Int.repr Int64.repr Byte.repr.

Specialization to offsets in pointer values

Module Wordsize_Ptrofs.
  Definition wordsize := if Archi.ptr64 then 64%nat else 32%nat.
  Remark wordsize_not_zero: wordsize <> 0%nat.
End Wordsize_Ptrofs.

Strategy opaque [Wordsize_Ptrofs.wordsize].

Module Ptrofs.

Include Make(Wordsize_Ptrofs).

Definition to_int (x: int): Int.int := Int.repr (unsigned x).

Definition to_int64 (x: int): Int64.int := Int64.repr (unsigned x).

Definition of_int (x: Int.int) : int := repr (Int.unsigned x).

Definition of_intu := of_int.

Definition of_ints (x: Int.int) : int := repr (Int.signed x).

Definition of_int64 (x: Int64.int) : int := repr (Int64.unsigned x).

Definition of_int64u := of_int64.

Definition of_int64s (x: Int64.int) : int := repr (Int64.signed x).

Section AGREE32.

Hypothesis _32: Archi.ptr64 = false.

Lemma modulus_eq32: modulus = Int.modulus.

Lemma eqm32:
  forall x y, Int.eqm x y <-> eqm x y.

Definition agree32 (a: Ptrofs.int) (b: Int.int) : Prop :=
  Ptrofs.unsigned a = Int.unsigned b.

Lemma agree32_repr:
  forall i, agree32 (Ptrofs.repr i) (Int.repr i).

Lemma agree32_signed:
  forall a b, agree32 a b -> Ptrofs.signed a = Int.signed b.

Lemma agree32_of_int:
  forall b, agree32 (of_int b) b.

Lemma agree32_of_ints:
  forall b, agree32 (of_ints b) b.

Lemma agree32_of_int_eq:
  forall a b, agree32 a b -> of_int b = a.

Lemma agree32_of_ints_eq:
  forall a b, agree32 a b -> of_ints b = a.

Lemma agree32_to_int:
  forall a, agree32 a (to_int a).

Lemma agree32_to_int_eq:
  forall a b, agree32 a b -> to_int a = b.

Lemma agree32_neg:
  forall a1 b1, agree32 a1 b1 -> agree32 (Ptrofs.neg a1) (Int.neg b1).

Lemma agree32_add:
  forall a1 b1 a2 b2,
  agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.add a1 a2) (Int.add b1 b2).

Lemma agree32_sub:
  forall a1 b1 a2 b2,
  agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.sub a1 a2) (Int.sub b1 b2).

Lemma agree32_mul:
  forall a1 b1 a2 b2,
  agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.mul a1 a2) (Int.mul b1 b2).

Lemma agree32_divs:
  forall a1 b1 a2 b2,
  agree32 a1 b1 -> agree32 a2 b2 -> agree32 (Ptrofs.divs a1 a2) (Int.divs b1 b2).

Lemma of_int_to_int:
  forall n, of_int (to_int n) = n.

Lemma to_int_of_int:
  forall n, to_int (of_int n) = n.

End AGREE32.

Section AGREE64.

Hypothesis _64: Archi.ptr64 = true.

Lemma modulus_eq64: modulus = Int64.modulus.

Lemma eqm64:
  forall x y, Int64.eqm x y <-> eqm x y.

Definition agree64 (a: Ptrofs.int) (b: Int64.int) : Prop :=
  Ptrofs.unsigned a = Int64.unsigned b.

Lemma agree64_repr:
  forall i, agree64 (Ptrofs.repr i) (Int64.repr i).

Lemma agree64_signed:
  forall a b, agree64 a b -> Ptrofs.signed a = Int64.signed b.

Lemma agree64_of_int:
  forall b, agree64 (of_int64 b) b.

Lemma agree64_of_int_eq:
  forall a b, agree64 a b -> of_int64 b = a.

Lemma agree64_to_int:
  forall a, agree64 a (to_int64 a).

Lemma agree64_to_int_eq:
  forall a b, agree64 a b -> to_int64 a = b.

Lemma agree64_neg:
  forall a1 b1, agree64 a1 b1 -> agree64 (Ptrofs.neg a1) (Int64.neg b1).

Lemma agree64_add:
  forall a1 b1 a2 b2,
  agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.add a1 a2) (Int64.add b1 b2).

Lemma agree64_sub:
  forall a1 b1 a2 b2,
  agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.sub a1 a2) (Int64.sub b1 b2).

Lemma agree64_mul:
  forall a1 b1 a2 b2,
  agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.mul a1 a2) (Int64.mul b1 b2).

Lemma agree64_divs:
  forall a1 b1 a2 b2,
  agree64 a1 b1 -> agree64 a2 b2 -> agree64 (Ptrofs.divs a1 a2) (Int64.divs b1 b2).

Lemma of_int64_to_int64:
  forall n, of_int64 (to_int64 n) = n.

Lemma to_int64_of_int64:
  forall n, to_int64 (of_int64 n) = n.

End AGREE64.

Global Hint Resolve
  agree32_repr agree32_of_int agree32_of_ints agree32_of_int_eq agree32_of_ints_eq
  agree32_to_int agree32_to_int_eq agree32_neg agree32_add agree32_sub agree32_mul agree32_divs
  agree64_repr agree64_of_int agree64_of_int_eq
  agree64_to_int agree64_to_int_eq agree64_neg agree64_add agree64_sub agree64_mul agree64_divs : ptrofs.

End Ptrofs.

Strategy 0 [Wordsize_Ptrofs.wordsize].

Notation ptrofs := Ptrofs.int.

Definition ptrofs_eq: forall (i1 i2: ptrofs), {i1=i2} + {i1<>i2}.

Global Opaque Ptrofs.repr.

Global Hint Resolve
  Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans
  Int.eqm_small_eq Int.eqm_add Int.eqm_neg Int.eqm_sub Int.eqm_mult
  Int.eqm_unsigned_repr Int.eqm_unsigned_repr_l Int.eqm_unsigned_repr_r
  Int.unsigned_range Int.unsigned_range_2
  Int.repr_unsigned Int.repr_signed Int.unsigned_repr : ints.

Global Hint Resolve
  Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans
  Int64.eqm_small_eq Int64.eqm_add Int64.eqm_neg Int64.eqm_sub Int64.eqm_mult
  Int64.eqm_unsigned_repr Int64.eqm_unsigned_repr_l Int64.eqm_unsigned_repr_r
  Int64.unsigned_range Int64.unsigned_range_2
  Int64.repr_unsigned Int64.repr_signed Int64.unsigned_repr : ints.

Global Hint Resolve
  Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans
  Ptrofs.eqm_small_eq Ptrofs.eqm_add Ptrofs.eqm_neg Ptrofs.eqm_sub Ptrofs.eqm_mult
  Ptrofs.eqm_unsigned_repr Ptrofs.eqm_unsigned_repr_l Ptrofs.eqm_unsigned_repr_r
  Ptrofs.unsigned_range Ptrofs.unsigned_range_2
  Ptrofs.repr_unsigned Ptrofs.repr_signed Ptrofs.unsigned_repr : ints.