make kyberslash work

mit-plv · Sep 30, 2024 · b8f0f55 · b8f0f55
1 parent ecef319
commit b8f0f55
Show file tree

Hide file tree

Showing 6 changed files with 29 additions and 44 deletions.
diff --git a/bedrock2/src/bedrock2/LeakageProgramLogic.v b/bedrock2/src/bedrock2/LeakageProgramLogic.v
@@ -258,32 +258,17 @@ Ltac straightline :=
   match goal with
   | _ => straightline_cleanup
   | |- Basics.impl _ _ => cbv [Basics.impl] (*why does swap break without this?*)
-  (*| |- program_logic_goal_for ?f _ =>
+  | |- program_logic_goal_for ?f _ =>
       enter f; intros;
-      repeat
-        match goal with
-        | H:?P ?functions |- _ =>
-            match type of functions with
-            | list (String.string * Syntax.func) =>
-                let f := fresh "f" in destruct H as [f H]
-            end
-        end;
       match goal with
-      | |- call _ _ _ _ _ _ _ => idtac
-      | _ => eexists
-      end; intros; unfold1_call_goal; cbv beta match delta [call_body];
-      lazymatch goal with
-      | |- if ?test then ?T else _ => replace test with true by reflexivity; change T
+      | |- LeakageWeakestPrecondition.call _ _ _ _ _ _ _ => idtac
+      | |- exists _, _ => eexists
+      end; intros;
+      match goal with
+      | H: map.get ?functions ?fname = Some _ |- _ =>
+          eapply start_func; [exact H | clear H]
       end;
-      cbv beta match delta [func]*)
-  (*old thing
-    | |- program_logic_goal_for ?f _ =>
-    enter f; intros;
-    match goal with
-    | H: map.get ?functions ?fname = Some _ |- _ =>
-        eapply start_func; [exact H | clear H]
-    end;
-    cbv match beta delta [LeakageWeakestPrecondition.func]*)
+      cbv match beta delta [LeakageWeakestPrecondition.func]
   | |- LeakageWeakestPrecondition.cmd _ (cmd.set ?s ?e) _ _ _ _ ?post =>
     unfold1_cmd_goal; cbv beta match delta [cmd_body];
     let __ := match s with String.String _ _ => idtac | String.EmptyString => idtac end in
@@ -358,7 +343,7 @@ Ltac straightline :=
   | |- exists x, ?P /\ ?Q => (*unsure whether still need this, or just case below*)
     let x := fresh x in refine (let x := _ in ex_intro (fun x => P /\ Q) x _);
                         split; [solve [repeat straightline]|]
-  | |- exists x y, ?P /\ ?Q => idtac "33'";
+  | |- exists x y, ?P /\ ?Q =>
     let x := fresh x in let y := fresh y in
              refine (let x := _ in let y := _ in
              ex_intro (fun x => exists y, P /\ Q) x
@@ -376,7 +361,7 @@ Ltac straightline :=
   | |- Markers.unique (exists x, Markers.split (?P /\ ?Q)) => (*unsure whether we still need this, or just need case below*)
     let x := fresh x in refine (let x := _ in ex_intro (fun x => P /\ Q) x _);
                         split; [solve [repeat straightline]|]
-  | |- Markers.unique (exists x y, Markers.split (?P /\ ?Q)) => idtac "35'";
+  | |- Markers.unique (exists x y, Markers.split (?P /\ ?Q)) =>
     let x := fresh x in let y := fresh y in
              refine (let x := _ in let y := _ in
              ex_intro (fun x => exists y, P /\ Q) x

diff --git a/bedrock2/src/bedrock2/LeakageSemantics.v b/bedrock2/src/bedrock2/LeakageSemantics.v
@@ -67,7 +67,7 @@ Existing Class PickSp.
 
 Section binops.
   Context {width : Z} {BW : Bitwidth width} {word : Word.Interface.word width}.
-  Definition leak_binop (bop : bopname) (x1 : word) (x2 : word) (k : leakage) : leakage :=
+  Definition leak_binop (bop : bopname) (x1 : word) (x2 : word) : leakage :=
     match bop with
     | bopname.divu | bopname.remu => cons (leak_word x2) (cons (leak_word x1) nil)
     | bopname.sru | bopname.slu | bopname.srs => cons (leak_word x2) nil
@@ -101,7 +101,7 @@ Section semantics.
       | expr.op op e1 e2 =>
           '(v1, k') <- eval_expr e1 k;
           '(v2, k'') <- eval_expr e2 k';
-          Some (interp_binop op v1 v2, leak_binop op v1 v2 k'')
+          Some (interp_binop op v1 v2, leak_binop op v1 v2 ++ k'')
       | expr.ite c e1 e2 =>
           '(vc, k') <- eval_expr c k;
           let b := word.eqb vc (word.of_Z 0) in

