cleanup

3 files changed, 89 insertions, 133 deletions

diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v
index f7151a283..ffe9a4942 100644
--- a/src/Fancy/Barrett256.v
+++ b/src/Fancy/Barrett256.v
@@ -182,48 +182,6 @@ Module Barrett256.
     reflexivity.
   Qed.
 
-  Local Ltac solve_bounds :=
-    match goal with
-    | H : ?a = ?b mod ?c |- 0 <= ?a < ?c => rewrite H; apply Z.mod_pos_bound; omega
-    | _ => assumption
-    end.
-  Local Ltac results_equiv :=
-    match goal with
-      |- ?lhs = ?rhs =>
-      match lhs with
-        context [spec ?li ?largs ?lcc] =>
-        match rhs with
-          context [spec ?ri ?rargs ?rcc] =>
-          replace (spec li largs lcc) with (spec ri rargs rcc)
-        end
-      end
-    end.
-  Local Ltac simplify_cc :=
-    match goal with
-      |- context [CC.update ?to_write ?result ?cc_spec ?old_state] =>
-      let e := eval cbv -[spec cc_spec CC.cc_l CC.cc_m CC.cc_z CC.cc_c] in
-      (CC.update to_write result cc_spec old_state) in
-          change (CC.update to_write result cc_spec old_state) with e
-    end.
-  Ltac remember_single_result :=
-    match goal with |- context [(spec ?i ?args ?cc) mod ?w] =>
-                    let x := fresh "x" in
-                    let y := fresh "y" in
-                    let Heqx := fresh "Heqx" in
-                    remember (spec i args cc) as x eqn:Heqx;
-                    remember (x mod w) as y
-    end.
-  Local Ltac step :=
-    match goal with
-      |- interp _ _ _ (Instr ?i ?rd1 ?args1 ?cont1) ?cc1 ?ctx1 =
-         interp _ _ _ (Instr ?i ?rd2 ?args2 ?cont2) ?cc2 ?ctx2 =>
-      rewrite (interp_step _ _ i rd1 args1 cont1);
-      rewrite (interp_step _ _ i rd2 args2 cont2)
-    end;
-    cbn - [interp spec cc_spec];
-    repeat progress rewrite ?reg_eqb_neq, ?reg_eqb_refl by congruence;
-    results_equiv; [ remember_single_result; repeat simplify_cc | try reflexivity ].
-
   Local Notation interp := (interp reg_eqb wordmax cc_spec).
   Lemma barrett_red256_alloc_equivalent errorP errorR cc_start_state start_context :
     forall x xHigh RegMuLow scratchp1 scratchp2 scratchp3 scratchp4 scratchp5 extra_reg,
@@ -256,62 +214,51 @@ Module Barrett256.
            | H : ~ False |- _ => clear H
            end.
 
-    repeat step_lhs.
-
-
-    repeat step_rhs.
-    rewrite interp_Mul256x256 with (tmp2 := extra_reg) by
-        (try congruence; push_value_unused).
-    repeat step_rhs.
-    rewrite mulhh_comm by simplify_with_register_properties.
-    repeat step_rhs.
-    rewrite mulll_comm by simplify_with_register_properties.
-    repeat step_rhs.
+    Ltac simplify_with_register_properties ::=
+      repeat
+        match goal with
+        | _ => rewrite reg_eqb_refl
+        | _ => rewrite reg_eqb_neq by (assumption || congruence) 
+        | H:?y = _ mod ?m |- 0 <= ?y < _ => rewrite H; apply Z.mod_pos_bound; lia
+        | _ => assumption
+        end.
+    Ltac cleanup ::=
+      cbn-[Spec.interp spec cc_spec]; simplify_with_register_properties;
+      cbv[CC.update in_dec list_rec list_rect CC.code_dec]; cbn[CC.cc_c CC.cc_m CC.cc_z CC.cc_l].
 
-    rewrite swap_add_chain
-      by
-        repeat match goal with
-               | |- _ <> _ => congruence
-               | _ => progress simplify_with_register_properties
-               | |- _ = 2 ^ 256 => reflexivity
-               | |- flags_unused _ _ =>
-                 cbv [flags_unused]; intros;
-                   do 2 step; reflexivity
-               end.
-    repeat step_rhs.
 
