Commit 9f85b58b authored by Fengmin Zhu's avatar Fengmin Zhu Committed by Michael Sammler
Browse files

Ci/bits

parent e3411f3a
Pipeline #42133 passed with stage
in 14 minutes and 50 seconds
......@@ -14,3 +14,4 @@ _opam
*.timing
.lia.cache
.nia.cache
.vscode/
......@@ -713,3 +713,41 @@ Proof.
elim: l. { split; inversion 1. }
move => ?? IH. split; inversion 1; simplify_eq; constructor => //; by apply IH.
Qed.
(* Binary representation of bounded integers. *)
Lemma pos_bounded_iff_bits k n :
(0 k 0 n n < 2^k l, k l Z.testbit n l = false)%Z.
Proof.
move => Hk Hn.
destruct (decide (n = 0)) as [->|].
- setoid_rewrite Z.bits_0. split => // ?. by apply: Z.pow_pos_nonneg.
- split.
+ move => /Z.log2_lt_pow2 Hb l Hl.
apply Z.bits_above_log2 => //. lia.
+ move => Hl.
destruct (decide (n < 2^k)%Z) => //.
have : Z.testbit n (Z.log2 n) = false.
{ apply Hl, Z.log2_le_pow2; lia. }
rewrite Z.bit_log2 //. lia.
Qed.
Lemma bounded_iff_bits k n :
(0 k -2^k n < 2^k
l, k l Z.testbit n l = bool_decide (n < 0))%Z.
Proof.
move => Hk.
case_bool_decide; last by rewrite -pos_bounded_iff_bits; lia.
have -> : (n = - Z.abs n)%Z by lia.
split.
+ move => [? _] l Hl.
rewrite Z.bits_opp ?negb_true_iff; last lia.
eapply pos_bounded_iff_bits => //; lia.
+ move => He.
split; last by etrans; [|apply: Z.pow_pos_nonneg]; lia.
rewrite -Z.opp_le_mono.
suff : (Z.abs n - 1 < 2 ^ k)%Z by lia.
apply pos_bounded_iff_bits; [lia..|] => l Hl.
rewrite -negb_true_iff -Z.bits_opp; last lia.
by apply: He.
Qed.
......@@ -138,6 +138,13 @@ Section IntType.
Definition bits_per_int (it : int_type) : Z :=
bytes_per_int it * bits_per_byte.
Lemma bits_per_int_gt_0 it : bits_per_int it > 0.
Proof.
rewrite /bits_per_int /bits_per_byte.
suff : (bytes_per_int it > 0) by lia.
by apply: bytes_per_int_gt_0.
Qed.
Definition int_modulus (it : int_type) : Z :=
2 ^ bits_per_int it.
......@@ -908,14 +915,20 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
(* we need to take `quot` and `rem` here for the correct rounding
behavior, i.e. rounding towards 0 (instead of `div` and `mod`,
which round towards floor)*)
| DivOp => if n2 is 0 then None else Some (n1 `quot` n2)
| ModOp => if n2 is 0 then None else Some (n1 `rem` n2)
(* TODO: Figure out if these are the operations we want and what sideconditions they have *)
| DivOp => if bool_decide (n2 0) then Some (n1 `quot` n2) else None
| ModOp => if bool_decide (n2 0) then Some (n1 `rem` n2) else None
| AndOp => Some (Z.land n1 n2)
| OrOp => Some (Z.lor n1 n2)
| XorOp => Some (Z.lxor n1 n2)
| ShlOp => Some (n1 n2)
| ShrOp => Some (n1 n2)
(* For shift operators (`ShlOp` and `ShrOp`), behaviors are defined if:
- lhs is nonnegative, and
- rhs (also nonnegative) is less than the number of bits in lhs.
See: https://en.cppreference.com/w/c/language/operator_arithmetic, "Shift operators". *)
| ShlOp => if bool_decide (0 n1 0 n2 < bits_per_int it) then Some (n1 n2) else None
(* NOTE: when lhs is negative, Coq's `≫` is not semantically equivalent to C's `>>`.
Counterexample: Coq `-1000 ≫ 10 = 0`; C `-1000 >> 10 == -1`.
This is because `≫` is implemented by `Z.div`. *)
| ShrOp => if bool_decide (0 n1 0 n2 < bits_per_int it) then Some (n1 n2) else None
| _ => None
end = Some n
val_to_int v1 it = Some n1
......
......@@ -174,9 +174,9 @@ Section programs.
| AddOp => n it
| SubOp => n it
| MulOp => n it
| AndOp => n it (* TODO: remove side-condition. *)
| OrOp => n it (* TODO: remove side-condition. *)
| XorOp => n it (* TODO: remove side-condition. *)
| AndOp => True
| OrOp => True
| XorOp => True
| ShlOp => 0 n2 < bits_per_int it 0 n1 n max_int it
| ShrOp => 0 n2 < bits_per_int it 0 n1 (* Result of shifting negative numbers is implementation defined. *)
| DivOp => n2 0 n it
......@@ -184,19 +184,71 @@ Section programs.
| _ => True (* Relational operators. *)
end.
Lemma bitwise_op_result_in_range op bop (it : int_type) n1 n2 :
(0 n1 0 n2 0 op n1 n2)
bool_decide (op n1 n2 < 0) = bop (bool_decide (n1 < 0)) (bool_decide (n2 < 0))
( k, Z.testbit (op n1 n2) k = bop (Z.testbit n1 k) (Z.testbit n2 k))
n1 it n2 it op n1 n2 it.
Proof.
move => Hnonneg Hsign Htestbit.
rewrite /elem_of /int_elem_of_it /min_int /max_int.
destruct (it_signed it).
- rewrite /int_half_modulus.
move ? : (bits_per_int it - 1) => k.
have ? : 0 k.
{ suff : bits_per_int it > 0 by lia. by apply: bits_per_int_gt_0. }
have Hb : n, -2^k n 2^k - 1
l, k l Z.testbit n l = bool_decide (n < 0)
by intros; rewrite -bounded_iff_bits; lia.
move => /Hb Hn1 /Hb Hn2.
apply Hb => l Hl.
by rewrite Htestbit Hsign Hn1 ?Hn2.
- rewrite /int_modulus.
move ? : (bits_per_int it) => k.
have ? : 0 k.
{ suff : bits_per_int it > 0 by lia. by apply: bits_per_int_gt_0. }
have Hb : n, 0 n n 2^k - 1
l, k l Z.testbit n l = bool_decide (n < 0)
by intros; rewrite bool_decide_false -?pos_bounded_iff_bits; lia.
move => [Hn1 /Hb HN1] [Hn2 /Hb HN2].
have Hn := Hnonneg Hn1 Hn2.
split; first done.
apply (Hb _ Hn) => l Hl.
by rewrite Htestbit HN1 ?HN2.
Qed.
Lemma arith_op_result_in_range (it : int_type) (n1 n2 n : Z) op :
n1 it n2 it arith_op_result it n1 n2 op = Some n
arith_op_sidecond it n1 n2 n op n it.
Proof.
move => [Hn1 HN1] [Hn2 HN2] Hn Hsc.
move => Hn1 Hn2 Hn Hsc.
destruct op => //=; simpl in Hsc, Hn; destruct_and? => //.
all: inversion Hn; simplify_eq; split => //.
- transitivity 0; [ apply min_int_le_0 | by apply Z.shiftl_nonneg ].
- transitivity 0; [ apply min_int_le_0 | by apply Z.shiftr_nonneg ].
- transitivity n1; last done. rewrite Z.shiftr_div_pow2; last by lia.
apply Z.div_le_upper_bound. { apply Z.pow_pos_nonneg => //. }
rewrite -[X in X _]Z.mul_1_l. apply Z.mul_le_mono_nonneg_r => //.
rewrite -(Z.pow_0_r 2). apply Z.pow_le_mono_r; lia.
all: inversion Hn; simplify_eq.
- apply (bitwise_op_result_in_range Z.land andb) => //.
+ rewrite Z.land_nonneg; naive_solver.
+ repeat case_bool_decide; try rewrite -> Z.land_neg in *; naive_solver.
+ by apply Z.land_spec.
- apply (bitwise_op_result_in_range Z.lor orb) => //.
+ by rewrite Z.lor_nonneg.
+ repeat case_bool_decide; try rewrite -> Z.lor_neg in *; naive_solver.
+ by apply Z.lor_spec.
- apply (bitwise_op_result_in_range Z.lxor xorb) => //.
+ by rewrite Z.lxor_nonneg.
+ have Hn : n, bool_decide (n < 0) = negb (bool_decide (0 n)).
{ intros. repeat case_bool_decide => //; lia. }
rewrite !Hn.
repeat case_bool_decide; try rewrite -> Z.lxor_nonneg in *; naive_solver.
+ by apply Z.lxor_spec.
- split.
+ trans 0; [ apply min_int_le_0 | by apply Z.shiftl_nonneg ].
+ done.
- split.
+ trans 0; [ apply min_int_le_0 | by apply Z.shiftr_nonneg ].
+ destruct Hn1.
trans n1; last done. rewrite Z.shiftr_div_pow2; last by lia.
apply Z.div_le_upper_bound. { apply Z.pow_pos_nonneg => //. }
rewrite -[X in X _]Z.mul_1_l. apply Z.mul_le_mono_nonneg_r => //.
rewrite -(Z.pow_0_r 2). apply Z.pow_le_mono_r; lia.
Qed.
Lemma type_arithop_int_int it v1 n1 v2 n2 T n op:
......@@ -215,13 +267,14 @@ Section programs.
iApply (wp_binop_det v). iSplit.
- iIntros (σ v') "_ !%". split.
+ destruct op => //.
all: inversion 1; destruct n2; simplify_eq/=.
all: inversion 1; simplify_eq/=.
all: try case_bool_decide => //.
all: destruct it as [? []]; simplify_eq/= => //.
all: try by rewrite ->it_in_range_mod in * => //; simplify_eq.
+ move => ->; destruct op, n2 => //; econstructor => // => //.
+ move => ->; destruct op => //; econstructor => // => //.
all: try by inversion Hsc; case_bool_decide; naive_solver.
all: destruct it as [? []]; simplify_eq/= => //.
all: try by rewrite it_in_range_mod; simplify_eq/=.
all: by destruct_and!.
all: try by rewrite it_in_range_mod.
- iIntros "!>". iApply "HΦ"; last done. by iPureIntro.
Qed.
Global Program Instance type_add_int_int_inst it v1 n1 v2 n2:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment