Library Stdlib.Zmod.Bits

From Stdlib Require Import ZArith ZModOffset Zcong Lia.
From Stdlib Require Import Bool.Bool Lists.List Sorting.Permutation.
Import ListNotations.

From Stdlib Require Export Zmod.ZmodDef Zmod.ZmodBase.
Local Open Scope Z_scope.
Local Coercion ZmodDef.Zmod.to_Z : Zmod >-> Z.

Local Hint Extern 0 (?x <-> ?x) => reflexivity : core.

Module bits.
Import ZmodDef.Zmod ZmodBase.Zmod ZmodDef.bits.

Notation to_Z_0 := to_Z_0 (only parsing).
Notation unsigned_0 := unsigned_0 (only parsing).

Lemma unsigned_1 [n : Z] (Hm : 1 <= n) : @to_Z (2^n) one = 1.
Notation to_Z_1 := unsigned_1 (only parsing).

Lemma signed_1 [n] (Hm : 2 <= n) : @signed (2^n) one = 1.

Lemma unsigned_m1 n : @to_Z (2^n) (opp one) = Z.ones n.
Notation to_Z_m1 := unsigned_m1 (only parsing).

Lemma signed_m1 [n] (Hm : 1 <= n) : @signed (2^n) (opp one) = -1.

Lemma one_neq_zero [n] (Hm : 1 <= n) : one <> zero :> bits n.

Lemma unsigned_of_Z [n] (z : Z) : to_Z (of_Z n z) = z mod 2^n.
Notation to_Z_of_Z := unsigned_of_Z.

Lemma unsigned_of_Z_small [n] z (H : 0 <= z < 2^n) : to_Z (bits.of_Z n z) = z.
Notation to_Z_of_Z_small := unsigned_of_Z_small (only parsing).

Lemma unsigned_of_Z_mod0 [n] (Hn : n < 0) x : unsigned (of_Z n x) = x.

Lemma unsigned_width [n] (Hn : 0 <= n) : unsigned (bits.of_Z n n) = n.
Notation to_Z_width := unsigned_width.

Lemma unsigned_range [n] (x : bits n) (Hn : 0 <= n) : 0 <= x < 2^n.
Notation to_Z_range := unsigned_range.

Lemma signed_of_Z [n] z : signed (of_Z n z) = Z.smodulo z (2^n).

Lemma signed_range [n] (x : bits n) (Hn : 0 <= n) : -2^n <= 2*signed x < 2^n.

Lemma signed_range' [n] (x : bits n) (Hn : 1 <= n) : -2^(n-1) <= signed x < 2^(n-1).

Lemma unsigned_width0 (a : bits 0) : to_Z a = 0.
Notation to_Z_width0 := unsigned_width0 (only parsing).

Lemma signed_width0 (a : bits 0) : signed a = 0.

Lemma of_Z_mod [n] x : bits.of_Z n (x mod 2^n) = bits.of_Z n x.

Lemma of_Z_inj [n] x y : bits.of_Z n x = bits.of_Z n y <-> x mod 2^n = y mod 2^n.

Lemma mod_to_Z [n] (x : bits n) : to_Z x mod 2^n = to_Z x.

Lemma mod_signed [n] (x : bits n) : signed x mod 2^n = unsigned x.

Lemma smod_unsigned [n] (x : bits n) : Z.smodulo (unsigned x) (2^n) = signed x.

Lemma smod_signed [n] (x : bits n) : Z.smodulo (signed x) (2^n) = signed x.

Lemma signed_small [n] (x : bits n) (H : 0 <= 2*x < 2^n) : signed x = unsigned x.

Lemma signed_large [n] (x : bits n) (H : 2^n <= 2*x) : signed x = x-2^n.

Lemma signed_neg_iff [n] (x : bits n) (Hn : 0 <= n) :
  signed x < 0 <-> 2^n <= 2 * unsigned x.

Lemma signed_small_iff [n] (x : bits n) (Hn : 0 <= n) :
  signed x = unsigned x <-> 2 * unsigned x < 2^n.

Lemma signed_nonneg_iff [n] (x : bits n) (Hn : 0 <= n) :
  0 <= signed x <-> 2 * unsigned x < 2^n.

Lemma signed_pos_iff [n] (x : bits n) (Hn : 0 <= n) :
  0 < signed x <-> 0 < 2 * unsigned x < 2^n.

Lemma unsigned_opp [n] (x : bits n) : to_Z (opp x) = (- to_Z x) mod 2^n.
Notation to_Z_opp := unsigned_opp (only parsing).
Lemma signed_opp [n] (x : bits n) : signed (opp x) = Z.smodulo (-signed x) (2^n).
Lemma unsigned_add [n] (x y : bits n) : to_Z (add x y) = (to_Z x + to_Z y) mod 2^n.
Notation to_Z_add := unsigned_add (only parsing).
Lemma signed_add [n] (x y : bits n) : signed (add x y) = Z.smodulo (signed x+signed y) (2^n).
Lemma unsigned_sub [n] (x y : bits n) : to_Z (sub x y) = (to_Z x - to_Z y) mod 2^n.
Notation to_Z_sub := unsigned_sub (only parsing).
Lemma signed_sub [n] (x y : bits n) : signed (sub x y) = Z.smodulo (signed x-signed y) (2^n).
Lemma unsigned_mul [n] (x y : bits n) : to_Z (mul x y) = (to_Z x * to_Z y) mod 2^n.
Notation to_Z_mul := unsigned_mul (only parsing).
Lemma signed_mul [n] (x y : bits n) : signed (mul x y) = Z.smodulo (signed x*signed y) (2^n).
Lemma unsigned_slu [n] (x : bits n) y : to_Z (slu x y) = Z.shiftl x y mod 2^n.
Notation to_Z_slu := unsigned_slu (only parsing).
Lemma unsigned_srs [n] (x : bits n) y (Hy : 0 <= y) : to_Z (srs x y) = Z.shiftr (signed x) y mod 2^n.
Notation to_Z_srs := unsigned_srs (only parsing).
Lemma signed_srs [n] (x : bits n) y (Hy : 0 <= y) : signed (srs x y) = Z.shiftr (signed x) y.
Lemma of_Z_div [n] (x y : Z) (Hx : 0 <= x < 2^n) (Hy : 0 < y < 2^n) :
  bits.of_Z n (x / y) = udiv (of_Z _ x) (of_Z _ y).
Lemma of_Z_umod [n] (x y : Z) (Hx : 0 <= x < 2^n) (Hy : 0 <= y < 2^n) :
  bits.of_Z n (x mod y) = umod (of_Z _ x) (of_Z _ y).
Lemma unsigned_mdiv [n] (x y : bits n) : to_Z (mdiv x y) = x * Z.invmod y (2^n) mod 2^n.
Notation to_Z_mdiv := unsigned_mdiv (only parsing).
Lemma unsigned_pow_nonneg_r [n] (x : bits n) z (Hz : 0 <= z) : to_Z (pow x z) = x^z mod 2^n.
Notation to_Z_pow_nonneg := unsigned_pow_nonneg_r (only parsing).
Lemma signed_pow_nonneg_r [n] (x z : bits n) (Hz : 0 <= z) : signed (pow x z) = Z.smodulo (signed x ^ z) (2^n).
Notation signed_pow_nonneg := signed_pow_nonneg_r.

Lemma of_Z_nz [n] (x : bits n) (H : (x mod 2^n <> 0)%Z) : bits.of_Z n x <> zero.

Lemma opp_overflow [n] (x : bits n) (Hn : 0 <= n) (Hx : signed x = -2^(n-1)) : opp x = x.

Lemma abs_overflow [n] (x : bits n) (Hn : 0 <= n) (Hx : signed x = -2^(n-1)) : abs x = x.

Lemma squot_overflow [n] (x y : bits n) (Hn : 0 <= n) (Hx : signed x = -2^(n-1)) (Hy : signed y = -1) :
  squot x y = x.

Lemma signed_squot_small [n] (x y : bits n) (Hn : 0 <= n) (Hy : signed y <> 0) :
  ~ (signed x = -2^(n-1) /\ signed y = -1) ->
  signed (squot x y) = signed x ÷ signed y.

Lemma signed_srem [n] (x y : bits n) : signed (srem x y) = Z.smodulo (Z.rem (signed x) (signed y)) (2^n).

Lemma signed_squot [n] (x y : bits n) : signed (squot x y) =
  Z.smodulo (if signed y =? 0 then -1 else signed x ÷ signed y) (2^n).

Lemma signed_squot_nz [n] (x y : bits n) : signed y <> 0 -> signed (squot x y) = Z.smodulo (signed x ÷ signed y) (2^n).

Lemma testbit_high [n] (x : bits n) i (Hn : 0 <= n) (Hi : (n <= i)%Z) : Z.testbit x i = false.

