Add little endian encoding of Z

theories/list_numbers.v

@@ -26,6 +26,26 @@ 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. A negative [z] is encoded using
+two's-complement. If [z] uses more than [m * n] bits, these additional
+bits are discarded (see [Z_to_little_endian_to_Z]). [m] and [n] should be
+non-negative. *)
+Definition Z_to_little_endian (m n : Z) : Z → list Z :=
+  Z.iter m (λ rec z, Z.land z (Z.ones n) :: rec (z ≫ n)%Z) (λ _, []).
+Global Arguments Z_to_little_endian : simpl never.
+
+(** [little_endian_to_Z n bs] converts the list [bs] of [n]-bit integers
+into a number by interpreting [bs] as the little endian encoding.
+The integers [b] in [bs] should be in the range [0 ≤ b < 2 ^ n]. *)
+Fixpoint little_endian_to_Z (n : Z) (bs : list Z) : Z :=
+  match bs with
+  | [] => 0
+  | b :: bs => Z.lor b (little_endian_to_Z n bs ≪ n)
+  end.
+
+
 (** * Properties *)
 (** ** Properties of the [seq] function *)
 Section seq.
@@ -192,3 +212,94 @@ 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 [little_endian_to_Z] functions *)
+Section Z_little_endian.
+  Local Open Scope Z_scope.
+  Implicit Types m n z : Z.
+
+  Lemma Z_to_little_endian_succ m n z :
+    0 ≤ m →
+    Z_to_little_endian (Z.succ m) n z
+    = Z.land z (Z.ones n) :: Z_to_little_endian m n (z ≫ n).
+  Proof.
+    unfold Z_to_little_endian. intros.
+    by rewrite !iter_nat_of_Z, Zabs2Nat.inj_succ by lia.
+  Qed.
+
+  Lemma Z_to_little_endian_to_Z m n bs:
+    m = Z.of_nat (length bs) → 0 ≤ n →
+    Forall (λ b, 0 ≤ b < 2 ^ n) bs →
+    Z_to_little_endian m n (little_endian_to_Z n bs) = bs.
+  Proof.
+    intros -> ?. induction 1 as [|b bs ? ? IH]; [done|]; simpl.
+    rewrite Nat2Z.inj_succ, Z_to_little_endian_succ by lia. f_equal.
+    - apply Z.bits_inj_iff'. intros z' ?.
+      rewrite !Z.land_spec, Z.lor_spec, Z_ones_spec by lia.
+      case_bool_decide.
+      + rewrite andb_true_r, Z.shiftl_spec_low, orb_false_r by lia. done.
+      + rewrite andb_false_r.
+        symmetry. eapply (Z_bounded_iff_bits_nonneg n); lia.
+    - rewrite <-IH at 3. f_equal.
+      apply Z.bits_inj_iff'. intros z' ?.
+      rewrite Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec by lia.
+      assert (Z.testbit b (z' + n) = false) as ->.
+      { apply (Z_bounded_iff_bits_nonneg n); lia. }
+      rewrite orb_false_l. f_equal. lia.
+  Qed.
+
+  (* TODO: replace the calls to [nia] by [lia] after dropping support for Coq 8.10.2. *)
+  Lemma little_endian_to_Z_to_little_endian m n z:
+    0 ≤ n → 0 ≤ m →
+    little_endian_to_Z n (Z_to_little_endian m n z) = z `mod` 2 ^ (m * n).
+  Proof.
+    intros ? Hm. rewrite <-Z.land_ones by nia.
+    revert z.
+    induction m as [|m ? IH|] using (Z_succ_pred_induction 0); intros z; [..|lia].
+    { Z.bitwise. by rewrite andb_false_r. }
+    rewrite Z_to_little_endian_succ by lia; simpl. rewrite IH by lia.
+    apply Z.bits_inj_iff'. intros z' ?.
+    rewrite Z.land_spec, Z.lor_spec, Z.shiftl_spec, !Z.land_spec by lia.
+    rewrite (Z_ones_spec n z') by lia. case_bool_decide.
+    - rewrite andb_true_r, (Z.testbit_neg_r _ (z' - n)), orb_false_r by lia. simpl.
+      by rewrite Z_ones_spec, bool_decide_true, andb_true_r by 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. lia.
+  Qed.
+
+  Lemma Z_to_little_endian_length m n z :
+    0 ≤ m →
+    Z.of_nat (length (Z_to_little_endian m n z)) = m.
+  Proof.
+    intros. revert z. induction m as [|m ? IH|]
+      using (Z_succ_pred_induction 0); intros z; [done| |lia].
+    rewrite Z_to_little_endian_succ by lia. simpl. by rewrite Nat2Z.inj_succ, IH.
+  Qed.
+
+  Lemma Z_to_little_endian_bound m n z:
+    0 ≤ n → 0 ≤ m →
+    Forall (λ b, 0 ≤ b < 2 ^ n) (Z_to_little_endian m n z).
+  Proof.
+    intros. revert z.
+    induction m as [|m ? IH|] using (Z_succ_pred_induction 0); intros z; [..|lia].
+    { by constructor. }
+    rewrite Z_to_little_endian_succ by lia.
+    constructor; [|by apply IH]. rewrite Z.land_ones by lia.
+    apply Z.mod_pos_bound, Z.pow_pos_nonneg; lia.
+  Qed.
+
+  Lemma little_endian_to_Z_bound n bs:
+    0 ≤ n →
+    Forall (λ b, 0 ≤ b < 2 ^ n) bs →
+    0 ≤ little_endian_to_Z n bs < 2 ^ (Z.of_nat (length bs) * n).
+  Proof.
+    intros ?. induction 1 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 z' ?. rewrite Z.lor_spec.
+    rewrite Z_bounded_iff_bits_nonneg' in Hb by lia.
+    rewrite Hb, orb_false_l, Z.shiftl_spec by nia.
+    apply (Z_bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); nia.
+  Qed.
+End Z_little_endian.