comment out broken code so things build

1 files changed, 11 insertions, 53 deletions

diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v
index d14d9a1b4..10bfd1af0 100644
--- a/src/Experiments/NewPipeline/Toplevel2.v
+++ b/src/Experiments/NewPipeline/Toplevel2.v
@@ -2375,10 +2375,11 @@ Module Barrett256.
                | |- Fancy.of_prefancy_scalar _ _ _ _ = _ => cbn; solve [eauto]
                end.
 
+      admit.
+      (* TODO: this code is currently broken because there are unexpected redundant ands in the code *)
+      (*
       repeat (econstructor; [ solve [sub] | intros ]).
       econstructor.
-      { sub. Print Fancy.valid_scalar.
-      [ solve [sub] | intros ].
       (* For the too-tight RSHI cast, we have to loosen the bounds *)
       eapply Fancy.valid_LetInZ_loosen; try solve [sub];
         [ cbn; omega | | intros; apply loosen_rshi_subgoal; solve [eauto] ].
@@ -2387,7 +2388,9 @@ Module Barrett256.
       { sub. admit.
       (* TODO: this is the too-tight RSHI cast *) }
       repeat (econstructor; [ solve [sub] | intros ]).
-      econstructor. sub. }
+      econstructor. sub. *)
+
+    }
     { cbn - [barrett_red256].
       cbv [id].
       cbv [expr.Interp].
@@ -2532,6 +2535,7 @@ Module Barrett256.
     
     cbv [barrett_red256_alloc barrett_red256_fancy].
 
+    (*
     step start_context.
     { match goal with H : Fancy.CC.cc_m _ = _ |- _ => rewrite H end.
       match goal with |- context [Z.cc_m ?s ?x] =>
@@ -2566,6 +2570,7 @@ Module Barrett256.
       split; [Z.zero_bounds|].
       apply Z.lt_succ_r.
       apply Z.div_lt_upper_bound; try lia; admit. }
+      *)
 (*
     step start_context.
     { rewrite Z.rshi_correct by omega.
@@ -2677,49 +2682,10 @@ barrett_red256 =  fun var : type -> Type => λ x : var (type.type_primitive type
      : Expr (type.uncurry (type.type_primitive type.Z -> type.type_primitive type.Z -> type.type_primitive type.Z))
   *)
 
-  Import PreFancy.
-  Import PreFancy.Notations.
-  (*
-Local Notation "'RegMod'" := (Straightline.expr.Primitive (t:=type.Z) 115792089210356248762697446949407573530086143415290314195533631308867097853951).
-  Local Notation "'RegMuLow'" := (Straightline.expr.Primitive (t:=type.Z) 26959946667150639793205513449348445388433292963828203772348655992835).
-   *)
-  (*
-  Print barrett_red256_prefancy.
-*)
-  (*
-    selm@(y, $x₂, RegZero, RegMuLow);
-    rshi@(y0, RegZero, $x₂,255);
-    rshi@(y1, $x₂, $x₁,255);
-    mulhh@(y2, RegMuLow, $y1);
-    mulhl@(y3, RegMuLow, $y1);
-    mullh@(y4, RegMuLow, $y1);
-    mulll@(y5, RegMuLow, $y1);
-    add@(y6, $y5, $y4, 128);
-    addc@(y7, carry{$y6}, $y2, $y4, -128);
-    add@(y8, $y6, $y3, 128);
-    addc@(y9, carry{$y8}, $y7, $y3, -128);
-    add@(y10, $y1, $y9, 0);
-    addc@(y11, carry{$y10}, RegZero, $y0, 0); #128
-    add@(y12, $y, $y10, 0);
-    addc@(y13, carry{$y12}, RegZero, $y11, 0); #128
-    rshi@(y14, $y13, $y12,1);
-    mulhh@(y15, RegMod, $y14);
-    mullh@(y16, RegMod, $y14);
-    mulhl@(y17, RegMod, $y14);
-    mulll@(y18, RegMod, $y14);
-    add@(y19, $y18, $y17, 128);
-    addc@(y20, carry{$y19}, $y15, $y17, -128);
-    add@(y21, $y19, $y16, 128);
-    addc@(y22, carry{$y21}, $y20, $y16, -128);
-    sub@(y23, $x₁, $y21, 0);
-    subb@(y24, carry{$y23}, $x₂, $y22, 0);
-    sell@(y25, $y24, RegZero, RegMod);
-    sub@(y26, $y23, $y25, 0);
-    addm@(y27, $y26, RegZero, RegMod);
-    ret $y27
-  *)
 End Barrett256.
 
+(* TODO : once Barrett is updated & working, fix Montgomery to match *)
+(*
 Module Montgomery256.
 
   Definition N := Eval lazy in (2^256-2^224+2^192+2^96-1).
@@ -2733,15 +2699,6 @@ Module Montgomery256.
          As montred256_correct.
   Proof. Time solve_rmontred machine_wordsize. Time Qed.
 
-  (*
-  Definition montred256_prefancy' := PreFancy.of_Expr machine_wordsize [N;N'] montred256.
-
-  Derive montred256_prefancy
-         SuchThat (montred256_prefancy = montred256_prefancy' type.interp)
-         As montred256_prefancy_eq.
-  Proof. lazy - [type.interp]; reflexivity. Qed.
-*)
-
   Lemma montred'_correct_specialized R' (R'_correct : Z.equiv_modulo N (R * R') 1) :
     forall (lo hi : Z),
       0 <= lo < R -> 0 <= hi < R -> 0 <= lo + R * hi < R * N ->
@@ -3288,4 +3245,5 @@ Eval cbv beta iota delta [barrett_red256_alloc] in barrett_red256_alloc.
 Check prod_barrett_red256_correct.
 Print Assumptions prod_barrett_red256_correct.
 (* The equivalence with generated code is admitted as barrett_red256_alloc_equivalent. *)
+*)
 *)
\ No newline at end of file