Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[saw-core-coq] Check bitvector lemmas for < 4 bits #1495

Merged
merged 4 commits into from
Nov 6, 2021
Merged

[saw-core-coq] Check bitvector lemmas for < 4 bits #1495

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e018613
add axiom-based holds_for_bits_up_to tactics, fix some bv lemmas (...)
m-yac Nov 2, 2021
ec1c8f6
fix definition of `shiftR`, resolve `bvToNat` warning
m-yac Nov 3, 2021
336781e
get heapster examples working with correct bv lemmas
m-yac Nov 5, 2021
91825b0
always use holds_for_bits_up_to_3 for better performance
m-yac Nov 5, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 5 additions & 11 deletions heapster-saw/examples/arrays_proofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ Proof.
(* Proving that the loop invariant holds inductively: *)
- transitivity a2.
+ assumption.
+ apply isBvsle_suc_r.
+ apply isBvsle_suc_r; eauto.
rewrite e_assuming2, e_assuming0.
reflexivity.
- apply isBvslt_to_isBvsle_suc.
Expand Down Expand Up @@ -80,7 +80,7 @@ Proof.
discriminate e_maybe.
- transitivity a2.
+ assumption.
+ apply isBvsle_suc_r.
+ apply isBvsle_suc_r; eauto.
rewrite e_assuming2, e_assuming0.
reflexivity.
- apply isBvslt_to_isBvsle_suc.
Expand Down Expand Up @@ -215,12 +215,6 @@ Admitted.

(* We *really* need a better bitvector library, the lemmas we need are getting pretty ad-hoc *)

Axiom bvSub_1_lt : forall w a, isBvslt w (intToBv w 0) a ->
isBvslt w (bvSub w a (intToBv w 1)) a.

Axiom isBvslt_suc_r : forall w a, isBvslt w a (bvsmax w) ->
isBvslt w a (bvAdd w a (intToBv w 1)).

Axiom isBvsle_bvSub_inj_pos : forall w a b c, isBvsle w (intToBv w 0) a ->
isBvsle w (intToBv w 0) b ->
isBvsle w (intToBv w 0) c ->
Expand Down Expand Up @@ -252,14 +246,14 @@ Proof.
(* apply isBvsle_bvSub_inj_pos. *)
(* I give up I'm done messing around manually with bitvectors for now *)
admit.
+ apply bvSub_1_lt.
rewrite e_assuming; reflexivity.
+ apply isBvslt_pred_l; eauto.
rewrite <- e_assuming; reflexivity.
- (* (e_if4 is a contradiction) *)
admit.
- rewrite e_assuming.
change (intToBv 64 2) with (bvAdd 64 (intToBv 64 1) (intToBv 64 1)).
rewrite <- bvAdd_assoc.
rewrite <- isBvslt_suc_r; [ rewrite <- isBvslt_suc_r; [ reflexivity |] |].
rewrite <- isBvslt_suc_r.
+ admit.
+ admit.
Admitted.
10 changes: 5 additions & 5 deletions heapster-saw/examples/iter_linked_list_proofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ Qed.

Definition incr_list_invar :=
@list_rect (bitvector 64) (fun _ => Prop) True
(fun x _ rec => isBvult 64 x (intToBv 64 0x7fffffffffffffff) /\ rec).
(fun x _ rec => isBvslt 64 x (bvsmax 64) /\ rec).

Arguments incr_list_invar !l.

Expand All @@ -105,11 +105,11 @@ Proof.
time "no_errors_incr_list" prove_refinement.
all: try destruct e_assuming as [?e_assuming ?e_assuming];
try destruct e_assuming0 as [?e_assuming ?e_assuming];
try destruct e_assuming1 as [?e_assuming ?e_assuming]; simpl in *.
try destruct e_assuming1 as [?e_assuming ?e_assuming]; cbn - [bvsmax] in *.
(* All but one of the remaining goals are taken care of by assumptions we have in scope: *)
all: try rewrite appendList_Nil_r; try split; eauto.
(* We just have to show this case is impossible by virtue of our loop invariant: *)
apply isBvult_to_isBvule_suc in e_assuming0.
apply bvule_msb_l in e_assuming0; try assumption.
compute_bv_funs in e_assuming0; inversion e_assuming0.
apply isBvslt_suc_r in e_assuming0.
rewrite <- e_assuming0, e_if in e_if0.
apply isBvslt_antirefl in e_if0; contradiction.
Qed.
30 changes: 19 additions & 11 deletions heapster-saw/examples/loops_proofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,10 +81,16 @@ Definition no_errors_sign_of_sum' : ltac:(let tp := type of no_errors_sign_of_su
in exact tp') := no_errors_sign_of_sum.
Hint Rewrite no_errors_sign_of_sum' : refinement_proofs.

Lemma no_errors_compare_sum : refinesFun compare_sum (fun _ _ _ => noErrorsSpec).
Lemma no_errors_compare_sum :
refinesFun compare_sum (fun x _ _ => assumingM (isBvslt 64 (bvsmin 64) x)
noErrorsSpec).
Proof.
unfold compare_sum, compare_sum__tuple_fun, noErrorsSpec.
time "no_errors_compare_sum" prove_refinement.
- assumption. (* doesn't matter what we put here *)
- rewrite bvNeg_bvslt_zero_iff in e_if; eauto.
rewrite e_if in e_if0.
apply isBvslt_antirefl in e_if0; contradiction.
Qed.


Expand All @@ -100,28 +106,30 @@ Hint Rewrite sign_of_sum_spec_ref' : refinement_proofs.


Definition compare_sum_spec (x y z : bitvector 64) : CompM (bitvector 64) :=
orM ( assertM (isBvslt _ x (bvAdd _ y z)) >> returnM (intToBv _ 1))
(orM (assertM (isBvslt _ (bvAdd _ y z) x) >> returnM (intToBv _ (-1)))
(assertM (x = bvAdd _ y z) >> returnM (intToBv _ 0))).
assumingM (isBvslt 64 (bvsmin 64) x /\ bvSubOverflow 64 (bvAdd 64 y z) x = false)
(orM ( assertM (isBvslt _ x (bvAdd _ y z)) >> returnM (intToBv _ 1))
(orM (assertM (isBvslt _ (bvAdd _ y z) x) >> returnM (intToBv _ (-1)))
(assertM (x = bvAdd _ y z) >> returnM (intToBv _ 0)))).

Lemma compare_sum_spec_ref : refinesFun compare_sum compare_sum_spec.
Proof.
unfold compare_sum, compare_sum__tuple_fun, compare_sum_spec.
time "compare_sum_spec_ref" prove_refinement.
all: rewrite bvSub_zero_n in e_assert.
all: try rewrite bvSub_zero_n, bvAdd_comm, <- bvSub_eq_bvAdd_neg in e_assert.
(* Note that there are two versions of each case because of the if! *)
(* The `x < y + z` case: *)
1,4: continue_prove_refinement_left.
1,2: rewrite bvslt_bvSub_r, bvSub_eq_bvAdd_neg, bvAdd_comm.
1,2: assumption.
1,2: apply bvslt_bvSub_r; eauto.
(* The `x > y + z` case: *)
1,3: continue_prove_refinement_right;
continue_prove_refinement_left.
1,2: rewrite bvslt_bvSub_l, bvSub_eq_bvAdd_neg, bvAdd_comm.
1,2: assumption.
1,2: apply bvslt_bvSub_l; eauto.
(* The `x = y + z` case: *)
1,2: continue_prove_refinement_right;
continue_prove_refinement_right.
1,2: rewrite bvEq_bvSub_r, bvSub_eq_bvAdd_neg, bvAdd_comm.
1,2: symmetry; assumption.
1,2: rewrite bvEq_bvSub_r; symmetry; eauto.
(* The remaining case follows from our precondition (same as no_errors) *)
rewrite bvNeg_bvslt_zero_iff in e_if0; eauto.
rewrite e_if0 in e_if1.
apply isBvslt_antirefl in e_if1; contradiction.
Qed.
2 changes: 0 additions & 2 deletions heapster-saw/examples/mbox_proofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,6 @@ Proof.
+ rewrite H1 in e_maybe; discriminate e_maybe.
(* Showing the loop invariant holds inductively (the remaining two cases) *)
- rewrite e_assuming1; apply isBvsle_suc_r.
apply isBvslt_to_isBvsle.
rewrite e_assuming2, e_assuming3.
reflexivity.
- apply isBvslt_to_isBvsle_suc.
Expand Down Expand Up @@ -180,7 +179,6 @@ Proof.
+ rewrite H1 in e_maybe; discriminate e_maybe.
(* Showing the loop invariant holds inductively (the remaining two cases) *)
- rewrite e_assuming1; apply isBvsle_suc_r.
apply isBvslt_to_isBvsle.
rewrite e_assuming2, e_assuming3.
reflexivity.
- apply isBvslt_to_isBvsle_suc.
Expand Down
Loading