Lemma testbit_m1 [n] i (Hn : 0 <= n) : Z.testbit (@Zmod.opp (2^n) one) i = (0 <=? i) && (i <? n).

Lemma testbit_sign [n] (x : bits n) (Hn : 0 <= n) : Z.testbit x (n-1) = (signed x <? 0).

Lemma testbit_signed_high [n] (x : bits n) i (Hn : 0 <= n) (Hi : (n <= i)%Z) :
  Z.testbit (signed x) i = (signed x <? 0).

Lemma unsigned_and [n] (x y : bits n) : unsigned (and x y) = Z.land x y.

Lemma unsigned_or [n] (x y : bits n) : to_Z (or x y) = Z.lor x y.
Notation to_Z_or := unsigned_or (only parsing).

Lemma unsigned_xor [n] (x y : bits n) : to_Z (xor x y) = Z.lxor x y.
Notation to_Z_xor := unsigned_xor (only parsing).

Lemma xor_zero_iff [n] (x y : bits n) : xor x y = zero <-> x = y.

Lemma eqb_xor_zero [n] (x y : bits n) : eqb (xor x y) zero = eqb x y.

Module Z.
Lemma ones_neg n (Hn : n < 0) : Z.ones n = -1.
End Z.

Lemma unsigned_not [n] (x : bits n) : to_Z (not x) = Z.ldiff (Z.ones n) x.
Local Notation to_Z_not := unsigned_not (only parsing).

Lemma unsigned_not' [n] (x : bits n) : to_Z (not x) = Z.ones n - x.
Local Notation to_Z_not' := unsigned_not' (only parsing).

Lemma of_Z_lnot [n] z : bits.of_Z n (Z.lnot z) = not (bits.of_Z n z).

Lemma not_not [n] (x : bits n) : not (not x) = x.

Lemma not_0 n : not zero = opp one :> bits n.

Lemma not_m1 n : not (opp one) = zero :> bits n.

Lemma unsigned_app [n m] a b (Hn : 0 <= n) (Hm : 0 <= m) :
  to_Z (@app n m a b) = Z.lor a (Z.shiftl b n).
Notation to_Z_app := unsigned_app (only parsing).

Lemma unsigned_firstn [n m] a : to_Z (@firstn n m a) = a mod 2^n.
Notation to_Z_firstn := unsigned_firstn (only parsing).

Lemma unsigned_skipn [n m] a (Hn : 0 <= n) : to_Z (@skipn n m a) = a/2^n.
Notation to_Z_skipn := unsigned_skipn (only parsing).

Lemma unsigned_slice start pastend [w] (a : bits w) (H : 0 <= start <= pastend) :
  to_Z (slice start pastend a) = a/2^start mod 2^(pastend-start).
Notation to_Z_slice := unsigned_slice (only parsing).

Lemma firstn_app [n m] a b (Hn : 0 <= n) (Hm : 0 <= m) :
  firstn n (@app n m a b) = a.

Lemma skipn_app_dep [n m] a b (Hn : 0 <= n) (Hm : 0 <= m) :
  existT _ _ (skipn n (@app n m a b)) = existT _ _ b.

Lemma skipn_app_ex [n m] a b (Hn : 0 <= n) (Hm : 0 <= m) :
  exists pf, skipn n (@app n m a b) = eq_rect _ Zmod b _ pf.

Lemma skipn_app [n m] a b (Hn : 0 <= n) (Hm : 0 <= m) :
  skipn n (@app n m a b) = of_Z _ (to_Z (skipn n (@app n m a b))).

Lemma app_assoc_dep [n m l] (a : bits n) (b : bits m) (c : bits l)
  (Hn : 0 <= n) (Hm : 0 <= m) (Hl : 0 <= l) :
  existT _ _ (app a (app b c)) = existT _ _ (app (app a b) c).

Lemma app_assoc_ex [n m l] (a : bits n) (b : bits m) (c : bits l)
  (Hn : 0 <= n) (Hm : 0 <= m) (Hl : 0 <= l) :
  exists pf, app a (app b c) = eq_rect _ _ (app (app a b) c) _ pf.

Lemma app_assoc [n m l] (a : bits n) (b : bits m) (c : bits l)
  (Hn : 0 <= n) (Hm : 0 <= m) (Hl : 0 <= l) :
  app a (app b c) = of_Z _ (to_Z (app (app a b) c)).

End bits.