-    assert (0 < 2 ^ 256) by ZeroBounds.Z.zero_bounds.
-    rewrite add_comm by simplify_with_register_properties.
-    step_rhs.
-    rewrite addc_comm by simplify_with_register_properties.
-    step_rhs.
-    rewrite add_comm by simplify_with_register_properties.
-    step_rhs.
-    rewrite addc_comm by simplify_with_register_properties.
-    step_rhs.
-    repeat step_rhs.
-    rewrite interp_Mul256x256 with (tmp2 := extra_reg) by
-        (try congruence; push_value_unused).
-    repeat step_rhs.
-    rewrite mulhh_comm by simplify_with_register_properties.
-    repeat step_rhs.
-    rewrite mulll_comm by simplify_with_register_properties.
-    repeat step_rhs.
-
-    rewrite swap_add_chain;
-        repeat match goal with
-               | |- _ <> _ => congruence
-               | _ => progress simplify_with_register_properties
-               | |- _ = 2 ^ 256 => reflexivity
-               | |- flags_unused _ _ =>
-                 cbv [flags_unused]; intros;
-                   repeat (step; try reflexivity)
-               end.
-
-    repeat step_rhs.
+    Ltac prove_programs_equivalent :=
+      repeat step_lhs; (* remember the results of each step on the LHS *)
+      repeat match goal with
+             | _ => step_rhs
+             | |- ?x = ?x => reflexivity
+             | _ => rewrite mulhh_comm by simplify_with_register_properties; step_rhs
+             | _ => rewrite mulll_comm by simplify_with_register_properties; step_rhs
+             | _ => rewrite add_comm by simplify_with_register_properties; step_rhs
+             | _ => rewrite addc_comm by simplify_with_register_properties; step_rhs
+             | _ => rewrite mullh_mulhl; step_rhs
+             | _ => rewrite <-mullh_mulhl; step_rhs
+             end.
+    Time repeat match goal with
+                | _ => progress prove_programs_equivalent
+                | _ => rewrite interp_Mul256x256 with (tmp2 := extra_reg) by
+                      (match goal with
+                       | |- _ <> _ => assumption || congruence
+                       | _ => push_value_unused
+                       end)
+                | _ => 
+                  rewrite swap_add_chain by
+                      repeat match goal with
+                             | |- _ <> _ => assumption || congruence
+                             | _ => progress simplify_with_register_properties
+                             | |- _ = 2 ^ 256 => reflexivity
+                             | |- flags_unused _ _ =>
+                               cbv [flags_unused]; intros; prove_programs_equivalent (* TODO: there is probably a faster way to do this one *)
+                             end
+                end.
 
     cbv [Spec.interp].
-    rewrite !reg_eqb_refl.
+    simplify_with_register_properties.
     reflexivity.
   Qed.
 
diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v
index bf18124ed..a4b27c561 100644
--- a/src/Fancy/Montgomery256.v
+++ b/src/Fancy/Montgomery256.v
@@ -101,6 +101,15 @@ Module Montgomery256.
            | |- of_prefancy_scalar _ _ _ _ = _ => cbn; solve [eauto]
            end.
 
+  (* TODO(jgross): switch out casts *)
+  (* might need to use CheckCasts.interp_eqv_without_casts? *)
+  Lemma swap_casts lo hi :
+    expr.interp (@ident.gen_interp cast_oor)
+                (invert_expr.smart_App_curried (montred256 (type.interp base.interp)) (lo, (hi, tt))) =
+    expr.interp (@ident.interp)
+                (invert_expr.smart_App_curried (montred256 (type.interp base.interp)) (lo, (hi, tt))).
+  Admitted.
+
   Lemma montred256_fancy_correct :
     forall lo hi error,
       0 <= lo < R ->
@@ -149,11 +158,8 @@ Module Montgomery256.
       econstructor. valid_expr_subgoal. }
     { cbn - [montred256]. cbv [id].
       f_equal.
-      (* TODO(jgross): switch out casts *)
-      (* might need to use CheckCasts.interp_eqv_without_casts? *)
-      replace (@ident.gen_interp cast_oor) with (@ident.interp) by admit.
-      reflexivity. }
-  Admitted.
+      apply swap_casts. }
+  Qed.
 
   Import Spec.Registers.
 
@@ -209,29 +215,21 @@ Module Montgomery256.
            | H : ~ False |- _ => clear H
            end.
 
