From e875433f0f6ca3f518f96d670c318f6d69edfcce Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2022 12:10:22 -0400 Subject: [PATCH 01/12] Fix probable typo introduced in bcd4bcf014b54db0137a534472baa32c9fd35200 --- bedrock2/src/bedrock2Examples/chacha20.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index 331b34f9f..365a46c94 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -42,7 +42,7 @@ Section chacha20. (x0, x5, x10, x15) = chacha20_quarter( x0, x5, x10, x15); (x1, x6, x11, x12) = chacha20_quarter( x1, x6, x11, x12); (x2, x7, x8, x13) = chacha20_quarter( x2, x7, x8, x13); - (x3, x4, x9, x1) = chacha20_quarter( x3, x4, x9, x14) + (x3, x4, x9, x14) = chacha20_quarter( x3, x4, x9, x14) }; x0 += $0x61707865; x1 += $0x3320646e; x2 += $0x79622d32; x3 += $0x6b206574; x4 += load4(key); x5 += load4(key+$4); x6 += load4(key+$8); x7 += load4(key+$12); From cbd45e733b8266fc45384f21c89da52738372333 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2022 12:09:59 -0400 Subject: [PATCH 02/12] Create non-inlined chacha20_block --- bedrock2/src/bedrock2Examples/chacha20.v | 29 ++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index 365a46c94..fe393de19 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -18,12 +18,20 @@ Section chacha20. c += d; b ^= c; b <<<= 7 ))). + Definition QUARTERROUND (a b c d : String.string) : cmd + := ltac:(let body := (eval cbv [chacha20_quarter] in (let '(_, (_, _, body)) := chacha20_quarter in body)) in + lazymatch (eval pattern "a", "b", "c", "d" in body) with + | ?x "a" "b" "c" "d" + => let y := (eval cbv beta in (x a b c d)) in + exact y + end). + Local Notation "'xorout' o x" := ( let addr := bedrock_expr:(out+coq:(expr.literal(4*o))) in bedrock_cmd:(store4($addr, load4($addr)^$(expr.var (ident_to_string! x))))) (in custom bedrock_cmd at level 0, o bigint, x ident). - Definition chacha20_block : func := + Definition chacha20_block_separate : func := (* NOTE: I (andreser) don't understand why xorout needs these *) let x0 := "x0" in let x1 := "x1" in let x2 := "x2" in let x3 := "x3" in let x4 := "x4" in let x5 := "x5" in let x6 := "x6" in let x7 := "x7" in @@ -53,11 +61,28 @@ Section chacha20. xorout 8 x8; xorout 9 x9; xorout 10 x10; xorout 11 x11; xorout 12 x12; xorout 13 x13; xorout 14 x14; xorout 15 x15 ))). + + Local Ltac repquarterround body := + lazymatch body with + | context body[cmd.call [?x1; ?x2; ?x3; ?x4] "chacha20_quarter" [expr.var ?x1; expr.var ?x2; expr.var ?x3; expr.var ?x4] ] + => let body := context body[QUARTERROUND x1 x2 x3 x4] in + repquarterround body + | context body[cmd.call ?ls "chacha20_quarter" ?ls' ] + => let v := constr:(cmd.call ls "chacha20_quarter" ls') in + fail 0 "could not replace ""chacha20_quarter"" in" v + | context["chacha20_quarter"] + => fail 0 "could not replace ""chacha20_quarter"" in" body + | _ => body + end. + Definition chacha20_block : func := + ltac:(let body := (eval cbv delta [chacha20_block_separate] in chacha20_block_separate) in + let body := repquarterround body in + exact body). End chacha20. (* Require bedrock2.ToCString. Example chacha20_block_c_string := Eval vm_compute in - ToCString.c_module [chacha20_quarter; chacha20_block]. + ToCString.c_module [chacha20_quarter; chacha20_block_separate]. Print chacha20_block_c_string. *) From 9cdaae2eb7f9a9304de4b5c6e018c45b527b66b9 Mon Sep 17 00:00:00 2001 From: John Grosen Date: Fri, 19 Apr 2019 00:02:30 -0400 Subject: [PATCH 03/12] pull out which byte/word instances to use in straightline when doing certain types of loads --- bedrock2/src/bedrock2Examples/chacha20.v | 113 +++++++++++++++++++++++ 1 file changed, 113 insertions(+) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index fe393de19..df0c66fe3 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -86,3 +86,116 @@ Example chacha20_block_c_string := Eval vm_compute in ToCString.c_module [chacha20_quarter; chacha20_block_separate]. Print chacha20_block_c_string. *) + +From coqutil Require Import Word.Interface Map.Interface. +From coqutil.Word Require Import Naive. +From coqutil.Tactics Require Import letexists eabstract. +From bedrock2 Require Import FE310CSemantics Semantics WeakestPrecondition ProgramLogic Array Scalars. +From bedrock2.Map Require Import Separation SeparationLogic. +From coqutil.Z Require Import Lia. + +Local Infix "*" := sep. +Local Infix "*" := sep : type_scope. + +Local Instance word32: Interface.word 32 := coqutil.Word.Naive.word 32 eq_refl. +Local Instance word32_ok: word.ok word32 := coqutil.Word.Naive.ok _ _. +Local Instance byte_ok: word.ok byte := coqutil.Word.Naive.ok _ _. +Local Instance mapok: map.ok mem := SortedListWord.ok (Naive.word 32 eq_refl) _. +Local Instance wordok: word.ok word := coqutil.Word.Naive.ok _ _. + +Instance spec_of_chacha20 : spec_of "chacha20_block" := fun functions => + forall outAddr out keyAddr key nonceAddr nonce cval R m t, + (array scalar32 (word.of_Z 4) outAddr out * + array scalar32 (word.of_Z 4) keyAddr key * + array scalar32 (word.of_Z 4) nonceAddr nonce * + R) m -> + 16 = Z.of_nat (List.length out) -> + 8 = Z.of_nat (List.length key) -> + 3 = Z.of_nat (List.length nonce) -> + WeakestPrecondition.call functions "chacha20_block" t m [outAddr; keyAddr; nonceAddr; cval] + (fun t' m' rets => rets = []). + +Lemma chacha20_ok : program_logic_goal_for_function! chacha20_block. +Proof. + straightline. + destruct key; [cbn in H1; congruence |]. + cbn [array] in H. + repeat straightline. + + letexists; split. + 1: { + repeat straightline. + letexists; split. + 1: { + Print Ltac straightline. + (* try subst v0; eapply Scalars.load_four_of_sep. *) + (* try subst v0; refine (@Scalars.load_four_of_sep _ (@word FE310CSemantics.parameters) (@byte FE310CSemantics.parameters) ltac:(typeclasses eauto) ltac:(typeclasses eauto) ltac:(typeclasses eauto) (@mem FE310CSemantics.parameters) ltac:(typeclasses eauto) _ _ _ _ _). *) + try subst v0; refine (@Scalars.load_four_of_sep _ (@word FE310CSemantics.parameters) (@byte FE310CSemantics.parameters) _ _ _ (@mem FE310CSemantics.parameters) _ _ _ _ _ _). + refine (Lift1Prop.subrelation_iff1_impl1 _ _ _ _ _ H). + ecancel. + Set Printing Implicit. + cbv [word32]. + cbn [Z.compare]. + ecancel. + cancel. + + let RHS := lazymatch goal with + | |- @Lift1Prop.iff1 _ _ (@seps _ _ _ ?RHS) => RHS + end in + let jy := index_and_element_of RHS in + let j := lazymatch jy with + | @pair _ _ ?i _ => i + end in + let y := lazymatch jy with + | @pair _ _ _ ?y => y + end in + assert_fails (idtac; (let y := rdelta.rdelta_var y in + is_evar y)); + (let LHS := lazymatch goal with + | |- @Lift1Prop.iff1 _ (@seps _ _ _ ?LHS) _ => LHS + end in + idtac LHS y). + let i := find_syntactic_unify_deltavar LHS y in + idtac). + simple refine (@cancel_seps_at_indices _ _ _ _ i j LHS RHS _ _); + idtac). + cbn[firstn skipn app hd tl]; + [ syntactic_unify._syntactic_exact_deltavar + (@RelationClasses.reflexivity _ _ + (@RelationClasses.Equivalence_Reflexive _ _ (Lift1Prop.Equivalence_iff1 _)) _) + | ]). + + let RHS := lazymatch goal with + | |- Lift1Prop.iff1 _ (seps ?RHS) => RHS + end in + let jy := index_and_element_of RHS in + let j := lazymatch jy with + | (?i, _) => i + end in + let y := lazymatch jy with + | (_, ?y) => y + end in + assert_fails idtac; (let y := rdelta.rdelta_var y in + is_evar y); + (let LHS := lazymatch goal with + | |- Lift1Prop.iff1 (seps ?LHS) _ => LHS + end in + let i := find_syntactic_unify_deltavar LHS y in + simple refine (cancel_seps_at_indices i j LHS RHS _ _); cbn[firstn skipn app hd tl]; + [ syntactic_exact_deltavar (RelationClasses.reflexivity _) | ]). + ecancel_step. + Print Ltac ecancel_step. + match goal with + | [ |- Lift1Prop.iff1 (seps ?lhs) (seps ?rhs) ] => + refine (cancel_seps_at_indices 1 0 lhs rhs _ _); cbn [firstn skipn app hd tl]; [reflexivity |] + end. + eapply RelationClasses.reflexivity. + cbn [seps]. + reflexivity. + } + 1: { + subst v v0. + reflexivity. + } + } + repeat straightline. From 58860a3aa64759491c5a70584646197e093108fc Mon Sep 17 00:00:00 2001 From: John Grosen Date: Fri, 19 Apr 2019 13:30:07 -0400 Subject: [PATCH 04/12] chacha20 memory safety proof wip --- bedrock2/src/bedrock2Examples/chacha20.v | 174 ++++++++++++----------- 1 file changed, 93 insertions(+), 81 deletions(-) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index df0c66fe3..2da7948e7 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -87,10 +87,11 @@ Example chacha20_block_c_string := Eval vm_compute in Print chacha20_block_c_string. *) -From coqutil Require Import Word.Interface Map.Interface. +From Coq Require Import ZArith.ZArith. +From coqutil Require Import Word.Interface Word.Properties Map.Interface. From coqutil.Word Require Import Naive. From coqutil.Tactics Require Import letexists eabstract. -From bedrock2 Require Import FE310CSemantics Semantics WeakestPrecondition ProgramLogic Array Scalars. +From bedrock2 Require Import FE310CSemantics Semantics WeakestPrecondition ProgramLogic Array Scalars TailRecursion. From bedrock2.Map Require Import Separation SeparationLogic. From coqutil.Z Require Import Lia. @@ -115,87 +116,98 @@ Instance spec_of_chacha20 : spec_of "chacha20_block" := fun functions => WeakestPrecondition.call functions "chacha20_block" t m [outAddr; keyAddr; nonceAddr; cval] (fun t' m' rets => rets = []). +Hint Rewrite + word.unsigned_of_Z word.signed_of_Z word.of_Z_unsigned word.unsigned_add word.unsigned_sub word.unsigned_opp word.unsigned_or word.unsigned_and word.unsigned_xor word.unsigned_not word.unsigned_ndn word.unsigned_mul word.signed_mulhss word.signed_mulhsu word.unsigned_mulhuu word.unsigned_divu word.signed_divs word.unsigned_modu word.signed_mods word.unsigned_slu word.unsigned_sru word.signed_srs word.unsigned_eqb word.unsigned_ltu word.signed_lts + using trivial + : word_laws. + +Monomorphic Definition word__monomorphic_ring_theory := Properties.word.ring_theory (word := word). +Add Ring word_ring : word__monomorphic_ring_theory. + Lemma chacha20_ok : program_logic_goal_for_function! chacha20_block. Proof. straightline. - destruct key; [cbn in H1; congruence |]. - cbn [array] in H. + repeat (destruct out; [cbn in H0; congruence |]). + repeat (destruct key; [cbn in H1; congruence |]). + repeat (destruct nonce; [cbn in H2; congruence |]). + cbn [array word.add word.of_Z] in H. + Local Ltac word_add_trans_one addr := + match goal with + | [ H : context[@word.add _ ?w (word.add addr ?x) ?y] |- _ ] => + replace (@word.add _ w (word.add addr x) y) with (@word.add _ w addr (word.add x y)) in H by ring + end. + Local Ltac word_add_trans addr := + repeat word_add_trans_one addr. + word_add_trans outAddr. + word_add_trans keyAddr. + word_add_trans nonceAddr. + repeat match goal with + | [ H : context[@word.add _ ?w (word.of_Z ?x) (word.of_Z ?y)] |- _ ] => + let z := eval cbv in (x + y) in + change (@word.add _ w (word.of_Z x) (word.of_Z y)) with (@word.of_Z _ w z) in H + end. repeat straightline. + subst c95. + match type of H with + | ?f m => set (Hsep := f) + end. + refine (tailrec (HList.polymorphic_list.nil) ("i"::"out"::"key"::"nonce"::"countervalue"::"x0"::"x1"::"x2"::"x3"::"x4"::"x5"::"x6"::"x7"::"x8"::"x9"::"x10"::"x11"::"x12"::"x13"::"x14"::"x15"::nil)%list%string (fun l t m i out key nonce cval _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => PrimitivePair.pair.mk (Hsep m) (fun T M I OUT KEY NONCE CVAL _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => T = t /\ Hsep m)) lt _ _ _ _ _); + cbn [reconstruct map.putmany_of_list HList.tuple.to_list + HList.hlist.foralls HList.tuple.foralls + HList.hlist.existss HList.tuple.existss + HList.hlist.apply HList.tuple.apply + HList.hlist + List.repeat Datatypes.length + HList.polymorphic_list.repeat HList.polymorphic_list.length + PrimitivePair.pair._1 PrimitivePair.pair._2] in *. + + { repeat straightline. } + { exact lt_wf. } + { exact (0%nat). } + { subst Hsep. + ecancel_assumption. } + { straightline. + straightline. + do 5 straightline. + straightline. + straightline. + do 100 straightline. + 2: solve [auto]. + straightline. + straightline. + straightline. + straightline. + do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. - letexists; split. - 1: { - repeat straightline. - letexists; split. - 1: { - Print Ltac straightline. - (* try subst v0; eapply Scalars.load_four_of_sep. *) - (* try subst v0; refine (@Scalars.load_four_of_sep _ (@word FE310CSemantics.parameters) (@byte FE310CSemantics.parameters) ltac:(typeclasses eauto) ltac:(typeclasses eauto) ltac:(typeclasses eauto) (@mem FE310CSemantics.parameters) ltac:(typeclasses eauto) _ _ _ _ _). *) - try subst v0; refine (@Scalars.load_four_of_sep _ (@word FE310CSemantics.parameters) (@byte FE310CSemantics.parameters) _ _ _ (@mem FE310CSemantics.parameters) _ _ _ _ _ _). - refine (Lift1Prop.subrelation_iff1_impl1 _ _ _ _ _ H). - ecancel. - Set Printing Implicit. - cbv [word32]. - cbn [Z.compare]. - ecancel. - cancel. - - let RHS := lazymatch goal with - | |- @Lift1Prop.iff1 _ _ (@seps _ _ _ ?RHS) => RHS - end in - let jy := index_and_element_of RHS in - let j := lazymatch jy with - | @pair _ _ ?i _ => i - end in - let y := lazymatch jy with - | @pair _ _ _ ?y => y - end in - assert_fails (idtac; (let y := rdelta.rdelta_var y in - is_evar y)); - (let LHS := lazymatch goal with - | |- @Lift1Prop.iff1 _ (@seps _ _ _ ?LHS) _ => LHS - end in - idtac LHS y). - let i := find_syntactic_unify_deltavar LHS y in - idtac). - simple refine (@cancel_seps_at_indices _ _ _ _ i j LHS RHS _ _); - idtac). - cbn[firstn skipn app hd tl]; - [ syntactic_unify._syntactic_exact_deltavar - (@RelationClasses.reflexivity _ _ - (@RelationClasses.Equivalence_Reflexive _ _ (Lift1Prop.Equivalence_iff1 _)) _) - | ]). - - let RHS := lazymatch goal with - | |- Lift1Prop.iff1 _ (seps ?RHS) => RHS - end in - let jy := index_and_element_of RHS in - let j := lazymatch jy with - | (?i, _) => i - end in - let y := lazymatch jy with - | (_, ?y) => y - end in - assert_fails idtac; (let y := rdelta.rdelta_var y in - is_evar y); - (let LHS := lazymatch goal with - | |- Lift1Prop.iff1 (seps ?LHS) _ => LHS - end in - let i := find_syntactic_unify_deltavar LHS y in - simple refine (cancel_seps_at_indices i j LHS RHS _ _); cbn[firstn skipn app hd tl]; - [ syntactic_exact_deltavar (RelationClasses.reflexivity _) | ]). - ecancel_step. - Print Ltac ecancel_step. - match goal with - | [ |- Lift1Prop.iff1 (seps ?lhs) (seps ?rhs) ] => - refine (cancel_seps_at_indices 1 0 lhs rhs _ _); cbn [firstn skipn app hd tl]; [reflexivity |] - end. - eapply RelationClasses.reflexivity. - cbn [seps]. - reflexivity. - } - 1: { - subst v v0. - reflexivity. - } - } - repeat straightline. From da5f6bd5f28f68ea97c4b73b001160c7045ca025 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 19 Apr 2019 18:50:52 -0400 Subject: [PATCH 05/12] expose some slowness --- bedrock2/src/bedrock2Examples/chacha20.v | 45 ++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index 2da7948e7..02686dca6 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -177,12 +177,56 @@ Proof. straightline. straightline. straightline. + Set Ltac Profiling. do 10 straightline. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. + Show Ltac Profile CutOff 0. + straightline. + + match goal with + | names:=_:string2ident.Context.list + |- @cmd _ _ (@cmd.set _ ?s ?e) _ _ _ ?post => + unfold1_cmd_goal; cbv beta match delta [cmd_body]; + (let names := eval cbv[names] in names in + let x := string2ident.lookup s names in + string2ident.ensure_free x; letexists _ as x; split) + end. +{ + do 57 straightline. + straightline. + straightline. + straightline. + straightline. + Print Ltac straightline. + match goal with + | |- exists x, ?P /\ ?Q => + let x := fresh x in + refine (let x := _ in ex_intro (fun x => P /\ Q) x _); split + end. + { + + Print Ltac straightline. + match goal with + | |- map.get _ _ = Some ?v => + let v' := rdelta.rdelta v in + is_evar v'; pose v' as X + end +. + + change v with X. subst X. + Time exact eq_refl. +(* Finished transaction in 1.907 secs (1.905u,0.s) (successful) *) + } + repeat straightline. + } + + + + Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. @@ -211,3 +255,4 @@ Proof. Time do 10 straightline. Time do 10 straightline. +Abort. \ No newline at end of file From c1b65592d08f614b741b27c98ba01f4bd05f69e6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 20 Apr 2019 21:07:01 -0400 Subject: [PATCH 06/12] cbv for map lookup seems rather difficult @jmgrosen @samuelgruetter --- bedrock2/src/bedrock2Examples/chacha20.v | 56 ++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index 02686dca6..c64227d31 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -218,6 +218,62 @@ Proof. . change v with X. subst X. +(* Goal : map.get l k = Some ?e , l = map.put k' ... *) +cbv [ + (* N.mul appears *) + map.get map.put + SortedList.map SortedList.parameters.key SortedList.parameters.value SortedListString.Build_parameters + SortedList.value SortedList.put + SortedList.eqb SortedList.parameters.ltb ltb Ascii.eqb Ascii.ltb Ascii.N_of_ascii Ascii.N_of_digits N.ltb Bool.eqb + List.find + SortedListString.map locals FE310CSemantics.parameters + l39 l38 l37 + fst snd + l0 + l1 + l2 + l3 + l4 + l5 + l6 + l7 + l8 + l9 + l10 + l11 + l12 + l13 + l14 + l15 + l16 + l17 + l18 + l19 + l20 + l21 + l22 + l23 + l24 + l25 + l26 + l27 + l28 + l29 + l30 + l31 + l32 + l33 + l34 + l35 + l36 + l37 + l38 + l39 + + + + ]. +revert dependent l. Time exact eq_refl. (* Finished transaction in 1.907 secs (1.905u,0.s) (successful) *) } From c92fdff50e2137a521aa9105a38618f735279fd9 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 22 Apr 2019 11:57:07 -0400 Subject: [PATCH 07/12] step through chacha20 loop body --- bedrock2/src/bedrock2Examples/chacha20.v | 145 +++++++---------------- 1 file changed, 46 insertions(+), 99 deletions(-) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index c64227d31..46e46d45b 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -177,118 +177,54 @@ Proof. straightline. straightline. straightline. - Set Ltac Profiling. do 10 straightline. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. - Show Ltac Profile CutOff 0. + Time do 10 straightline. straightline. - - match goal with - | names:=_:string2ident.Context.list - |- @cmd _ _ (@cmd.set _ ?s ?e) _ _ _ ?post => - unfold1_cmd_goal; cbv beta match delta [cmd_body]; - (let names := eval cbv[names] in names in - let x := string2ident.lookup s names in - string2ident.ensure_free x; letexists _ as x; split) - end. -{ - do 57 straightline. - straightline. - straightline. - straightline. - straightline. - Print Ltac straightline. - match goal with - | |- exists x, ?P /\ ?Q => - let x := fresh x in - refine (let x := _ in ex_intro (fun x => P /\ Q) x _); split - end. - { - - Print Ltac straightline. - match goal with - | |- map.get _ _ = Some ?v => - let v' := rdelta.rdelta v in - is_evar v'; pose v' as X - end -. - - change v with X. subst X. -(* Goal : map.get l k = Some ?e , l = map.put k' ... *) -cbv [ - (* N.mul appears *) - map.get map.put - SortedList.map SortedList.parameters.key SortedList.parameters.value SortedListString.Build_parameters - SortedList.value SortedList.put - SortedList.eqb SortedList.parameters.ltb ltb Ascii.eqb Ascii.ltb Ascii.N_of_ascii Ascii.N_of_digits N.ltb Bool.eqb - List.find - SortedListString.map locals FE310CSemantics.parameters - l39 l38 l37 - fst snd - l0 - l1 - l2 - l3 - l4 - l5 - l6 - l7 - l8 - l9 - l10 - l11 - l12 - l13 - l14 - l15 - l16 - l17 - l18 - l19 - l20 - l21 - l22 - l23 - l24 - l25 - l26 - l27 - l28 - l29 - l30 - l31 - l32 - l33 - l34 - l35 - l36 - l37 - l38 - l39 - - - - ]. -revert dependent l. - Time exact eq_refl. -(* Finished transaction in 1.907 secs (1.905u,0.s) (successful) *) - } - repeat straightline. - } - - - - Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + Time do 10 straightline. + + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + + (* prove [enforce] *) + match goal with |- Markers.unique (Markers.left (exists x131 x132 x133 x134 x135 x136 x137 x138 x139 x140 x141 x142 x143 x144 x145 x146 x147 x148 x149 x150 x151, _)) => idtac end. + + repeat letexists. split. + { + cbv [enforce gather]. + repeat match goal with + | |- context G [@map.get ?K ?V ?M ?m ?k] => + let v := match goal with H := context [map.put _ k ?v] |- _ => v end in + let goal := context G [Some v] in + change goal + end. + cbv beta iota. + split; exact eq_refl. + } + Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. @@ -310,5 +246,16 @@ revert dependent l. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. + Time do 10 straightline. + + letexists. split. + 2:split. + + all : repeat straightline. + all : try typeclasses eauto with core. + + subst v'. + revert dependent v. + (* GOAL: forall v : nat, (?Goal0 < v)%nat *) Abort. \ No newline at end of file From 746069428cb50cc4c8d2883dc04b4409b470ad01 Mon Sep 17 00:00:00 2001 From: John Grosen Date: Tue, 23 Apr 2019 23:12:33 -0400 Subject: [PATCH 08/12] get to Qed on basic chacha20 proof --- bedrock2/src/bedrock2Examples/chacha20.v | 132 ++++++++++++++++++++--- 1 file changed, 119 insertions(+), 13 deletions(-) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index 46e46d45b..e86955912 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -151,7 +151,7 @@ Proof. match type of H with | ?f m => set (Hsep := f) end. - refine (tailrec (HList.polymorphic_list.nil) ("i"::"out"::"key"::"nonce"::"countervalue"::"x0"::"x1"::"x2"::"x3"::"x4"::"x5"::"x6"::"x7"::"x8"::"x9"::"x10"::"x11"::"x12"::"x13"::"x14"::"x15"::nil)%list%string (fun l t m i out key nonce cval _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => PrimitivePair.pair.mk (Hsep m) (fun T M I OUT KEY NONCE CVAL _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => T = t /\ Hsep m)) lt _ _ _ _ _); + refine (tailrec (HList.polymorphic_list.nil) ("i"::"out"::"key"::"nonce"::"countervalue"::"x0"::"x1"::"x2"::"x3"::"x4"::"x5"::"x6"::"x7"::"x8"::"x9"::"x10"::"x11"::"x12"::"x13"::"x14"::"x15"::nil)%list%string (fun l t m i out key nonce cval _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => PrimitivePair.pair.mk (Hsep m /\ word.unsigned i = 10 - Z.of_nat l /\ (l <= 10)%nat) (fun T M I OUT KEY NONCE CVAL _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => T = t /\ OUT = out /\ KEY = key /\ NONCE = nonce /\ CVAL = cval /\ Hsep M)) lt _ _ _ _ _); cbn [reconstruct map.putmany_of_list HList.tuple.to_list HList.hlist.foralls HList.tuple.foralls HList.hlist.existss HList.tuple.existss @@ -163,16 +163,28 @@ Proof. { repeat straightline. } { exact lt_wf. } - { exact (0%nat). } - { subst Hsep. - ecancel_assumption. } + { split; [| split]. + { subst Hsep. + ecancel_assumption. } + { subst i. + rewrite word.unsigned_of_Z. + cbv [word.wrap]. + rewrite Zmod_0_l. + match goal with + | [ |- _ = _ - Z.of_nat ?n ] => + unify n (10%nat) + end. + reflexivity. + } + { blia. } + } { straightline. straightline. do 5 straightline. straightline. straightline. do 100 straightline. - 2: solve [auto]. + 2: solve [intuition]. straightline. straightline. straightline. @@ -197,8 +209,18 @@ Proof. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. - Time do 10 straightline. - + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. + Time straightline. Time straightline. Time straightline. Time straightline. @@ -222,9 +244,9 @@ Proof. change goal end. cbv beta iota. - split; exact eq_refl. + split; refine eq_refl. } - + Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. @@ -247,15 +269,99 @@ Proof. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. + Time straightline. + Time straightline. + Time straightline. letexists. split. 2:split. + 1: split. + 2: split. all : repeat straightline. all : try typeclasses eauto with core. - subst v'. - revert dependent v. - (* GOAL: forall v : nat, (?Goal0 < v)%nat *) + { + lazymatch goal with + | [ H : word.unsigned br <> 0 |- _ ] => + subst br; + rewrite word.unsigned_ltu in H; + lazymatch type of H with + | word.unsigned (if ?x _ => + destruct (Z.ltb_spec0 x y) as [Hv |]; + rewrite word.unsigned_of_Z in H; + cbv in H; + [| congruence] + end + end. + subst x131. + subst v'. + match goal with + | [ |- word.unsigned ?w = _ ] => + change w with (word.add x (word.of_Z 1)) + end. + rewrite word.unsigned_add, word.unsigned_of_Z. + match goal with + | [ H : word.unsigned _ = 10 - _ |- _ ] => + rewrite H in * + end. + rewrite word.unsigned_of_Z in Hv. + change (word.wrap 10) with 10 in Hv. + instantiate (1 := Nat.pred v). + rewrite Nat2Z.inj_pred; [| blia]. + change (word.wrap 1) with 1. + cbv [word.wrap]. + rewrite Z.mod_small; [blia |]. + split; [blia |]. + match goal with + | [ H : (_ <= _)%nat |- _ ] => + let H' := fresh "H" in + pose proof (inj_le _ _ H) as H'; cbn in H' + end. + match goal with + | [ |- _ < 2^?w ] => + let w' := eval cbv in w in + change w with w' + end. + blia. + } + { subst v'. blia. } + { subst v'. + lazymatch goal with + | [ H : word.unsigned br <> 0 |- _ ] => + subst br; + rewrite word.unsigned_ltu in H; + lazymatch type of H with + | word.unsigned (if ?x _ => + destruct (Z.ltb_spec0 x y) as [Hv |]; + rewrite word.unsigned_of_Z in H; + cbv in H; + [| congruence] + end + end. + match goal with + | [ H : word.unsigned _ = 10 - _ |- _ ] => + rewrite H in * + end. + rewrite word.unsigned_of_Z in Hv. + change (word.wrap 10) with 10 in Hv. + apply lt_pred_n_n. + apply Nat2Z.inj_lt. + blia. + } + } -Abort. \ No newline at end of file + subst Hsep. + repeat straightline. + replace (scalar32 x47 r) with (scalar32 (word.add x47 (word.of_Z 0)) r) in H8. + 2: { + f_equal. + 1: { + intros. + rewrite H9. + reflexivity. + } + ring. + } + repeat straightline. +Qed. From 0f95bf6104fa9674a67867e357d3ff36a3e668bd Mon Sep 17 00:00:00 2001 From: John Grosen Date: Tue, 23 Apr 2019 23:49:09 -0400 Subject: [PATCH 09/12] a more useful postcondition on chacha20 spec --- bedrock2/src/bedrock2Examples/chacha20.v | 39 ++++++++++++++++++++++-- 1 file changed, 37 insertions(+), 2 deletions(-) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index e86955912..6d14679e7 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -114,7 +114,11 @@ Instance spec_of_chacha20 : spec_of "chacha20_block" := fun functions => 8 = Z.of_nat (List.length key) -> 3 = Z.of_nat (List.length nonce) -> WeakestPrecondition.call functions "chacha20_block" t m [outAddr; keyAddr; nonceAddr; cval] - (fun t' m' rets => rets = []). + (fun t' m' rets => exists out', + t' = t /\ (array scalar32 (word.of_Z 4) outAddr out' * + array scalar32 (word.of_Z 4) keyAddr key * + array scalar32 (word.of_Z 4) nonceAddr nonce * + R) m' /\ rets = []). Hint Rewrite word.unsigned_of_Z word.signed_of_Z word.of_Z_unsigned word.unsigned_add word.unsigned_sub word.unsigned_opp word.unsigned_or word.unsigned_and word.unsigned_xor word.unsigned_not word.unsigned_ndn word.unsigned_mul word.signed_mulhss word.signed_mulhsu word.unsigned_mulhuu word.unsigned_divu word.signed_divs word.unsigned_modu word.signed_mods word.unsigned_slu word.unsigned_sru word.signed_srs word.unsigned_eqb word.unsigned_ltu word.signed_lts @@ -364,4 +368,35 @@ Proof. ring. } repeat straightline. -Qed. + intuition. + destruct out; cbn in H0; [| blia]. + cbn [array] in H19. + let x := open_constr:(@cons word32 _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ (cons _ nil)))))))))))))))) in + unify out' x. + subst out'. + cbn [array]. + repeat match goal with + | [ |- context[@word.add _ ?w (word.add x47 ?x) ?y] ] => + replace (@word.add _ w (word.add x47 x) y) with (@word.add _ w x47 (word.add x y)) by ring + end. + repeat match goal with + | [ |- context[@word.add _ ?w (word.add x16 ?x) ?y] ] => + replace (@word.add _ w (word.add x16 x) y) with (@word.add _ w x16 (word.add x y)) by ring + end. + repeat match goal with + | [ |- context[@word.add _ ?w (word.add x17 ?x) ?y] ] => + replace (@word.add _ w (word.add x17 x) y) with (@word.add _ w x17 (word.add x y)) by ring + end. + repeat match goal with + | [ |- context[@word.add _ ?w (word.of_Z ?x) (word.of_Z ?y)] ] => + let z := eval cbv in (x + y) in + change (@word.add _ w (word.of_Z x) (word.of_Z y)) with (@word.of_Z _ w z) + end. + rewrite !word.of_Z_unsigned in H19. + repeat match type of H19 with + | context[scalar32 ?a _] => + subst a + end. + replace (word.add x47 (word.of_Z 0)) with x47 in H19 by ring. + ecancel_assumption. +Defined. From 71a677798a448b9dc7b7b8e1683f7ffdd578400a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2022 11:28:49 -0400 Subject: [PATCH 10/12] Fix after rebase --- bedrock2/src/bedrock2Examples/chacha20.v | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index 6d14679e7..625f52db8 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -87,22 +87,19 @@ Example chacha20_block_c_string := Eval vm_compute in Print chacha20_block_c_string. *) +From Coq Require Import String. From Coq Require Import ZArith.ZArith. From coqutil Require Import Word.Interface Word.Properties Map.Interface. From coqutil.Word Require Import Naive. From coqutil.Tactics Require Import letexists eabstract. -From bedrock2 Require Import FE310CSemantics Semantics WeakestPrecondition ProgramLogic Array Scalars TailRecursion. +From bedrock2 Require Import FE310CSemantics Semantics WeakestPrecondition ProgramLogic Array Scalars Loops. From bedrock2.Map Require Import Separation SeparationLogic. From coqutil.Z Require Import Lia. Local Infix "*" := sep. Local Infix "*" := sep : type_scope. -Local Instance word32: Interface.word 32 := coqutil.Word.Naive.word 32 eq_refl. -Local Instance word32_ok: word.ok word32 := coqutil.Word.Naive.ok _ _. -Local Instance byte_ok: word.ok byte := coqutil.Word.Naive.ok _ _. -Local Instance mapok: map.ok mem := SortedListWord.ok (Naive.word 32 eq_refl) _. -Local Instance wordok: word.ok word := coqutil.Word.Naive.ok _ _. +Local Existing Instance coqutil.Word.Naive.word. Instance spec_of_chacha20 : spec_of "chacha20_block" := fun functions => forall outAddr out keyAddr key nonceAddr nonce cval R m t, @@ -125,9 +122,6 @@ Hint Rewrite using trivial : word_laws. -Monomorphic Definition word__monomorphic_ring_theory := Properties.word.ring_theory (word := word). -Add Ring word_ring : word__monomorphic_ring_theory. - Lemma chacha20_ok : program_logic_goal_for_function! chacha20_block. Proof. straightline. @@ -199,7 +193,6 @@ Proof. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. - Time do 10 straightline. straightline. Time do 10 straightline. Time do 10 straightline. @@ -239,7 +232,7 @@ Proof. match goal with |- Markers.unique (Markers.left (exists x131 x132 x133 x134 x135 x136 x137 x138 x139 x140 x141 x142 x143 x144 x145 x146 x147 x148 x149 x150 x151, _)) => idtac end. repeat letexists. split. - { + { cbv [enforce gather]. repeat match goal with | |- context G [@map.get ?K ?V ?M ?m ?k] => @@ -273,6 +266,7 @@ Proof. Time do 10 straightline. Time do 10 straightline. Time do 10 straightline. + Time do 10 straightline. Time straightline. Time straightline. Time straightline. From 1771f630ae43aa3743c1b9146ce37f495b56d4dc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2022 12:24:30 -0400 Subject: [PATCH 11/12] Add back ring instance --- bedrock2/src/bedrock2Examples/chacha20.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/bedrock2/src/bedrock2Examples/chacha20.v b/bedrock2/src/bedrock2Examples/chacha20.v index 625f52db8..7dde85e39 100644 --- a/bedrock2/src/bedrock2Examples/chacha20.v +++ b/bedrock2/src/bedrock2Examples/chacha20.v @@ -122,6 +122,8 @@ Hint Rewrite using trivial : word_laws. +Import BasicC64Semantics. (* for ring *) + Lemma chacha20_ok : program_logic_goal_for_function! chacha20_block. Proof. straightline. From ba6b597f19b867a0c7c0e556b1924b06fbcdbd81 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 22 Jul 2022 12:38:12 -0400 Subject: [PATCH 12/12] Improve perf of straightline_cleanup --- bedrock2/src/bedrock2/ProgramLogic.v | 103 +++++++++++++++------------ 1 file changed, 57 insertions(+), 46 deletions(-) diff --git a/bedrock2/src/bedrock2/ProgramLogic.v b/bedrock2/src/bedrock2/ProgramLogic.v index e82632cd2..1e5f66588 100644 --- a/bedrock2/src/bedrock2/ProgramLogic.v +++ b/bedrock2/src/bedrock2/ProgramLogic.v @@ -98,54 +98,65 @@ Ltac enter f := Require coqutil.Map.SortedList. (* special-case eq_refl *) -Ltac straightline_cleanup := - match goal with +From Ltac2 Require Notations Control. +Module Ltac2ForPerf. + Import Ltac2.Notations Ltac2.Init. + Ltac2 straightline_cleanup_clear () := + let h := Control.hyps () in + let should_clear_type ty := (match! ty with (* TODO remove superfluous _ after .rep, but that will break some proofs that rely on x not being cleared to instantiate evars with terms depending on x *) - | x : Word.Interface.word.rep _ |- _ => clear x - | x : Init.Byte.byte |- _ => clear x - | x : Semantics.trace |- _ => clear x - | x : Syntax.cmd |- _ => clear x - | x : Syntax.expr |- _ => clear x - | x : coqutil.Map.Interface.map.rep |- _ => clear x - | x : BinNums.Z |- _ => clear x - | x : unit |- _ => clear x - | x : bool |- _ => clear x - | x : list _ |- _ => clear x - | x : nat |- _ => clear x - (* same TODO as above *) - | x := _ : Word.Interface.word.rep _ |- _ => clear x - | x := _ : Init.Byte.byte |- _ => clear x - | x := _ : Semantics.trace |- _ => clear x - | x := _ : Syntax.cmd |- _ => clear x - | x := _ : Syntax.expr |- _ => clear x - | x := _ : coqutil.Map.Interface.map.rep |- _ => clear x - | x := _ : BinNums.Z |- _ => clear x - | x := _ : unit |- _ => clear x - | x := _ : bool |- _ => clear x - | x := _ : list _ |- _ => clear x - | x := _ : nat |- _ => clear x - | |- forall _, _ => intros - | |- let _ := _ in _ => intros - | |- dlet.dlet ?v (fun x => ?P) => change (let x := v in P); intros - | _ => progress (cbn [Semantics.interp_binop] in * ) - | H: exists _, _ |- _ => destruct H - | H: _ /\ _ |- _ => destruct H - | x := ?y |- ?G => is_var y; subst x - | H: ?x = ?y |- _ => constr_eq x y; clear H - | H: ?x = ?y |- _ => is_var x; is_var y; assert_fails (idtac; let __ := eval cbv [x] in x in idtac); subst x - | H: ?x = ?y |- _ => is_var x; is_var y; assert_fails (idtac; let __ := eval cbv [y] in y in idtac); subst y - | H: ?x = ?v |- _ => - is_var x; - assert_fails (idtac; let __ := eval cbv delta [x] in x in idtac); - lazymatch v with context[x] => fail | _ => idtac end; - let x' := fresh x in - rename x into x'; - simple refine (let x := v in _); - change (x' = x) in H; - symmetry in H; - destruct H - end. + | Word.Interface.word.rep _ => true + | Init.Byte.byte => true + | Semantics.trace => true + | Syntax.cmd => true + | Syntax.expr => true + | coqutil.Map.Interface.map.rep => true + | BinNums.Z => true + | unit => true + | bool => true + | list _ => true + | nat => true + | _ => false + end) in + let h := List.filter (fun (name, body, ty) => should_clear_type ty) h in + progress (List.iter (fun (name, _, _) => try (clear $name)) h). +End Ltac2ForPerf. + +Ltac straightline_cleanup := + first [ ltac2:(Ltac2ForPerf.straightline_cleanup_clear ()) + | match goal with + | |- forall _, _ => idtac + | |- let _ := _ in _ => idtac + end; + intros + | match goal with + | |- dlet.dlet ?v (fun x => ?P) => change (let x := v in P) + end; intros + | progress (cbn [Semantics.interp_binop] in * ) + | let H := match goal with + | H: exists _, _ |- _ => H + | H: _ /\ _ |- _ => H + end in + destruct H + | match goal with + | x := ?y |- ?G => is_var y; subst x + end + | let H := multimatch goal with | H: ?x = ?v |- _ => H end in + let x := lazymatch type of H with ?x = ?y => x end in + let y := lazymatch type of H with ?x = ?y => y end in + first [ constr_eq x y; clear H + | is_var x; is_var y; assert_fails (idtac; let __ := eval cbv [x] in x in idtac); subst x + | is_var x; is_var y; assert_fails (idtac; let __ := eval cbv [y] in y in idtac); subst y + | is_var x; + assert_fails (idtac; let __ := eval cbv delta [x] in x in idtac); + lazymatch y with context[x] => fail | _ => idtac end; + let x' := fresh x in + rename x into x'; + simple refine (let x := y in _); + change (x' = x) in H; + symmetry in H; + destruct H ] ]. Import WeakestPrecondition. Import coqutil.Map.Interface.