diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index dd1113996c..457ee56fb5 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -685,54 +685,60 @@ Open a new coq file `tutorial_c_proofs.v` in the same folder ``` From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors. +From CryptolToCoq Require Import SAWCoreBitvectors. From CryptolToCoq Require Import SAWCorePrelude. -From CryptolToCoq Require Import CompMExtra. -(* The following line enables pretty printing*) -Import CompMExtraNotation. Open Scope fun_syntax. +(* The following 2 lines allows better automation *) +Require Import Examples.common. +Require Import Coq.Program.Tactics. (* Great tacticals, move to automation. Perhaps `Require Export`? *) +(* Import our function definitions*) Require Import Examples.tutorial_c_gen. Import tutorial_c. ``` -It first imports all the SAW functionality we need and enables pretty -printing. Then it imports our new definitions (e.g. `add`). +It first imports all the SAW functionality we need and some useful +tactics. Then it imports our new definitions (e.g. `add`). Our first proof will claim that the function `add` produces no errors. More specifically, it says that for all inputs (that's what -`refinesFun` quantifies) `add` always refines to `noErrorsSpec`. That -is, it returns a pure value. +`spec_refines_eq` quantifies) `add` always refines to `safety_spec`. That +is, it returns a pure value without errors. ``` -Lemma no_errors_add - : refinesFun add (fun _ _ => noErrorsSpec). + +Lemma no_errors_add (x y: bitvector 64) : + spec_refines_eq (add x y) (safety_spec (x,y)). Proof. ``` -We will use our automation to quickly prove the lemma, but we must -first unfold those definitions the the automation is unfamiliar with. +We will use our automation to quickly prove the lemma, ``` -unfold add, add__tuple_fun, noErrorsSpec. +solve_trivial_spec 0 0. Qed. ``` -Then our function `prove_refinement` will deal with the proof. +You can also attempt the same proof with `add_mistyped`, which +obviously will fail, since `add_mistyped` has an error. First, you +will note that `add_mistyped` only takes one argument (since only one +was defined in its signature) ``` - prove_refinement. -Qed. +Lemma no_errors_add_mistyped (x: bitvector 64) : + spec_refines_eq (add_mistyped x) (safety_spec (x)). +Proof. solve_trivial_spec 0 0. + + clarify_goal_tutorial. ``` -You can also attempt the same proof with `add_mistyped`, which -obviously will fail, since `add_mistyped` has an error. +After rewriting the terms for clarity, you can see the +remaining goal says that an `ErrorS` is a refinement of +`RetS`. In other words, it's trying to prove that a trivially +pure function has an error. That's obviously false. ``` -Lemma no_errors_add_mistyped - : refinesFun add_mistyped (fun _ => noErrorsSpec). -Proof. - unfold add_mistyped, add_mistyped__tuple_fun, noErrorsSpec. - prove_refinement. - (* Fails to solve the goal. *) Abort. ``` @@ -793,12 +799,9 @@ You will have to generate the `.vo` again to write proofs about produces no errors. ``` -Lemma no_errors_incr_ptr - : refinesFun incr_ptr (fun _ => noErrorsSpec). -Proof. - unfold incr_ptr, incr_ptr__tuple_fun. - prove_refinement. -Qed. +Lemma no_errors_incr_ptr (x: bitvector 64) : + spec_refines_eq (incr_ptr x) (safety_spec x). +Proof. solve_trivial_spec 0 0. Qed. ``` ### Structs @@ -963,48 +966,39 @@ adds dynamic checks on the extracted code which we will see in the Coq code. Let's go to `arrays_gen.v` (which has already been generated for you) -and look for the definition of `zero_array__tuple_fun`. You will -notice that it calls `errorM` twice but, in this case that's not a +and look for the definition of `zero_array__bodies`. You will +notice that it calls `errorS` twice, but in this case, that's not a sign of a typing error! Heapster includes these errors to catch out-of-bounds array accesses and unrepresentable indices (i.e. index that can't be written as a machine integer). The code below is a -simplification of the `zero_array__tuple_fun` with some notation for +simplification of the `zero_array__bodies` with some notation for readability (see below for how to enable such pritty printing). ``` -zero_array__tuple_fun = - (* ... Some ommited code ... *) - LetRec f:= - (fun (e1 e2 : int64) (p1 : Vector int64 e1) - (_ _ _ : unit : Type) => - (* ... Some ommited code ... *) - let var__4 := (0)[1] in - let var__6 := e2 < e1 in - (*... Some ommited code ...*) - if - not - ((if var__6 then 1 else var__4) == - var__4) - then - if - ((17293822569102704640)[64] <= e2) && - (e2 <= (1152921504606846975)[64]) - then - If e2

+ CallS VoidEv emptyFunStack zero_array__frame + (mkFrameCall zero_array__frame 1 e0 (0)[64] p0 tt tt tt), + (fun (e0 e1 : int64) (p0 : Vector int64 e0) (_ _ _ : unit) => + if negb ((if e1 < e0 then (-1)[1] else (0)[1]) == (0)[1]) + then + if ((17293822569102704640)[64] <= e1) && (e1 <= (1152921504606846975)[64]) + then + If e1

assumingM (zero_array_precond x) noErrorsSpec). -Proof +Lemma no_errors_zero_array x y: + spec_refines_eq (zero_array x y) + (total_spec (fun '(len, vec, dec) => zero_array_precond len) (fun _ _ => True) (x,y, bvAdd _ x (intToBv _ 1))). +Proof. ``` It claims that, assuming the precondition `zero_array_precond` is @@ -1057,12 +1053,10 @@ Definition zero_array_precond x We will not go into detail about the proof, but notice that the -important steps are handled by custom automation. Namely we use the -commands `prove_refinement_match_letRecM_l` and `prove_refinement` to -handle refinements with and without recursion (respectively). The rest -of the proof, consists of discharging simple inequalities and a couple -of trivial entailments, where the left hand side is an error (and thus -entails anything). +important steps are handled by custom automation. + +TODO: This proof is involved. Perhaps add some more details? + ### Recursive data structures diff --git a/heapster-saw/examples/_CoqProject b/heapster-saw/examples/_CoqProject index 267f4afa42..448319ce4c 100644 --- a/heapster-saw/examples/_CoqProject +++ b/heapster-saw/examples/_CoqProject @@ -6,11 +6,11 @@ linked_list_gen.v linked_list_proofs.v xor_swap_gen.v -#xor_swap_proofs.v +xor_swap_proofs.v xor_swap_rust_gen.v #xor_swap_rust_proofs.v c_data_gen.v -#c_data_proofs.v +c_data_proofs.v string_set_gen.v #string_set_proofs.v loops_gen.v @@ -39,3 +39,4 @@ sha512_gen.v #sha512_proofs.v io_gen.v #io_proofs.v +common.v \ No newline at end of file diff --git a/heapster-saw/examples/arrays_proofs.v b/heapster-saw/examples/arrays_proofs.v index e1504a8a9e..1c69ae0032 100644 --- a/heapster-saw/examples/arrays_proofs.v +++ b/heapster-saw/examples/arrays_proofs.v @@ -1,4 +1,3 @@ -From Coq Require Import Program.Basics. From Coq Require Import Lists.List. From Coq Require Import String. From Coq Require Import Vectors.Vector. @@ -7,15 +6,107 @@ From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors. From CryptolToCoq Require Import SAWCoreBitvectors. From CryptolToCoq Require Import SAWCorePrelude. -From CryptolToCoq Require Import CompMExtra. - -Import SAWCorePrelude. - +From EnTree Require Import Automation. +Require Import Lia. +From CryptolToCoq Require Import SAWCoreBitvectorsZifyU64. + +Require Import Examples.common. Require Import Examples.arrays_gen. Import arrays. +Import SAWCorePrelude. + Import VectorNotations. +Set Nested Proofs Allowed. +Lemma UIP_bv : + forall {n} (x y : bitvector n) (p1 p2 : x = y), p1 = p2. +Proof. + intros. + apply UIP_dec. + clear. intros. + refine (eq_dec _ boolEq _ n x y). + clear. intros. + split; intros H. + - destruct x; destruct y; auto. + - subst x. destruct y; reflexivity. +Qed. +Require Import Coq.Program.Tactics. + +Declare Scope bv_64. +Local Open Scope bv_64. +Bind Scope bv_64 with bitvector. + +Infix "+":= (bvAdd 64) (at level 50, left associativity): bv_64. +Infix "-":= (bvSub 64) (at level 50, left associativity): bv_64. +Infix "<":= (isBvslt 64) (at level 70): bv_64. +Infix "<=":= (isBvsle 64) (at level 70): bv_64. + +(*This is a prototype of a tactic to solve all signed inequalities for +Boolean vectors, as long as there is no overflow. Ideally, if the +tactic fails, it will show you the bounds you need to prove that thre +is no overflow. You probably missed them in your invariants. + +The idea is pretty simple: convert everything to to `Int` and, becasue +there is no overflow, we can remove the module quantifiers and crush +it with standard lia. + +TO DO: + +- Support all arith relations eq[ ], lt[ ], gt[ ], le[✓], ge[ ] + +- Don't directly apply rewrites to all subgoals for efficiency + +- Recognize when there is a terminal "node" to apply `lia`. Right now + we attempt lia at every step, whcih is wasteful. + + *) + +Lemma eq_bvToInt: + forall n a b, + (BinInt.Z.lt (bvToInt n a) (bvToInt n b)) -> + isBvslt n a b. +Proof. +Admitted. +Lemma lt_bvToInt: + forall n a b, + (BinInt.Z.lt (bvToInt n a) (bvToInt n b)) -> + isBvslt n a b. +Proof. +Admitted. +Lemma le_bvToInt: + forall n a b, + (BinInt.Z.le (bvToInt n a) (bvToInt n b)) -> + isBvsle n a b. +Proof. +Admitted. + + +Ltac bvToInt_ineq:= + first [apply eq_bvToInt | + apply lt_bvToInt | + apply le_bvToInt]. + +Ltac remove_mods:= + (*TODO: Add other operations*) + try rewrite bvAdd_Zadd_mod_64; + try rewrite bvSub_Zsub_mod_64; + try rewrite bvMul_Zmul_mod_64; + repeat rewrite bvToInt_intToBv_64; + repeat rewrite BinInt.Z.mod_small. + +Ltac solve_bv_no_overflow:= + try lia; + match goal with + | |- isBvsle _ ?LHA ?RHS => + apply le_bvToInt + | |- isBvslt _ ?LHA ?RHS => + apply lt_bvToInt + end; remove_mods; + try solve_bv_no_overflow. + + + Definition bvMem_lo := intToBv 64 0xf000000000000000. Definition bvMem_hi := intToBv 64 0x0fffffffffffffff. @@ -26,35 +117,117 @@ Definition zero_array_precond x Definition zero_array_invariant x x' i := isBvsle 64 (intToBv 64 0) i /\ isBvsle 64 i x /\ x = x'. -Lemma no_errors_zero_array - : refinesFun zero_array (fun x _ => assumingM (zero_array_precond x) noErrorsSpec). +Record HeVector T := + someVector { + hvLen1 : nat + ; hvLen2 : _ + ; theVector : BVVec hvLen1 hvLen2 T + }. +Arguments someVector {T hvLen1 hvLen2} theVector. + + +(* Simpler version of `inversion_sigma` where the inversion is only applied if the hyp has the same *) +Ltac simple_inv_sigma:= + match goal with + | H: (_; ?x) = (_; ?y) |- _ => eapply inj_pair2 in H; try subst x + end. +Ltac inv_with_sigma H:= inversion H; repeat simple_inv_sigma. +Tactic Notation "inv_someVector" "in" "*" := + match goal with H: someVector _ = someVector _ |- _ => inv_with_sigma H end. + + +Lemma HeVectorToSigma: + forall len len' vec vec', + (exists (Plen : len = len'), + eq_rect len (fun x => BVVec 64 x (bitvector 64)) vec len' Plen = vec') -> + someVector vec = someVector vec'. +Proof. intros * [Plen Heq]. subst len'. + rewrite <- eq_rect_eq in Heq; subst; auto. +Qed. + +Hint Extern 101 (IntroArg ?n (someVector ?a = someVector ?b) _) => + let e1 := argName n in IntroArg_intro e1; +(eapply HeVectorToSigma in e1); +revert e1; apply (IntroArg_fold n _ _) : refines prepostcond. + +Polymorphic Lemma IntroArg_someVector T n m a1 a2 b1 b2 (eq : a1 = a2) goal : + IntroArg n (eq_rect _ (fun x => BVVec m x T) b1 _ eq = b2) (fun _ => goal) -> + IntroArg n (@someVector T m a1 b1 = @someVector T m a2 b2) (fun _ => goal). Proof. - unfold zero_array, zero_array__tuple_fun, zero_array_precond. - prove_refinement_match_letRecM_l. - - exact (fun a' i _ _ _ _ => assumingM (zero_array_invariant a a' i) noErrorsSpec). - unfold zero_array_invariant, noErrorsSpec. - fold bvMem_lo; fold bvMem_hi. - time "no_errors_zero_array" prove_refinement. - (* A number of the remaining cases are covered exactly by hypotheses we already have in - scope (e.g. proving the loop invariant holds initially). Note that `prove_refinement` - doesn't do this automatically because it may matter which hypothesis is used, if - there are multiple. For this poof though, it doesn't. *) - all: try assumption. - (* Proving that the loop invariant holds inductively: *) - - discriminate e_maybe. - - transitivity a2. - + assumption. - + apply isBvsle_suc_r; eauto. - rewrite e_assuming2, e_assuming0. - reflexivity. - - apply isBvslt_to_isBvsle_suc. - apply isBvult_to_isBvslt_pos; assumption. - (* Proving that these branches are impossible, by virtue of our loop invariant: *) - - rewrite <- e_assuming1 in e_if0. - discriminate e_if0. - - rewrite e_assuming2, e_assuming0 in e_if0. - apply isBvslt_antirefl in e_if0; contradiction e_if0. - (* The remaining cases are all taken care of by either prove_refinement or assumption! *) + destruct eq. + intros HH a. + inv_with_sigma a. + eapply HH; reflexivity. +Qed. + +Hint Extern 101 (IntroArg ?n ?A ?g) => + simple apply IntroArg_someVector; idtac "Done it" + : refines prepostcond. + +Lemma no_errors_zero_array x y: + spec_refines_eq (zero_array x y) + (total_spec (fun '(len, vec, dec) => zero_array_precond len) (fun _ _ => True) (x,y, bvAdd _ x (intToBv _ 1))). +Proof. + intros; unfold_function. + prove_refinement. + - wellfounded_decreasing_nat. + exact (bvToNat _ x1). + - prepost_case 0 0. + + exact (someVector a = someVector a0 /\ + x = x1 /\ + bvAdd _ x (intToBv _ 1) = x2). + + exact (someVector r = someVector r0). + + prepost_case 1 0. + * exact (someVector a = someVector a0 /\ + x = x2 /\ + x3 = bvSub _ x0 x1 /\ + zero_array_invariant x0 x x1). + * exact ( (someVector r = someVector r0)). + * prepost_exclude_remaining. + - prove_refinement_continue; + (* Need to add `inv_someVector` to the automation to reduce better*) + try inv_someVector in *. + (* with NoRewrite NoSolve *) + + reflexivity. + + assert (HH: isBvule _ x0 (bvsmax _)). + { clear - e_assume. + destruct e_assume. + eapply isBvule_to_isBvsle_pos; auto. + vm_compute; auto. + rewrite H0. vm_compute. reflexivity. + } + clear - HH. lia. + + reflexivity. + + repeat split. + eapply e_assume. + + reflexivity. + + destruct_conjs; subst. + clear HPrePost HWf. lia. + + destruct_conjs; subst. auto. + + unfold zero_array_precond in *; destruct_conjs; subst; hnf; split. + * solve_bv_no_overflow. + * split; auto. + solve_bv_no_overflow. + + reflexivity. + + unfold zero_array_precond, zero_array_invariant in *. + destruct_conjs; subst. + subst. + hnf. + rewrite and_bool_eq_false in *. + exfalso. + destruct e_if0 as [e_if0 | e_if0]. + * eapply isBvslt_def_opp in e_if0. + rewrite <- i1 in e_if0. + vm_compute in e_if0; congruence. + * eapply isBvslt_def_opp in e_if0. + rewrite -> i2 in e_if0. + rewrite -> i0 in e_if0. + vm_compute in e_if0. congruence. + + reflexivity. + + Unshelve. + all: auto. + Qed. diff --git a/heapster-saw/examples/c_data_proofs.v b/heapster-saw/examples/c_data_proofs.v index 505387e908..cdb6fe0a6f 100644 --- a/heapster-saw/examples/c_data_proofs.v +++ b/heapster-saw/examples/c_data_proofs.v @@ -6,27 +6,27 @@ From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors. From CryptolToCoq Require Import SAWCoreBitvectors. From CryptolToCoq Require Import SAWCorePrelude. -From CryptolToCoq Require Import CompMExtra. +From EnTree Require Import Automation. +Require Import Examples.common. Require Import Examples.c_data_gen. Import c_data. Import SAWCorePrelude. -Lemma no_errors_incr_u64_ptr_byte : - refinesFun incr_u64_ptr_byte (fun _ => noErrorsSpec). - unfold incr_u64_ptr_byte, incr_u64_ptr_byte__tuple_fun, noErrorsSpec. - time "no_errors_incr_u64_ptr_byte" prove_refinement. -Qed. + +Set Bullet Behavior "Strict Subproofs". + +Global Hint Unfold malloc: automation. + +Lemma no_errors_incr_u64_ptr_byte x: + spec_refines_eq (incr_u64_ptr_byte x) (safety_spec (x)). +Proof. solve_trivial_spec 0 0. Qed. Lemma no_errors_alloc_padded_struct : - refinesFun alloc_padded_struct noErrorsSpec. - unfold alloc_padded_struct, alloc_padded_struct__tuple_fun, noErrorsSpec, malloc. - time "no_errors_alloc_padded_struct" prove_refinement. -Qed. - -Lemma no_errors_padded_struct_incr_all : - refinesFun padded_struct_incr_all (fun _ => noErrorsSpec). - unfold padded_struct_incr_all, padded_struct_incr_all__tuple_fun, noErrorsSpec. - time "no_errors_padded_struct_incr_all" prove_refinement. -Qed. + spec_refines_eq alloc_padded_struct (safety_spec tt). +Proof. solve_trivial_spec 0 0; solve_trivial_sidecondition. Qed. + +Lemma no_errors_padded_struct_incr_all x0: + spec_refines_eq (padded_struct_incr_all x0) (safety_spec (x0)). +Proof. solve_trivial_spec 0 0; solve_trivial_sidecondition. Qed. diff --git a/heapster-saw/examples/common.v b/heapster-saw/examples/common.v new file mode 100644 index 0000000000..98786d08eb --- /dev/null +++ b/heapster-saw/examples/common.v @@ -0,0 +1,154 @@ +(* +* Common definitions and tactics that make the examples easier to +* state and prove. Some or all of these could go into an automation file +* so we can start building functionality. *) + +From Coq Require Import Lists.List. +From Coq Require Import String. +From Coq Require Import Vectors.Vector. +From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors. +From CryptolToCoq Require Import SAWCoreBitvectors. + +From CryptolToCoq Require Import SAWCorePrelude. +From CryptolToCoq Require Import SpecMExtra. +From EnTree Require Import Automation. + +Require Import Coq.Program.Tactics. (* Great tacticals, move to automation. Perhaps `Require Export`? *) + + +Global Set Bullet Behavior "Strict Subproofs". + + +(** *Basic Coq tactics These are natural extensions of the Coq + standard library. I generally try to use names that are compatible + with those used in opther projects to help new users. + + We should consider moveing them at the top level + *) + +Ltac break_match:= + match goal with + |- context [match ?a with _ => _ end] => destruct a + end. +Ltac break_match_hyp:= + match goal with + [ H:context [match ?a with _ => _ end] |- _] => destruct a + end. + +Ltac forget_as term name:= + let Hforget := fresh in + remember term as name eqn:Hforget; clear Hforget. + + +(** *Basic Spec definitions *) + +(* Spec when all events and returns are expected to be the same *) +Definition spec_refines_eq {E Γ R}: + Rel (SpecM E Γ R) (SpecM E Γ R):= + @spec_refines E E Γ Γ eqPreRel eqPostRel R R eq. + +(* The spec fro things that have no errors. *) +Definition safety_spec {E Γ R A} {QT: QuantType R}: forall a: A, SpecM E Γ R:= + total_spec (fun _ => True) (fun _ _ => True). + + +(** * Tactics for solving trivial spec refinement *) + +(* unfolds the corresponding to the `fun__bodies` of a spec. *) +Ltac unfold_bodies:= + match goal with |- context[MultiFixS _ _ _ ?X__bodies] => unfold X__bodies end. + +(* | Unfolds a function applied to an arbitrary number of +arguments. Might fail if the function is a transparent definition of +an applied relation. *) +Ltac unfold_head T := + match T with + | ?T _ => unfold_head T + | ?T => unfold T; unfold_bodies + end. + +(* | Unfolds a function definition `func` and its body `func__bodies` *) +Create HintDb automation. +Ltac unfold_function:= + try unfold spec_refines_eq, safety_spec; + match goal with + | |- spec_refines _ _ _ ?fun_applied _ => let T := fun_applied in + unfold_head T + end; autounfold with automation. + +(* The follwoing functions are for automatically matching arguments, + in a spec trivial spec *) +Ltac PreCase_conjunction x y:= + eapply Logic.and;[exact (x=y)| ]. + +Ltac cont_join x tl cont:= + match tl with + | (?front, ?final) => + PreCase_conjunction x final; (cont front) + | _ => exact (x = tl) + end. + +Ltac SubGoal ls1 ls2 cont:= + match ls1 with + | (?x0 ; ?tl1 ) => SubGoal tl1 ls2 ltac:(fun tl2 => cont_join x0 tl2 cont) + | _ => cont ls2 + end. + +(* Ltac for trivial PreCase *) +Ltac PreCase_Trivial:= + match goal with + |- PreCase _ _ ?ls1 (?ls2; tt) => + SubGoal ls1 ls2 ltac:(fun ls => exact True) (* last part is only triggered if the lists are empty*) + end. + +(* Ltac for trivial PostCase *) +Ltac list_zip ls1 ls2:= + match ls1 with + | (?x, ?ls1') => match ls2 with + | (?y, ?ls2') => + apply Logic.and; + [list_zip ls1' ls2' | exact (x = y)] + | _ => fail "Mismatched lists" + end + | _ => exact (ls1 = ls2) + end. + +Ltac PostCase_Trivial:= + match goal with + |- PostCase _ _ _ _ ?ls1 ?ls2 => list_zip ls1 ls2 + end. + + +Ltac solve_prepost_case n m:= + prepost_case n m; + [PreCase_Trivial + | PostCase_Trivial + | prepost_exclude_remaining]. + +(* | This tactic solves many trivial spec refinements, specially good + when proving there is no error, which is generally trivial. *) +Ltac solve_trivial_spec n m:= + intros; unfold_function; prove_refinement; + [wellfounded_none | solve_prepost_case n m| prove_refinement_continue]. + +Ltac solve_trivial_sidecondition := + repeat break_match; repeat break_match_hyp; destruct_conjs; subst; tauto. + +(** *Tactics for clarity*) + +(* | This tactic allows you to forget errors, the precondition, +postcondition and relations to clearly see what we are proving.*) +Ltac clarify_goal_tutorial:= + match goal with + |- context [ErrorS _ ?st] => + let error_msg:=fresh "error_msg" in + forget_as st error_msg + end; + match goal with + | |- Automation.spec_refines ?pre ?post ?RR _ _ => + let PRE:=fresh "PRE" in + let POST:=fresh "POST" in + let Relation:=fresh "Relation" in + forget_as pre PRE; forget_as post POST; forget_as RR Relation + end. diff --git a/heapster-saw/examples/tutorial_c_proofs.v b/heapster-saw/examples/tutorial_c_proofs.v index ebb55b0e8d..099e4cfda4 100644 --- a/heapster-saw/examples/tutorial_c_proofs.v +++ b/heapster-saw/examples/tutorial_c_proofs.v @@ -1,40 +1,45 @@ From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors. +From CryptolToCoq Require Import SAWCoreBitvectors. From CryptolToCoq Require Import SAWCorePrelude. -From CryptolToCoq Require Import CompMExtra. -(* The following line enables pretty printing*) +(* The following 2 lines enables pretty printing*) +From CryptolToCoq Require Import CompMExtra. Import CompMExtraNotation. Open Scope fun_syntax. +(* The following 2 lines allows better automatio*) +Require Import Examples.common. +Require Import Coq.Program.Tactics. + Require Import Examples.tutorial_c_gen. Import tutorial_c. +Lemma no_errors_add (x y: bitvector 64) : + spec_refines_eq (add x y) (safety_spec (x,y)). +Proof. solve_trivial_spec 0 0. Qed. + +Lemma no_errors_add_mistyped (x: bitvector 64) : + spec_refines_eq (add_mistyped x) (safety_spec (x)). +Proof. solve_trivial_spec 0 0. -Lemma no_errors_add - : refinesFun add (fun _ _ => noErrorsSpec). -Proof. - unfold add, add__tuple_fun. - prove_refinement. -Qed. - -Lemma no_errors_add_mistyped - : refinesFun add_mistyped (fun _ => noErrorsSpec). -Proof. - unfold add_mistyped, add_mistyped__tuple_fun, noErrorsSpec. - prove_refinement. - (* Fails to solve the goal. *) +(* After rewriting the terms for clarity, you can see the + remaining goal says that an `ErrorS` is a refinement of + `RetS`. In other words, it's trying to prove that a trivially + pure function has an error. That's obviously false. *) + clarify_goal_tutorial. Abort. - -Lemma no_errors_incr_ptr - : refinesFun incr_ptr (fun _ => noErrorsSpec). -Proof. - unfold incr_ptr, incr_ptr__tuple_fun, noErrorsSpec. - prove_refinement. -Qed. +Lemma no_errors_incr_ptr (x: bitvector 64) : + spec_refines_eq (incr_ptr x) (safety_spec x). +Proof. solve_trivial_spec 0 0. Qed. -Lemma no_errors_norm_vector - : refinesFun norm_vector (fun _ _ _ => noErrorsSpec). -Proof. - unfold norm_vector, norm_vector__tuple_fun, noErrorsSpec. - prove_refinement. +Lemma no_errors_norm_vector (x y z: bitvector 64) : + spec_refines_eq (norm_vector x y z) (safety_spec (x, y, z)). +Proof. solve_trivial_spec 0 0. + + (* The remaining goal, is to show that if initial arguments are + equal (for both specs) then at the end of the execution, they + are also equal.*) + destruct_conjs; subst; reflexivity. Qed. diff --git a/heapster-saw/examples/xor_swap_proofs.v b/heapster-saw/examples/xor_swap_proofs.v index c78cd2dc5d..1736f00e92 100644 --- a/heapster-saw/examples/xor_swap_proofs.v +++ b/heapster-saw/examples/xor_swap_proofs.v @@ -1,4 +1,3 @@ - From Coq Require Import Lists.List. From Coq Require Import String. From Coq Require Import Vectors.Vector. @@ -7,40 +6,52 @@ From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors. From CryptolToCoq Require Import SAWCoreBitvectors. From CryptolToCoq Require Import SAWCorePrelude. -From CryptolToCoq Require Import CompMExtra. +From EnTree Require Import Automation. +Require Import Examples.common. Require Import Examples.xor_swap_gen. Import xor_swap. +Set Bullet Behavior "Strict Subproofs". -Definition xor_swap_spec x1 x2 : - CompM (bitvector 64 * bitvector 64) := - returnM (x2, x1). +Definition xor_swap_spec (x1 x2: bitvector 64) := (x2, x1). Arguments xor_swap_spec /. -Lemma no_errors_xor_swap : refinesFun xor_swap (fun _ _ => noErrorsSpec). -Proof. - unfold xor_swap, xor_swap__tuple_fun, noErrorsSpec. - time "no_errors_xor_swap" prove_refinement. -Qed. +(* First prove safety (i.e. no errors) *) +Lemma xor_swap_not_error (x y: bitvector 64) : + spec_refines_eq (xor_swap x y) (safety_spec (x,y)). +Proof. solve_trivial_spec 0 0. Qed. + +Local Hint Extern 10 (spec_refines eqPreRel eqPostRel eq (xor_swap _ _) _) => + simple apply xor_swap_not_error: refine_proofs. -Lemma bvXor_twice_r n x y : - SAWCorePrelude.bvXor n (SAWCorePrelude.bvXor n x y) y = x. -Proof. - rewrite <- bvXor_assoc. rewrite bvXor_same. rewrite bvXor_zero. reflexivity. -Qed. -Lemma bvXor_twice_l n x y : - SAWCorePrelude.bvXor n (SAWCorePrelude.bvXor n y x) y = x. +(* | Nice notation for better reading in this file*) +Local Infix "^^" := (SAWCorePrelude.bvXor 64) (at level 30). +Lemma bvXor_twice_l: + forall x1 x2 : bitvector 64, x2 ^^ (x2 ^^ x1) = x1. Proof. - rewrite bvXor_comm. rewrite bvXor_assoc. - rewrite bvXor_same. rewrite bvXor_comm. rewrite bvXor_zero. reflexivity. + intros; rewrite bvXor_assoc, bvXor_same, bvXor_comm, bvXor_zero. + reflexivity. Qed. -Lemma xor_swap_correct : refinesFun xor_swap xor_swap_spec. +Lemma bvXor_twice_r: + forall x1 x2 : bitvector 64, (x1 ^^ x2) ^^ x2 = x1. Proof. - prove_refinement. - subst. rewrite bvXor_twice_r. rewrite bvXor_twice_l. + intros; rewrite <- bvXor_assoc, bvXor_same, bvXor_zero. reflexivity. +Qed. + +(* | Now we can prove correctness *) +Lemma xor_swap_spec_ref (x y: bitvector 64) : + spec_refines_eq (xor_swap x y) + (total_spec (fun _ => True) (fun xy r => r = xor_swap_spec (fst xy) (snd xy)) + (x,y)). +Proof. solve_trivial_spec 0 0. + - apply bvXor_twice_r. + - apply bvXor_twice_l. Qed. + +Local Hint Extern 10 (spec_refines eqPreRel eqPostRel eq (xor_swap _ _) _) => + simple apply xor_swap_spec_ref: refine_proofs.