-    (* TODO: the manual steps here can probably be replaced with a
-    tactic *)
-    
-    repeat step_lhs.
-    rewrite interp_Mul256 with (tmp2:=extra_reg) by (congruence || push_value_unused).
-
-    rewrite mullh_mulhl.
-    step_rhs.
-    rewrite <-mullh_mulhl.
-    repeat step_rhs.
-    
-    rewrite interp_Mul256x256 with (tmp2:=extra_reg) by (congruence || push_value_unused).
-    rewrite mulhh_comm by simplify_with_register_properties.
-    repeat step_rhs.
-    rewrite mulll_comm by simplify_with_register_properties.
-    repeat step_rhs.
-    rewrite add_comm by simplify_with_register_properties.
-    step_rhs.
-    rewrite addc_comm by simplify_with_register_properties.
-    repeat step_rhs.
-    
+    Time repeat match goal with
+                | _ => progress prove_programs_equivalent
+                | _ => rewrite interp_Mul256 with (tmp2 := extra_reg) by
+                      (match goal with
+                       | |- _ <> _ => assumption || congruence
+                       | _ => push_value_unused
+                       end)
+                | _ => rewrite interp_Mul256x256 with (tmp2 := extra_reg) by
+                      (match goal with
+                       | |- _ <> _ => assumption || congruence
+                       | _ => push_value_unused
+                       end)
+                end.
 
-    cbn; repeat progress rewrite ?reg_eqb_neq, ?reg_eqb_refl by congruence.
+    cbn [Spec.interp]; simplify_with_register_properties.
     reflexivity.
   Qed.
 
diff --git a/src/Fancy/Prod.v b/src/Fancy/Prod.v
index a46a7a4f0..de5680727 100644
--- a/src/Fancy/Prod.v
+++ b/src/Fancy/Prod.v
@@ -85,9 +85,19 @@ Section Prod.
                                                                                                                       (Ret x))))))))))))))).
 End Prod.
 
+(* Solves subgoals for commutativity proofs and simplifies register
+lookup expressions *)
+Ltac simplify_with_register_properties :=
+  repeat
+    match goal with
+    | _ => rewrite reg_eqb_refl
+    | _ => rewrite reg_eqb_neq by (assumption || congruence) 
+    | H:?y = _ mod ?m |- 0 <= ?y < _ => rewrite H; apply Z.mod_pos_bound; lia
+    | _ => assumption
+    end.
 Ltac cleanup :=
   cbn - [interp spec cc_spec];
-  rewrite ?reg_eqb_refl, ?reg_eqb_neq by congruence;
+  simplify_with_register_properties;
   cbv [CC.update in_dec list_rec list_rect
                  CC.code_dec];
   cbn [CC.cc_c CC.cc_m CC.cc_z CC.cc_l].
@@ -110,6 +120,18 @@ Ltac step_rhs :=
   | H : ?y = (?x mod ?m)%Z |- context [(?x mod ?m)%Z] =>
     rewrite <-H
   end.
+Ltac prove_programs_equivalent :=
+  repeat step_lhs; (* remember the results of each step on the LHS *)
+  repeat match goal with
+         | _ => step_rhs
+         | |- ?x = ?x => reflexivity
+         | _ => rewrite mulhh_comm by simplify_with_register_properties; step_rhs
+         | _ => rewrite mulll_comm by simplify_with_register_properties; step_rhs
+         | _ => rewrite add_comm by simplify_with_register_properties; step_rhs
+         | _ => rewrite addc_comm by simplify_with_register_properties; step_rhs
+         | _ => rewrite mullh_mulhl; step_rhs
+         | _ => rewrite <-mullh_mulhl; step_rhs
+         end.
 
 Section ProdEquiv.
   Context (wordmax : Z).
@@ -375,15 +397,4 @@ Ltac push_value_unused :=
          | _ => apply not_in_cons; split;
                 [ try assumption; symmetry; assumption | ]
          | _ => apply in_nil
-         end.
-
-(* Solves subgoals for commutativity proofs and simplifies register
-lookup expressions *)
-Ltac simplify_with_register_properties :=
-  repeat match goal with
-         | _ => rewrite reg_eqb_refl
-         | _ => rewrite reg_eqb_neq by congruence
-         | H : ?y = _ mod ?m |- 0 <= ?y < _ =>
-           rewrite H; apply Z.mod_pos_bound; lia
-         | _ => assumption
          end.
\ No newline at end of file