proposition: Remark ptrofs_2_aligned: forall ofs, Ptrofs.and ofs Ptrofs.one = Ptrofs.zero <-> (2 | Ptrofs.unsigned ofs).
proof: Proof. assert (A: forall n, (2 | n) <-> Z.Even n). { intros; split; intros [k E]; rewrite E; exists k; ring. } assert (B: forall n, Z.Even n <-> Z.testbit n 0 = false). { intros. rewrite Z.bit0_odd, <- Z.negb_even, <- Z.even_spec, negb_false_iff. tauto. } intros; split; intros. - apply A. apply B. change false with (Ptrofs.testbit Ptrofs.zero 0). rewrite <- H. rewrite Ptrofs.bits_and, Ptrofs.bits_one. simpl. rewrite andb_true_r; auto. generalize Ptrofs.wordsize_pos; omega. - apply A in H. apply B in H. Ptrofs.bit_solve. rewrite Ptrofs.bits_one. destruct (zeq i 0); simpl. rewrite andb_true_r. subst i. exact H. apply andb_false_r. Qed.
imports: compcert.lib.Coqlib compcert.lib.Zbits compcert.common.AST compcert.lib.Integers compcert.common.Values compcert.common.Memory compcert.common.Globalenvs compcert.common.Events