proposition: Lemma bit_ones : forall n p, bit (ones n) p = if (ltb p n && (ltb p 63))%uint63 then true else false.
proof: Proof. unfold ones,one. intros. rewrite bitE. rewrite sub_spec. rewrite lsl_spec. replace (((φ (1)%uint63 * 2 ^ φ (n)%uint63)))%Z with (2 ^ (to_Z n))%Z by lia. unfold wB. rewrite power2_mod by (unfold size ; lia). destruct ((φ (n)%uint63 <? Z.of_nat size)%Z) eqn:T. - unfold size in *. rewrite Z.mod_small. replace ( 2 ^ φ (n)%uint63 - φ (1)%uint63)%Z with (Z.pred (2 ^ φ (n)%uint63))%Z by lia. rewrite <- Z.ones_equiv. rewrite Z.testbit_ones_nonneg by lia. destruct ((p <? n) && (p <? 63))%uint63 eqn:LT. lia. lia. assert (BOUND : (0 < 2 ^ to_Z n < wB)%Z). { unfold wB. split. apply Z.pow_pos_nonneg; lia. apply Z.pow_lt_mono_r. lia. unfold size. lia. unfold digits, size in *. lia. } lia. - assert (1 < 2 ^ Z.of_nat size)%Z. { apply Z.pow_gt_1. lia. lia. } rewrite Z_mod_nz_opp_full; rewrite Z.mod_small ; try lia. replace ( 2 ^ Z.of_nat size - φ (1)%uint63)%Z with (Z.pred (2 ^ Z.of_nat size))%Z by lia. rewrite <- Z.ones_equiv. rewrite Z.testbit_ones_nonneg by lia. destruct ((p <? n)%uint63 && (p <? 63)%uint63) eqn:T2. lia. lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR