Add little endian encoding of Z

theories/list_numbers.v

@@ -26,6 +26,24 @@ Definition max_list_with {A} (f : A → nat) : list A → nat :=
   end.
 Notation max_list := (max_list_with id).
 
+(** ** Conversion of integers to and from little endian *)
+(** [Z_to_little_endian m n z] converts [z] into a list of [m] [n]-bit
+integers in the little endian format. *)
+Fixpoint Z_to_little_endian (m : nat) (n : Z) (z : Z) : list Z :=
+  match m with
+  | O => []
+  | S m' => Z.land z (Z.ones n) :: Z_to_little_endian m' n (z ≫ n)
+  end.
+
+(** [Z_of_little_endian n bs] converts the list [bs] of [n]-bit integers into
+a number by interpreting [bs] as the little endian encoding. *)
+Fixpoint Z_of_little_endian (n : Z) (bs : list Z) : Z :=
+  match bs with
+  | [] => 0
+  | b :: bs => Z.lor b (Z_of_little_endian n bs ≪ n)
+  end.
+
+
 (** * Properties *)
 (** ** Properties of the [seq] function *)
 Section seq.
@@ -192,3 +210,77 @@ Section sum_list.
     n ∈ ns → n ≤ max_list ns.
   Proof. induction 1; simpl; lia. Qed.
 End sum_list.
+
+(** ** Properties of the [Z_to_little_endian] and [Z_of_little_endian] functions *)
+Section Z_little_endian.
+  Local Open Scope Z_scope.
+  Lemma Z_to_of_little_endian m n bs:
+    m = length bs → 0 ≤ n →
+    Forall (λ b, 0 ≤ b < 2 ^ n) bs →
+    Z_to_little_endian m n (Z_of_little_endian n bs) = bs.
+  Proof.
+    intros -> ? Hall. induction Hall as [|b bs ? ? IH]; [done|]; csimpl.
+    f_equal.
+    - apply Z.bits_inj_iff'. intros n' ?.
+      rewrite !Z.land_spec, Z.lor_spec, Z_ones_spec by lia.
+      case_decide.
+      + rewrite andb_true_r, Z.shiftl_spec_low, orb_false_r by lia. done.
+      + rewrite !andb_false_r by lia.
+        symmetry. eapply (Z_bounded_iff_bits_nonneg n); lia.
+    - rewrite <-IH at 3. f_equal.
+      apply Z.bits_inj_iff'. intros n' ?.
+      rewrite Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec by lia.
+      assert (Z.testbit b (n' + n) = false) as ->. {
+        eapply (Z_bounded_iff_bits_nonneg n); lia.
+      }
+      rewrite orb_false_l. f_equal. lia.
+  Qed.
+
+  Lemma Z_of_to_little_endian m n z:
+    0 ≤ n →
+    Z_of_little_endian n (Z_to_little_endian m n z) = z `mod` 2 ^ (m * n).
+  Proof.
+    intros. rewrite <-Z.land_ones by nia.
+    revert z. induction m as [|m IH]; simpl.
+    { intros. Z.bitwise. by rewrite andb_false_r. }
+    intros z. rewrite IH.
+    apply Z.bits_inj_iff'. intros n' ?.
+    rewrite Z.land_spec, Z.lor_spec, Z.shiftl_spec, !Z.land_spec by lia.
+    rewrite (Z_ones_spec n n') by lia. case_bool_decide.
+    - rewrite andb_true_r. rewrite (Z.testbit_neg_r _ (n' - n)), orb_false_r by lia. simpl.
+      rewrite Z_ones_spec by nia. case_bool_decide; [ by rewrite andb_true_r| nia].
+    - rewrite andb_false_r, orb_false_l.
+      rewrite Z.shiftr_spec by lia. f_equal. { f_equal. lia. }
+      rewrite !Z_ones_spec by nia. apply bool_decide_iff. nia.
+  Qed.
+
+  Lemma Z_to_little_endian_bound m n z:
+    0 ≤ n →
+    Forall (λ b, 0 ≤ b < 2 ^ n) (Z_to_little_endian m n z).
+  Proof.
+    intros ?. revert z. induction m as [|m IH]; simpl.
+    { by constructor. }
+    intros ?. constructor; [|by apply IH]. rewrite Z.land_ones by lia.
+    apply Z.mod_pos_bound. apply Z.pow_pos_nonneg; lia.
+  Qed.
+
+  Lemma Z_of_little_endian_bound n bs:
+    0 ≤ n →
+    Forall (λ b, 0 ≤ b < 2 ^ n) bs →
+    0 ≤ Z_of_little_endian n bs < 2 ^ (length bs * n).
+  Proof.
+    intros ? Hall.
+    induction Hall as [|b bs Hb ? IH]; [done|]; simpl.
+    apply Z_bounded_iff_bits_nonneg'; [ nia | |].
+    - apply Z.lor_nonneg. split; [lia|]. apply Z.shiftl_nonneg. lia.
+    - intros l ?. rewrite Z.lor_spec.
+      eapply Z_bounded_iff_bits_nonneg' in Hb.
+      + erewrite Hb, orb_false_l.
+        rewrite Z.shiftl_spec by nia.
+        eapply Z_bounded_iff_bits_nonneg'; [| | done |]; nia.
+      + lia.
+      + lia.
+      + nia.
+  Qed.
+  Local Close Scope Z_scope.
+End Z_little_endian.

theories/numbers.v

@@ -485,6 +485,15 @@ Lemma Zmod_in_range q a c :
   a `mod` c = a - q * c.
 Proof. intros ?. symmetry. apply Z.mod_unique_pos with q; lia. Qed.
 
+Lemma Z_ones_spec n m:
+  0 ≤ m → 0 ≤ n →
+  Z.testbit (Z.ones n) m = bool_decide (m < n).
+Proof.
+  intros. case_bool_decide.
+  - by rewrite Z.ones_spec_low by lia.
+  - by rewrite Z.ones_spec_high by lia.
+Qed.
+
 Lemma Z_bounded_iff_bits_nonneg k n :
   0 ≤ k → 0 ≤ n →
   n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.