phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp_bitvector/definitions.v *)
Lemma bv_mods_unsigned b1 b2 :
    bv_unsigned (b1 `mods` b2) = bv_wrap n (bv_signed b1 `mod` bv_signed b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_mods_signed b1 b2 :
    bv_signed (b1 `mods` b2) = bv_swrap n (bv_signed b1 `mod` bv_signed b2).
Proof. unfold bv_mods. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_rems_unsigned b1 b2 :
    bv_unsigned (b1 `rems` b2) = bv_wrap n (bv_signed b1 `rem` bv_signed b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_rems_signed b1 b2 :
    bv_signed (b1 `rems` b2) = bv_swrap n (bv_signed b1 `rem` bv_signed b2).
Proof. unfold bv_rems. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_shiftl_unsigned b1 b2 :
    bv_unsigned (b1 ≪ b2) = bv_wrap n (bv_unsigned b1 ≪ bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_shiftl_signed b1 b2 :
    bv_signed (b1 ≪ b2) = bv_swrap n (bv_unsigned b1 ≪ bv_unsigned b2).
Proof. unfold bv_shiftl. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_shiftr_unsigned b1 b2 :
    bv_unsigned (b1 ≫ b2) = bv_unsigned b1 ≫ bv_unsigned b2.
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_shiftr_signed b1 b2 :
    bv_signed (b1 ≫ b2) = bv_swrap n (bv_unsigned b1 ≫ bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_ashiftr_unsigned b1 b2 :
    bv_unsigned (b1 `ashiftr` b2) = bv_wrap n (bv_signed b1 ≫ bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_ashiftr_signed b1 b2 :
    bv_signed (b1 `ashiftr` b2) = bv_swrap n (bv_signed b1 ≫ bv_unsigned b2).
Proof. unfold bv_ashiftr. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_or_unsigned b1 b2 :
    bv_unsigned (bv_or b1 b2) = Z.lor (bv_unsigned b1) (bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_or_signed b1 b2 :
    bv_signed (bv_or b1 b2) = bv_swrap n (Z.lor (bv_unsigned b1) (bv_unsigned b2)).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_and_unsigned b1 b2 :
    bv_unsigned (bv_and b1 b2) = Z.land (bv_unsigned b1) (bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_and_signed b1 b2 :
    bv_signed (bv_and b1 b2) = bv_swrap n (Z.land (bv_unsigned b1) (bv_unsigned b2)).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_xor_unsigned b1 b2 :
    bv_unsigned (bv_xor b1 b2) = Z.lxor (bv_unsigned b1) (bv_unsigned b2).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_xor_signed b1 b2 :
    bv_signed (bv_xor b1 b2) = bv_swrap n (Z.lxor (bv_unsigned b1) (bv_unsigned b2)).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_not_unsigned b :
    bv_unsigned (bv_not b) = bv_wrap n (Z.lnot (bv_unsigned b)).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_not_signed b :
    bv_signed (bv_not b) = bv_swrap n (Z.lnot (bv_unsigned b)).
Proof. unfold bv_not. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_zero_extend_unsigned' z b :
    bv_unsigned (bv_zero_extend z b) = bv_wrap z (bv_unsigned b).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
(* [bv_zero_extend_unsigned] is the version that we want, but it
  only holds with a precondition. *)
Lemma bv_zero_extend_unsigned z b :
    (n ≤ z)%N →
    bv_unsigned (bv_zero_extend z b) = bv_unsigned b.
Proof.
    intros ?. rewrite bv_zero_extend_unsigned', bv_wrap_small; [done|].
    bv_saturate. pose proof (bv_modulus_le_mono n z). lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_zero_extend_signed z b :
    bv_signed (bv_zero_extend z b) = bv_swrap z (bv_unsigned b).
Proof. unfold bv_zero_extend. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_sign_extend_unsigned z b :
    bv_unsigned (bv_sign_extend z b) = bv_wrap z (bv_signed b).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_sign_extend_signed' z b :
    bv_signed (bv_sign_extend z b) = bv_swrap z (bv_signed b).
Proof. unfold bv_sign_extend. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
(* [bv_sign_extend_signed] is the version that we want, but it
  only holds with a precondition. *)
Lemma bv_sign_extend_signed z b :
    (n ≤ z)%N →
    bv_signed (bv_sign_extend z b) = bv_signed b.
Proof.
    intros ?. rewrite bv_sign_extend_signed'.
    destruct (decide (n = 0%N)); subst.
    { by rewrite bv_signed_N_0, bv_swrap_0. }
    apply bv_swrap_small. bv_saturate.
    pose proof bv_half_modulus_le_mono n z. lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_extract_unsigned s l b :
    bv_unsigned (bv_extract s l b) = bv_wrap l (bv_unsigned b ≫ Z.of_N s).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_extract_signed s l b :
    bv_signed (bv_extract s l b) = bv_swrap l (bv_unsigned b ≫ Z.of_N s).
Proof. unfold bv_extract. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_concat_unsigned' m  n2 b1 (b2 : bv n2) :
    bv_unsigned (bv_concat m b1 b2) = bv_wrap m (Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2)).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
(* [bv_concat_unsigned] is the version that we want, but it
  only holds with a precondition. *)
Lemma bv_concat_unsigned m n2 b1 (b2 : bv n2) :
    (m = n + n2)%N →
    bv_unsigned (bv_concat m b1 b2) = Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2).
Proof.
    intros ->. rewrite bv_concat_unsigned', bv_wrap_small; [done|].
    apply Z.bounded_iff_bits_nonneg'; [lia | |].
    { apply Z.lor_nonneg. bv_saturate. split; [|lia]. apply Z.shiftl_nonneg. lia. }
    intros k ?. rewrite Z.lor_spec, Z.shiftl_spec; [|lia].
    apply orb_false_intro; (eapply Z.bounded_iff_bits_nonneg; [..|done]); bv_saturate; try lia.
    - apply (Z.lt_le_trans _ (bv_modulus n)); [lia|]. apply Z.pow_le_mono_r; lia.
    - apply (Z.lt_le_trans _ (bv_modulus n2)); [lia|]. apply Z.pow_le_mono_r; lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_concat_signed m n2 b1 (b2 : bv n2) :
    bv_signed (bv_concat m b1 b2) = bv_swrap m (Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2)).
Proof. unfold bv_concat. rewrite Z_to_bv_signed. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_Z_unsigned b z :
    bv_unsigned (b `+Z` z) = bv_wrap n (bv_unsigned b + z).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_Z_signed b z :
    bv_signed (b `+Z` z) = bv_swrap n (bv_signed b + z).
Proof. unfold bv_add_Z. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_sub_Z_unsigned b z :
    bv_unsigned (b `-Z` z) = bv_wrap n (bv_unsigned b - z).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_sub_Z_signed b z :
    bv_signed (b `-Z` z) = bv_swrap n (bv_signed b - z).
Proof. unfold bv_sub_Z. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_mul_Z_unsigned b z:
    bv_unsigned (b `*Z` z) = bv_wrap n (bv_unsigned b * z).
Proof. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_mul_Z_signed b z :
    bv_signed (b `*Z` z) = bv_swrap n (bv_signed b * z).
Proof. unfold bv_mul_Z. rewrite Z_to_bv_signed. bv_wrap_simplify_solve. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_sub_add_opp b1 b2:
    b1 - b2 = b1 + - b2.
Proof.
    apply bv_eq. unfold bv_sub, bv_add, bv_opp. rewrite !Z_to_bv_unsigned.
    bv_wrap_simplify_solve.
  Qed.
(* stdpp_bitvector/definitions.v *)
Instance bv_add_assoc : Assoc (=) (@bv_add n).
Proof.
    intros ???. unfold bv_add. apply bv_eq. rewrite !Z_to_bv_unsigned.
    bv_wrap_simplify_solve.
  Qed.
(* stdpp_bitvector/definitions.v *)
Instance bv_mul_assoc : Assoc (=) (@bv_mul n).
Proof.
    intros ???. unfold bv_mul. apply bv_eq. rewrite !Z_to_bv_unsigned.
    bv_wrap_simplify_solve.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_0_l b1 b2 :
    bv_unsigned b1 = 0%Z →
    b1 + b2 = b2.
Proof.
    intros Hb. apply bv_eq.
    rewrite bv_add_unsigned, Hb, Z.add_0_l, bv_wrap_small; [done|apply bv_unsigned_in_range].
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_0_r b1 b2 :
    bv_unsigned b2 = 0%Z →
    b1 + b2 = b1.
Proof.
    intros Hb. apply bv_eq.
    rewrite bv_add_unsigned, Hb, Z.add_0_r, bv_wrap_small; [done|apply bv_unsigned_in_range].
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_Z_0 b : b `+Z` 0 = b.
Proof.
    unfold bv_add_Z. rewrite Z.add_0_r.
    apply bv_eq. apply Z_to_bv_small. apply bv_unsigned_in_range.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_Z_add_r b m o:
    b `+Z` (m + o) = (b `+Z` o) `+Z` m.
Proof.
    apply bv_eq. unfold bv_add_Z. rewrite !Z_to_bv_unsigned.
     bv_wrap_simplify_solve.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_Z_add_l b m o:
    b `+Z` (m + o) = (b `+Z` m) `+Z` o.
Proof.
    apply bv_eq. unfold bv_add_Z. rewrite !Z_to_bv_unsigned.
     bv_wrap_simplify_solve.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_Z_succ b m:
    b `+Z` Z.succ m = (b `+Z` 1) `+Z` m.
Proof.
    apply bv_eq. unfold bv_add_Z. rewrite !Z_to_bv_unsigned.
    bv_wrap_simplify_solve.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_add_Z_inj_l b i j:
    0 ≤ i < bv_modulus n →
    0 ≤ j < bv_modulus n →
    b `+Z` i = b `+Z` j ↔ i = j.
Proof.
    intros ??. split; [|naive_solver].
    intros Heq%bv_eq. rewrite !bv_add_Z_unsigned, !(Z.add_comm (bv_unsigned _)) in Heq.
    by rewrite <-bv_wrap_add_inj, !bv_wrap_small in Heq.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_opp_not b:
    - b `-Z` 1 = bv_not b.
Proof.
    apply bv_eq.
    rewrite bv_not_unsigned, bv_sub_Z_unsigned, bv_opp_unsigned, <-Z.opp_lnot.
    bv_wrap_simplify_solve.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_and_comm b1 b2:
    bv_and b1 b2 = bv_and b2 b1.
Proof. apply bv_eq. by rewrite !bv_and_unsigned, Z.land_comm. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_or_comm b1 b2:
    bv_or b1 b2 = bv_or b2 b1.
Proof. apply bv_eq. by rewrite !bv_or_unsigned, Z.lor_comm. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_or_0_l b1 b2 :
    bv_unsigned b1 = 0%Z →
    bv_or b1 b2 = b2.
Proof. intros Hb. apply bv_eq. by rewrite bv_or_unsigned, Hb, Z.lor_0_l. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_or_0_r b1 b2 :
    bv_unsigned b2 = 0%Z →
    bv_or b1 b2 = b1.
Proof. intros Hb. apply bv_eq. by rewrite bv_or_unsigned, Hb, Z.lor_0_r. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_extract_0_unsigned l b:
    bv_unsigned (bv_extract 0 l b) = bv_wrap l (bv_unsigned b).
Proof. rewrite bv_extract_unsigned, Z.shiftr_0_r. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_extract_0_bv_add_distr l b1 b2:
    (l ≤ n)%N →
    bv_extract 0 l (bv_add b1 b2) = bv_add (bv_extract 0 l b1) (bv_extract 0 l b2).
Proof.
    intros ?.
    apply bv_eq. rewrite !bv_extract_0_unsigned, !bv_add_unsigned, !bv_extract_0_unsigned.
    rewrite bv_wrap_bv_wrap by done.
    bv_wrap_simplify_solve.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_concat_0 m n2 b1 (b2 : bv n2) :
    bv_unsigned b1 = 0%Z →
    bv_concat m b1 b2 = bv_zero_extend m b2.
Proof.
    intros Hb1. apply bv_eq.
    by rewrite bv_zero_extend_unsigned', bv_concat_unsigned', Hb1, Z.shiftl_0_l, Z.lor_0_l.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_zero_extend_idemp b:
    bv_zero_extend n b = b.
Proof. apply bv_eq. by rewrite bv_zero_extend_unsigned. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_sign_extend_idemp b:
    bv_sign_extend n b = b.
Proof. apply bv_eq_signed. by rewrite bv_sign_extend_signed. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_to_litte_endian_unsigned m n z:
    0 ≤ m →
    bv_unsigned <$> bv_to_little_endian m n z = Z_to_little_endian m (Z.of_N n) z.
Proof.
    intros ?. apply list_eq. intros i. unfold bv_to_little_endian.
    rewrite list_lookup_fmap, list_lookup_fmap.
    destruct (Z_to_little_endian m (Z.of_N n) z !! i) eqn: Heq; [simpl |done].
    rewrite Z_to_bv_small; [done|].
    eapply (Forall_forall (λ z, _ ≤ z < _)); [ |by eapply list_elem_of_lookup_2].
    eapply Z_to_little_endian_bound; lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_to_little_endian_to_bv m n bs:
    m = Z.of_nat (length bs) →
    bv_to_little_endian m n (little_endian_to_bv n bs) = bs.
Proof.
    intros ->. apply (inj (fmap bv_unsigned)).
    rewrite bv_to_litte_endian_unsigned; [|lia].
    apply Z_to_little_endian_to_Z; [by rewrite length_fmap | lia |].
    apply Forall_forall. intros ? [?[->?]]%list_elem_of_fmap. apply bv_unsigned_in_range.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma little_endian_to_bv_to_little_endian m n z:
    0 ≤ m →
    little_endian_to_bv n (bv_to_little_endian m n z) = z `mod` 2 ^ (m * Z.of_N n).
Proof.
    intros ?. unfold little_endian_to_bv.
    rewrite bv_to_litte_endian_unsigned; [|lia].
    apply little_endian_to_Z_to_little_endian; lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma length_bv_to_little_endian m n z :
    0 ≤ m →
    length (bv_to_little_endian m n z) = Z.to_nat m.
Proof.
    intros ?. unfold bv_to_little_endian. rewrite length_fmap.
    apply Nat2Z.inj. rewrite length_Z_to_little_endian, ?Z2Nat.id; try lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma little_endian_to_bv_bound n bs :
    0 ≤ little_endian_to_bv n bs < 2 ^ (Z.of_nat (length bs) * Z.of_N n).
Proof.
    unfold little_endian_to_bv. rewrite <-(length_fmap bv_unsigned bs).
    apply little_endian_to_Z_bound; [lia|].
    apply Forall_forall. intros ? [? [-> ?]]%list_elem_of_fmap.
    apply bv_unsigned_in_range.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma Z_to_bv_little_endian_to_bv_to_little_endian x m n (b : bv x):
    0 ≤ m →
    x = (Z.to_N m * n)%N →
    Z_to_bv x (little_endian_to_bv n (bv_to_little_endian m n (bv_unsigned b))) = b.
Proof.
    intros ? ->. rewrite little_endian_to_bv_to_little_endian, Z.mod_small; [| |lia].
    - apply bv_eq. rewrite Z_to_bv_small; [done|]. apply bv_unsigned_in_range.
    - pose proof bv_unsigned_in_range _ b as Hr. unfold bv_modulus in Hr.
      by rewrite N2Z.inj_mul, Z2N.id in Hr.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_to_little_endian_lookup_Some m n z (i : nat) x:
    0 ≤ m → bv_to_little_endian m n z !! i = Some x ↔
      Z.of_nat i < m ∧ x = Z_to_bv n (z ≫ (Z.of_nat i * Z.of_N n)).
Proof.
    unfold bv_to_little_endian. intros Hm. rewrite list_lookup_fmap, fmap_Some.
    split.
    - intros [?[[??]%Z_to_little_endian_lookup_Some ?]]; [|lia..]; subst. split; [done|].
      rewrite <-bv_wrap_land. apply bv_eq. by rewrite !Z_to_bv_unsigned, bv_wrap_bv_wrap.
    - intros [?->]. eexists _. split; [apply Z_to_little_endian_lookup_Some; try done; lia| ].
      rewrite <-bv_wrap_land. apply bv_eq. by rewrite !Z_to_bv_unsigned, bv_wrap_bv_wrap.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma little_endian_to_bv_spec n bs i b:
    0 ≤ i → n ≠ 0%N →
    bs !! Z.to_nat (i `div` Z.of_N n) = Some b →
    Z.testbit (little_endian_to_bv n bs) i = Z.testbit (bv_unsigned b) (i `mod` Z.of_N n).
Proof.
    intros ???. unfold little_endian_to_bv. apply little_endian_to_Z_spec; [lia|lia| |].
    { apply Forall_fmap. apply Forall_true. intros ?; simpl. apply bv_unsigned_in_range. }
    rewrite list_lookup_fmap. apply fmap_Some. naive_solver.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma length_bv_seq b len:
    length (bv_seq b len) = Z.to_nat len.
Proof. unfold bv_seq. by rewrite length_fmap, length_seqZ. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_seq_succ b m:
    0 ≤ m →
    bv_seq b (Z.succ m) = b :: bv_seq (b `+Z` 1) m.
Proof.
    intros. unfold bv_seq. rewrite seqZ_cons by lia. csimpl.
    rewrite bv_add_Z_0. f_equal.
    assert (Z.succ 0 = 1 + 0) as -> by lia.
    rewrite <-fmap_add_seqZ, <-list_fmap_compose, Z.pred_succ. apply list_fmap_ext.
    intros i x. simpl. by rewrite bv_add_Z_add_l.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma NoDup_bv_seq b z:
    0 ≤ z ≤ bv_modulus n →
    NoDup (bv_seq b z).
Proof.
    intros ?. apply NoDup_alt. intros i j b'. unfold bv_seq. rewrite !list_lookup_fmap.
    intros [?[[??]%lookup_seqZ ?]]%fmap_Some ; simplify_eq.
    intros [?[[->?]%lookup_seqZ ?%bv_add_Z_inj_l]]%fmap_Some; lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bool_to_bv_unsigned n b:
    n ≠ 0%N →
    bv_unsigned (bool_to_bv n b) = bool_to_Z b.
Proof.
    intros ?. pose proof (bv_modulus_gt_1 n).
    apply Z_to_bv_small. destruct b; simpl; lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_extract_bool_to_bv n n2 b:
    n ≠ 0%N → n2 ≠ 0%N →
    bv_extract 0 n (bool_to_bv n2 b) = bool_to_bv n b.
Proof.
    intros ??. apply bv_eq. pose proof (bv_modulus_gt_1 n).
    rewrite bv_extract_unsigned, !bool_to_bv_unsigned, Z.shiftr_0_r by done.
    rewrite bv_wrap_small; [done|]. destruct b; simpl; lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_not_bool_to_bv b:
    bv_not (bool_to_bv 1 b) = bool_to_bv 1 (negb b).
Proof. apply bv_eq. by destruct b. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bool_decide_bool_to_bv_0 b:
    bool_decide (bv_unsigned (bool_to_bv 1 b) = 0) = negb b.
Proof. by destruct b. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bool_decide_bool_to_bv_1 b:
    bool_decide (bv_unsigned (bool_to_bv 1 b) = 1) = b.
Proof. by destruct b. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma length_bv_to_bits b : length (bv_to_bits b) = N.to_nat n.
Proof. unfold bv_to_bits. rewrite length_fmap, length_seqZ, <-Z_N_nat, N2Z.id. done. Qed.
(* stdpp_bitvector/definitions.v *)
Lemma bv_to_bits_lookup_Some b i x:
    bv_to_bits b !! i = Some x ↔ (i < N.to_nat n)%nat ∧ x = Z.testbit (bv_unsigned b) (Z.of_nat i).
Proof.
    unfold bv_to_bits. rewrite list_lookup_fmap, fmap_Some.
    split.
    - intros [?[?%lookup_seqZ?]]. naive_solver lia.
    - intros [??]. eexists _. split; [|done]. apply lookup_seqZ. lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
Instance bv_to_bits_inj : Inj eq eq (@bv_to_bits n).
Proof.
    unfold bv_to_bits. intros x y Hf.
    apply bv_eq_wrap. apply Z.bits_inj_iff'. intros i Hi.
    rewrite !bv_wrap_spec; [|lia..]. case_bool_decide; simpl; [|done].
    eapply list_fmap_inj_1 in Hf; [done|]. apply elem_of_seqZ. lia.
  Qed.
(* stdpp_bitvector/definitions.v *)
(* * [bvn] *)
Record bvn
:= bv_to_bvn {
  bvn_n : N;
  bvn_val : bv bvn_n;
}.
(* stdpp_bitvector/definitions.v *)
Instance bv_to_bvn_inj {n} : Inj (=) (=) (@bv_to_bvn n).
Proof. intros Hb. naive_solver. Qed.
(* stdpp_bitvector/definitions.v *)
Definition bvn_unsigned (b : bvn)
:= bv_unsigned (b.(bvn_val)).
(* stdpp_bitvector/definitions.v *)
Lemma bvn_eq (b1 b2 : bvn) :
  b1 = b2 ↔ b1.(bvn_n) = b2.(bvn_n) ∧ bvn_unsigned b1 = bvn_unsigned b2.
Proof. split; [ naive_solver|]. destruct b1, b2; simpl; intros [??]. subst. f_equal. by apply bv_eq. Qed.
(* stdpp_bitvector/definitions.v *)
Instance bvn_eq_dec : EqDecision bvn := λ '(@bv_to_bvn n1 b1) '(@bv_to_bvn n2 b2),
   cast_if_and (decide (n1 = n2)) (decide (bv_unsigned b1 = bv_unsigned b2)).
(* TODO: The following does not compute to eq_refl*)
Next Obligation. intros. apply bvn_eq. naive_solver. Qed.
(* stdpp_bitvector/definitions.v *)
Definition bvn_to_bv (n : N) (b : bvn) : option (bv n)
:=
  match decide (b.(bvn_n) = n) with
  | left eq => Some (eq_rect (bvn_n b) (λ n0 : N, bv n0) (bvn_val b) n eq)
  | right _ => None
  end.
(* stdpp_bitvector/definitions.v *)
Coercion bv_to_bvn : bv >-> bvn.
(* stdpp_bitvector/tactics.v *)
(* * General tactics *)
Ltac unfold_lets_in_context
:=
  repeat match goal with
         | H := _ |- _ => unfold H in *; clear H
         end.
(* stdpp_bitvector/tactics.v *)
(* * General lemmas *)
Lemma bv_extract_concat_later m n1 n2 s l (b1 : bv n1) (b2 : bv n2):
  (n2 ≤ s)%N →
  (m = n1 + n2)%N →
  bv_extract s l (bv_concat m b1 b2) = bv_extract (s - n2) l b1.
Proof.
  intros ? ->. apply bv_eq.
  rewrite !bv_extract_unsigned, bv_concat_unsigned, !bv_wrap_land by done.
  apply Z.bits_inj_iff' => ??.
  rewrite !Z.land_spec, !Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec, Z.ones_spec; [|lia..].
  case_bool_decide; rewrite ?andb_false_r, ?andb_true_r; [|done].
  rewrite <-(bv_wrap_bv_unsigned _ b2), bv_wrap_spec_high, ?orb_false_r; [|lia].
  f_equal. lia.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_extract_concat_here m n1 n2 s (b1 : bv n1) (b2 : bv n2):
  s = 0%N →
  (m = n1 + n2)%N →
  bv_extract s n2 (bv_concat m b1 b2) = b2.
Proof.
  intros -> ->. apply bv_eq.
  rewrite !bv_extract_unsigned, bv_concat_unsigned, !bv_wrap_land by done.
  apply Z.bits_inj_iff' => ??.
  rewrite !Z.land_spec, !Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec, Z.ones_spec; [|lia..].
  case_bool_decide; rewrite ?andb_false_r, ?andb_true_r.
  - rewrite (Z.testbit_neg_r (bv_unsigned b1)); [|lia]. simpl. f_equal. lia.
  - rewrite <-(bv_wrap_bv_unsigned _ b2), bv_wrap_spec_high, ?orb_false_l; lia.
Qed.
(* stdpp_bitvector/tactics.v *)
Notation bv_suwrap signed
:= (if signed then bv_swrap else bv_wrap).
(* stdpp_bitvector/tactics.v *)
Class BvUnfold (n : N) (signed : bool) (wrapped : bool) (b : bv n) (z : Z)
:= {
    bv_unfold_proof : ((if signed then bv_signed else bv_unsigned) b) =
                        (if wrapped then bv_suwrap signed n z else z);
}.
(* stdpp_bitvector/tactics.v *)
(* [BV_UNFOLD_BLOCK] is a marker that this occurrence of [bv_signed]
or [bv_unsigned] has already been simplified. *)
Definition BV_UNFOLD_BLOCK {A} (x : A) : A
:= x.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_end s w n b :
  BvUnfold n s w b ((if s then BV_UNFOLD_BLOCK bv_signed else BV_UNFOLD_BLOCK bv_unsigned) b).
Proof.
  constructor. unfold BV_UNFOLD_BLOCK.
  destruct w, s; by rewrite ?bv_wrap_bv_unsigned, ?bv_swrap_bv_signed.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_BV s w n z Hwf :
  BvUnfold n s w (@BV _ z Hwf) (if w then z else if s then bv_swrap n z else z).
Proof.
  constructor. unfold bv_unsigned.
  destruct w, s; simpl; try done; by rewrite bv_wrap_small by by apply bv_wf_in_range.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_bv_0 s w n :
  BvUnfold n s w (bv_0 n) 0.
Proof. constructor. destruct w, s; rewrite ?bv_0_signed, ?bv_0_unsigned, ?bv_swrap_0; done. Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_Z_to_bv s w n z :
  BvUnfold n s w (Z_to_bv _ z) (if w then z else bv_suwrap s n z).
Proof. constructor. destruct w, s; rewrite ?Z_to_bv_signed, ?Z_to_bv_unsigned; done. Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_succ s w n b z :
  BvUnfold n s true b z →
  BvUnfold n s w (bv_succ b) (if w then Z.succ z else bv_suwrap s n (Z.succ z)).
Proof.
  intros [Hz]. constructor.
  destruct w, s; rewrite ?bv_succ_signed, ?bv_succ_unsigned, ?Hz; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_pred s w n b z :
  BvUnfold n s true b z →
  BvUnfold n s w (bv_pred b) (if w then Z.pred z else bv_suwrap s n (Z.pred z)).
Proof.
  intros [Hz]. constructor.
  destruct w, s; rewrite ?bv_pred_signed, ?bv_pred_unsigned, ?Hz; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_add s w n b1 b2 z1 z2 :
  BvUnfold n s true b1 z1 →
  BvUnfold n s true b2 z2 →
  BvUnfold n s w (bv_add b1 b2) (if w then z1 + z2 else bv_suwrap s n (z1 + z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_add_signed, ?bv_add_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_sub s w n b1 b2 z1 z2 :
  BvUnfold n s true b1 z1 →
  BvUnfold n s true b2 z2 →
  BvUnfold n s w (bv_sub b1 b2) (if w then z1 - z2 else bv_suwrap s n (z1 - z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_sub_signed, ?bv_sub_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_opp s w n b z :
  BvUnfold n s true b z →
  BvUnfold n s w (bv_opp b) (if w then - z else bv_suwrap s n (- z)).
Proof.
  intros [Hz]. constructor.
  destruct w, s; rewrite ?bv_opp_signed, ?bv_opp_unsigned, ?Hz; bv_wrap_simplify_solve.
Qed.
(* stdpp_bitvector/tactics.v *)
Lemma bv_unfold_mul s w n b1 b2 z1 z2 :
  BvUnfold n s true b1 z1 →
  BvUnfold n s true b2 z2 →
  BvUnfold n s w (bv_mul b1 b2) (if w then z1 * z2 else bv_suwrap s n (z1 * z2)).
Proof.
  intros [Hz1] [Hz2]. constructor.
  destruct w, s; rewrite ?bv_mul_signed, ?bv_mul_unsigned, ?Hz1, ?Hz2; bv_wrap_simplify_solve.
Qed.