diff --git a/bedrock2/src/bedrock2/LeakageWeakestPrecondition.v b/bedrock2/src/bedrock2/LeakageWeakestPrecondition.v
@@ -29,7 +29,7 @@ Section WeakestPrecondition.
       | expr.op op e1 e2 =>
         rec k e1 (fun k' v1 =>
         rec k' e2 (fun k'' v2 =>
-        post (leak_binop op v1 v2 k'') (interp_binop op v1 v2)))
+        post (leak_binop op v1 v2 ++ k'') (interp_binop op v1 v2)))
       | expr.load s e =>
         rec k e (fun k' a =>
         load s m a (post (leak_word a :: k')))
@@ -153,7 +153,7 @@ Ltac unfold1_expr e :=
   lazymatch e with
     @expr ?width ?BW ?word ?mem ?locals ?m ?l ?k ?arg ?post =>
     let arg := eval hnf in arg in
-    constr:(@expr_body width BW word mem locals m l k (@expr width BW word mem locals m l k) arg post)
+    constr:(@expr_body width BW word mem locals m l (@expr width BW word mem locals m l) k arg post)
   end.
 Ltac unfold1_expr_goal :=
   let G := lazymatch goal with |- ?G => G end in

diff --git a/bedrock2/src/bedrock2/LeakageWeakestPreconditionProperties.v b/bedrock2/src/bedrock2/LeakageWeakestPreconditionProperties.v
@@ -56,6 +56,8 @@ Section WeakestPrecondition.
       cbv [pointwise_relation Basics.impl]. auto. }
     { eapply IHa2; eauto; intuition idtac. eapply Proper_load; eauto using Proper_load.
       cbv [pointwise_relation Basics.impl]. auto. }
+    { eapply IHa2_1; eauto; intuition idtac.
+      eapply IHa2_2; eauto; intuition idtac. eauto. }
     { eapply IHa2_1; eauto; intuition idtac.
       Tactics.destruct_one_match; eauto using Proper_load. }
   Qed.

diff --git a/bedrock2/src/bedrock2/MetricLeakageSemantics.v b/bedrock2/src/bedrock2/MetricLeakageSemantics.v
@@ -45,7 +45,7 @@ Section semantics.
       | expr.op op e1 e2 =>
           '(v1, k', mc') <- eval_expr e1 k mc;
           '(v2, k'', mc'') <- eval_expr e2 k' mc';
-          Some (interp_binop op v1 v2, leak_binop op v1 v2 k'', cost_op isRegStr UNK UNK UNK mc'')
+          Some (interp_binop op v1 v2, leak_binop op v1 v2 ++ k'', cost_op isRegStr UNK UNK UNK mc'')
       | expr.ite c e1 e2 =>
           '(vc, k', mc') <- eval_expr c k mc;
           let b := word.eqb vc (word.of_Z 0) in

diff --git a/bedrock2/src/bedrock2Examples/kyberslash.v b/bedrock2/src/bedrock2Examples/kyberslash.v
@@ -157,7 +157,7 @@ Section WithWord.
                List.repeat Datatypes.length
                HList.polymorphic_list.repeat HList.polymorphic_list.length
                PrimitivePair.pair._1 PrimitivePair.pair._2] in *.
-      { cbv [Loops.enforce]; cbn.
+      { cbv [LeakageLoops.enforce]; cbn.
           subst l l0.
           repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn). split.
           { exact eq_refl. }
@@ -216,7 +216,7 @@ Section WithWord.
             rewrite <- Ex1 in H3.
             ecancel_assumption. }
           repeat straightline. (* neat, why did that work now? *)
-          refine ((Loops.tailrec
+          refine ((LeakageLoops.tailrec
                      (* types of ghost variables*) (let c := HList.polymorphic_list.cons in c _ (c _ HList.polymorphic_list.nil))
                      (* program variables *) ("j" :: "i" :: "a_coeffs" :: "msg" :: nil))%string
                     (fun vj msg_vals a_coeffs_vals k t m j i a_coeffs msg =>
@@ -244,11 +244,11 @@ Section WithWord.
                    List.repeat Datatypes.length
                    HList.polymorphic_list.repeat HList.polymorphic_list.length
                    PrimitivePair.pair._1 PrimitivePair.pair._2] in *.
-          { cbv [Loops.enforce]; cbn.
+          { cbv [LeakageLoops.enforce]; cbn.
             subst l.
             repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn). split.
             { exact eq_refl. }
-            { eapply map.map_ext; intros k0.
+            { eapply map.map_ext; intros k0'.
               repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec, ?map.get_empty; cbn -[String.eqb]).
               repeat (destruct String.eqb; trivial). } }
           { exact (Z.lt_wf _). }
@@ -427,11 +427,11 @@ Section WithWord.
                 repeat straightline. }
               repeat straightline.
               do 4 eexists. Print enforce. Print gather. split.
-              { Print enforce. repeat straightline. Print Loops.enforce. cbv [Loops.enforce]; cbn.
+              { Print enforce. repeat straightline. Print LeakageLoops.enforce. cbv [LeakageLoops.enforce]; cbn.
                 subst l6 l5 l4 l3 l2 l1 l0 l localsmap.
                 repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn). split.
                 { exact eq_refl. }
-                { eapply map.map_ext; intros k0.
+                { eapply map.map_ext; intros k0'.
                   repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec, ?map.get_empty; cbn -[String.eqb]).
                   repeat (destruct String.eqb; trivial). } }
               seprewrite_in (symmetry! @array_cons) H12.
@@ -471,7 +471,7 @@ Section WithWord.
               1,2,3: auto.
               subst v0. replace (Z.to_nat (8 mod 2 ^ width - word.unsigned x6)) with
                 (S (Z.to_nat (8 - word.unsigned (word.add x6 (word.of_Z 1))))).
-              { cbn [get_inner_leakage]. 
+              { cbn [get_inner_leakage].
                 rewrite H22. repeat rewrite app_assoc. Search (_ :: _ ++ _)%list.
                 assert (app_one_cons : forall A (a : A) l, (a :: l = (cons a nil) ++ l)%list).
                 { reflexivity. }
@@ -480,10 +480,7 @@ Section WithWord.
                 { f_equal.
                   { instantiate (1 := fun _ _ => _). simpl. reflexivity. }
                   { instantiate (1 := fun _ _ => _). simpl. reflexivity. } }
-                repeat (rewrite List.app_assoc || rewrite (app_one_cons _ _ (_ ++ k)%list)).
-                f_equal.
-                repeat rewrite <- List.app_assoc.
-                instantiate (1 := fun _ _ => _). simpl. reflexivity. }
+                instantiate (1 := fun _ _ => _). simpl. align_trace. }
               clear H22. rewrite word.unsigned_add. clear H12. cbv [word.wrap].
               rewrite word.unsigned_of_Z. cbv [word.wrap]. rewrite (Z.mod_small 1) by blia.
               rewrite (Z.mod_small 8) by blia. rewrite Z.mod_small.
@@ -511,7 +508,7 @@ Section WithWord.
                 reflexivity. }
             repeat straightline. }
           repeat straightline. eexists. eexists. eexists. split.
-          { cbv [Loops.enforce]; cbn.
+          { cbv [LeakageLoops.enforce]; cbn.
             subst l l0.
             repeat (rewrite ?map.get_put_dec, ?map.get_remove_dec; cbn). split.
             { exact eq_refl. }
@@ -543,15 +540,16 @@ Section WithWord.
           repeat straightline. eexists. eexists. split; [|split; [|split] ].
           3: ecancel_assumption.
           1,2: assumption.
-          subst k0. subst k'. subst k''.
+          simpl. subst k1. subst k'. subst k''.
           replace (Z.to_nat v0) with (S (Z.to_nat
               (word.unsigned (word:=word) (word.divu (word.of_Z KYBER_N) (word.of_Z 8)) -
                  word.unsigned (word.add x1 (word.of_Z 1))))).
           { cbn [get_outer_leakage].
             rewrite H17. clear H17.
             assert (app_one_cons : forall A (a : A) l, (a :: l = (cons a nil) ++ l)%list).
             { reflexivity. }
-            repeat (rewrite List.app_assoc || rewrite (app_one_cons _ _ (_ ++ k)%list)).
+            simpl. Print align_trace. Check align_trace_app.
+            repeat (rewrite List.app_assoc || rewrite (app_one_cons _ _ (_ ++ k0)%list) || rewrite (app_one_cons _ _ k0)).
             f_equal. repeat rewrite <- List.app_assoc. f_equal.
             2: { instantiate (1 := fun _ => _). cbv beta. simpl. reflexivity. }
             f_equal.