Only use bool in freeze

This closes #186

7 files changed, 41 insertions, 30 deletions

diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v
index fd61fefb4..c2ce603f5 100644
--- a/src/Compilers/Z/Bounds/Pipeline.v
+++ b/src/Compilers/Z/Bounds/Pipeline.v
@@ -1,6 +1,10 @@
 (** * Reflective Pipeline *)
+Require Import Coq.Lists.List.
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.Glue.
 Require Import Crypto.Compilers.Z.Bounds.Pipeline.ReflectiveTactics.
+Import ListNotations.
+Local Open Scope nat_scope.
+Local Open Scope list_scope.
 (** This file combines the various PHOAS modules in tactics,
     culminating in a tactic [refine_reflectively], which solves a goal of the form
 <<
@@ -19,16 +23,23 @@ Ltac refine_reflectively_gen allowable_bit_widths opts :=
   refine_to_reflective_glue allowable_bit_widths;
   do_reflective_pipeline opts.
 
-Ltac refine_reflectively128_with opts := refine_reflectively_gen (1::128::256::nil)%nat%list opts.
-Ltac refine_reflectively64_with opts := refine_reflectively_gen (1::64::128::nil)%nat%list opts.
-Ltac refine_reflectively32_with opts := refine_reflectively_gen (1::32::64::nil)%nat%list opts.
+Ltac refine_reflectively128_with opts := refine_reflectively_gen [128; 256] opts.
+Ltac refine_reflectively64_with opts := refine_reflectively_gen [64; 128] opts.
+Ltac refine_reflectively32_with opts := refine_reflectively_gen [32; 64] opts.
+Ltac refine_reflectively128_with_bool_with opts := refine_reflectively_gen [1; 128; 256] opts.
+Ltac refine_reflectively64_with_bool_with opts := refine_reflectively_gen [1; 64; 128] opts.
+Ltac refine_reflectively32_with_bool_with opts := refine_reflectively_gen [1; 32; 64] opts.
 Ltac refine_reflectively128 := refine_reflectively128_with default_PipelineOptions.
 Ltac refine_reflectively64 := refine_reflectively64_with default_PipelineOptions.
 Ltac refine_reflectively32 := refine_reflectively32_with default_PipelineOptions.
+Ltac refine_reflectively128_with_bool := refine_reflectively128_with_bool_with default_PipelineOptions.
+Ltac refine_reflectively64_with_bool := refine_reflectively64_with_bool_with default_PipelineOptions.
+Ltac refine_reflectively32_with_bool := refine_reflectively32_with_bool_with default_PipelineOptions.
 
 (** Convenience notations for options *)
 Definition anf := {| Pipeline.Definition.anf := true |}.
 
 (** The default *)
+Ltac refine_reflectively_with_bool_with opts := refine_reflectively64_with_bool_with opts.
 Ltac refine_reflectively_with opts := refine_reflectively64_with opts.
 Ltac refine_reflectively := refine_reflectively_with default_PipelineOptions.
diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v
index 74731f6c6..63cc76fc2 100644
--- a/src/Specific/IntegrationTestFreeze.v
+++ b/src/Specific/IntegrationTestFreeze.v
@@ -71,7 +71,7 @@ Section BoundedField25p5.
     apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
     (* jgross start here! *)
     (*Set Ltac Profiling.*)
-    Time refine_reflectively_with anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *)
+    Time refine_reflectively_with_bool_with anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *)
     (*Show Ltac Profile.*)
     (* total time:      5.680s
 
diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log
index c08157343..95f2237c0 100644
--- a/src/Specific/IntegrationTestLadderstep130Display.log
+++ b/src/Specific/IntegrationTestLadderstep130Display.log
@@ -23,7 +23,7 @@ let (a, b) := Interp-η
  uint128_t x51 = x50 >> 0x55;
  uint128_t x52 = x50 & 0x1fffffffffffffffffffffL;
  uint128_t x53 = x51 + x46;
- bool x54 = (bool) (x53 >> 0x55);
+ uint128_t x54 = x53 >> 0x55;
  uint128_t x55 = x53 & 0x1fffffffffffffffffffffL;
  uint128_t x56 = x54 + x49;
  uint256_t x57 = (uint256_t) x38 * x36 + ((uint256_t) x37 * x37 + (uint256_t) x36 * x38);
@@ -41,7 +41,7 @@ let (a, b) := Interp-η
  uint128_t x69 = x68 >> 0x55;
  uint128_t x70 = x68 & 0x1fffffffffffffffffffffL;
  uint128_t x71 = x69 + x64;
- bool x72 = (bool) (x71 >> 0x55);
+ uint128_t x72 = x71 >> 0x55;
  uint128_t x73 = x71 & 0x1fffffffffffffffffffffL;
  uint128_t x74 = x72 + x67;
  uint256_t x75 = (uint256_t) x52 * x74 + ((uint256_t) x55 * x73 + (uint256_t) x56 * x70);
@@ -59,7 +59,7 @@ let (a, b) := Interp-η
  uint128_t x87 = x86 >> 0x55;
  uint128_t x88 = x86 & 0x1fffffffffffffffffffffL;
  uint128_t x89 = x87 + x82;
- bool x90 = (bool) (x89 >> 0x55);
+ uint128_t x90 = x89 >> 0x55;
  uint128_t x91 = x89 & 0x1fffffffffffffffffffffL;
  uint128_t x92 = x90 + x85;
  uint128_t x93 = 0x3ffffffffffffffffffffeL + x56 - x74;
@@ -77,10 +77,10 @@ let (a, b) := Interp-η
  uint128_t x105 = x104 >> 0x55;
  uint128_t x106 = x104 & 0x1fffffffffffffffffffffL;
  uint128_t x107 = x100 + 0x5 * x105;
- bool x108 = (bool) (x107 >> 0x55);
+ uint128_t x108 = x107 >> 0x55;
  uint128_t x109 = x107 & 0x1fffffffffffffffffffffL;
  uint128_t x110 = x108 + x103;
- bool x111 = (bool) (x110 >> 0x55);
+ uint128_t x111 = x110 >> 0x55;
  uint128_t x112 = x110 & 0x1fffffffffffffffffffffL;
  uint128_t x113 = x111 + x106;
  uint128_t x114 = x56 + x113;
@@ -101,7 +101,7 @@ let (a, b) := Interp-η
  uint128_t x129 = x128 >> 0x55;
  uint128_t x130 = x128 & 0x1fffffffffffffffffffffL;
  uint128_t x131 = x129 + x124;
- bool x132 = (bool) (x131 >> 0x55);
+ uint128_t x132 = x131 >> 0x55;
  uint128_t x133 = x131 & 0x1fffffffffffffffffffffL;
  uint128_t x134 = x132 + x127;
  uint128_t x135 = x27 + x31;
@@ -125,7 +125,7 @@ let (a, b) := Interp-η
  uint128_t x153 = x152 >> 0x55;
  uint128_t x154 = x152 & 0x1fffffffffffffffffffffL;
  uint128_t x155 = x153 + x148;
- bool x156 = (bool) (x155 >> 0x55);
+ uint128_t x156 = x155 >> 0x55;
  uint128_t x157 = x155 & 0x1fffffffffffffffffffffL;
  uint128_t x158 = x156 + x151;
  uint256_t x159 = (uint256_t) x140 * x33 + ((uint256_t) x139 * x34 + (uint256_t) x138 * x35);
@@ -143,7 +143,7 @@ let (a, b) := Interp-η
  uint128_t x171 = x170 >> 0x55;
  uint128_t x172 = x170 & 0x1fffffffffffffffffffffL;
  uint128_t x173 = x171 + x166;
- bool x174 = (bool) (x173 >> 0x55);
+ uint128_t x174 = x173 >> 0x55;
  uint128_t x175 = x173 & 0x1fffffffffffffffffffffL;
  uint128_t x176 = x174 + x169;
  uint128_t x177 = x176 + x158;
@@ -167,7 +167,7 @@ let (a, b) := Interp-η
  uint128_t x195 = x194 >> 0x55;
  uint128_t x196 = x194 & 0x1fffffffffffffffffffffL;
  uint128_t x197 = x195 + x190;
- bool x198 = (bool) (x197 >> 0x55);
+ uint128_t x198 = x197 >> 0x55;
  uint128_t x199 = x197 & 0x1fffffffffffffffffffffL;
  uint128_t x200 = x198 + x193;
  uint128_t x201 = 0x3ffffffffffffffffffffeL + x176 - x158;
@@ -191,7 +191,7 @@ let (a, b) := Interp-η
  uint128_t x219 = x218 >> 0x55;
  uint128_t x220 = x218 & 0x1fffffffffffffffffffffL;
  uint128_t x221 = x219 + x214;
- bool x222 = (bool) (x221 >> 0x55);
+ uint128_t x222 = x221 >> 0x55;
  uint128_t x223 = x221 & 0x1fffffffffffffffffffffL;
  uint128_t x224 = x222 + x217;
  uint256_t x225 = (uint256_t) x10 * x224 + ((uint256_t) x12 * x223 + (uint256_t) x11 * x220);
@@ -209,7 +209,7 @@ let (a, b) := Interp-η
  uint128_t x237 = x236 >> 0x55;
  uint128_t x238 = x236 & 0x1fffffffffffffffffffffL;
  uint128_t x239 = x237 + x232;
- bool x240 = (bool) (x239 >> 0x55);
+ uint128_t x240 = x239 >> 0x55;
  uint128_t x241 = x239 & 0x1fffffffffffffffffffffL;
  uint128_t x242 = x240 + x235;
  return (Return x92, Return x91, Return x88, (Return x134, Return x133, Return x130), (Return x200, Return x199, Return x196, (Return x242, Return x241, Return x238))))
diff --git a/src/Specific/IntegrationTestLadderstepDisplay.log b/src/Specific/IntegrationTestLadderstepDisplay.log
index 8f4998081..73c47fa40 100644
--- a/src/Specific/IntegrationTestLadderstepDisplay.log
+++ b/src/Specific/IntegrationTestLadderstepDisplay.log
@@ -53,7 +53,7 @@ let (a, b) := Interp-η
  uint64_t x101 = x100 >> 0x33;
  uint64_t x102 = x100 & 0x7ffffffffffff;
  uint64_t x103 = x101 + x90;
- bool x104 = (bool) (x103 >> 0x33);
+ uint64_t x104 = x103 >> 0x33;
  uint64_t x105 = x103 & 0x7ffffffffffff;
  uint64_t x106 = x104 + x93;
  uint128_t x107 = (uint128_t) x57 * x72;
@@ -87,7 +87,7 @@ let (a, b) := Interp-η
  uint64_t x135 = x134 >> 0x33;
  uint64_t x136 = x134 & 0x7ffffffffffff;
  uint64_t x137 = x135 + x124;
- bool x138 = (bool) (x137 >> 0x33);
+ uint64_t x138 = x137 >> 0x33;
  uint64_t x139 = x137 & 0x7ffffffffffff;
  uint64_t x140 = x138 + x127;
  uint64_t x141 = x99 + x133;
@@ -128,7 +128,7 @@ let (a, b) := Interp-η
  uint64_t x176 = x175 >> 0x33;
  uint64_t x177 = x175 & 0x7ffffffffffff;
  uint64_t x178 = x176 + x165;
- bool x179 = (bool) (x178 >> 0x33);
+ uint64_t x179 = x178 >> 0x33;
  uint64_t x180 = x178 & 0x7ffffffffffff;
  uint64_t x181 = x179 + x168;
  uint64_t x182 = x150 * 0x2;
@@ -159,7 +159,7 @@ let (a, b) := Interp-η
  uint64_t x207 = x206 >> 0x33;
  uint64_t x208 = x206 & 0x7ffffffffffff;
  uint64_t x209 = x207 + x196;
- bool x210 = (bool) (x209 >> 0x33);
+ uint64_t x210 = x209 >> 0x33;
  uint64_t x211 = x209 & 0x7ffffffffffff;
  uint64_t x212 = x210 + x199;
  uint128_t x213 = (uint128_t) x208 * x10;
@@ -193,7 +193,7 @@ let (a, b) := Interp-η
  uint64_t x241 = x240 >> 0x33;
  uint64_t x242 = x240 & 0x7ffffffffffff;
  uint64_t x243 = x241 + x230;
- bool x244 = (bool) (x243 >> 0x33);
+ uint64_t x244 = x243 >> 0x33;
  uint64_t x245 = x243 & 0x7ffffffffffff;
  uint64_t x246 = x244 + x233;
  uint64_t x247 = x57 * 0x2;
@@ -224,7 +224,7 @@ let (a, b) := Interp-η
  uint64_t x272 = x271 >> 0x33;
  uint64_t x273 = x271 & 0x7ffffffffffff;
  uint64_t x274 = x272 + x261;
- bool x275 = (bool) (x274 >> 0x33);
+ uint64_t x275 = x274 >> 0x33;
  uint64_t x276 = x274 & 0x7ffffffffffff;
  uint64_t x277 = x275 + x264;
  uint64_t x278 = x62 * 0x2;
@@ -255,7 +255,7 @@ let (a, b) := Interp-η
  uint64_t x303 = x302 >> 0x33;
  uint64_t x304 = x302 & 0x7ffffffffffff;
  uint64_t x305 = x303 + x292;
- bool x306 = (bool) (x305 >> 0x33);
+ uint64_t x306 = x305 >> 0x33;
  uint64_t x307 = x305 & 0x7ffffffffffff;
  uint64_t x308 = x306 + x295;
  uint128_t x309 = (uint128_t) x273 * x304;
@@ -289,7 +289,7 @@ let (a, b) := Interp-η
  uint64_t x337 = x336 >> 0x33;
  uint64_t x338 = x336 & 0x7ffffffffffff;
  uint64_t x339 = x337 + x326;
- bool x340 = (bool) (x339 >> 0x33);
+ uint64_t x340 = x339 >> 0x33;
  uint64_t x341 = x339 & 0x7ffffffffffff;
  uint64_t x342 = x340 + x329;
  uint64_t x343 = 0xffffffffffffe + x270 - x301;
@@ -317,10 +317,10 @@ let (a, b) := Interp-η
  uint64_t x365 = (uint64_t) (x364 >> 0x33);
  uint64_t x366 = (uint64_t) x364 & 0x7ffffffffffff;
  uint64_t x367 = x354 + 0x13 * x365;
- bool x368 = (bool) (x367 >> 0x33);
+ uint64_t x368 = x367 >> 0x33;
  uint64_t x369 = x367 & 0x7ffffffffffff;
  uint64_t x370 = x368 + x357;
- bool x371 = (bool) (x370 >> 0x33);
+ uint64_t x371 = x370 >> 0x33;
  uint64_t x372 = x370 & 0x7ffffffffffff;
  uint64_t x373 = x371 + x360;
  uint64_t x374 = x366 + x270;
@@ -359,7 +359,7 @@ let (a, b) := Interp-η
  uint64_t x407 = x406 >> 0x33;
  uint64_t x408 = x406 & 0x7ffffffffffff;
  uint64_t x409 = x407 + x396;
- bool x410 = (bool) (x409 >> 0x33);
+ uint64_t x410 = x409 >> 0x33;
  uint64_t x411 = x409 & 0x7ffffffffffff;
  uint64_t x412 = x410 + x399;
  return (Return x335, Return x332, Return x342, Return x341, Return x338, (Return x405, Return x402, Return x412, Return x411, Return x408), (Return x174, Return x171, Return x181, Return x180, Return x177, (Return x239, Return x236, Return x246, Return x245, Return x242))))
diff --git a/src/Specific/IntegrationTestMulDisplay.log b/src/Specific/IntegrationTestMulDisplay.log
index fadf37f9d..e49d7c117 100644
--- a/src/Specific/IntegrationTestMulDisplay.log
+++ b/src/Specific/IntegrationTestMulDisplay.log
@@ -33,7 +33,7 @@ Interp-η
  uint64_t x48 = x47 >> 0x33;
  uint64_t x49 = x47 & 0x7ffffffffffff;
  uint64_t x50 = x48 + x37;
- bool x51 = (bool) (x50 >> 0x33);
+ uint64_t x51 = x50 >> 0x33;
  uint64_t x52 = x50 & 0x7ffffffffffff;
  return (Return x46, Return x43, x51 + x40, Return x52, Return x49))
 (x, x0)%core
diff --git a/src/Specific/IntegrationTestSquareDisplay.log b/src/Specific/IntegrationTestSquareDisplay.log
index b2e5092fc..006b83cd9 100644
--- a/src/Specific/IntegrationTestSquareDisplay.log
+++ b/src/Specific/IntegrationTestSquareDisplay.log
@@ -30,7 +30,7 @@ Interp-η
  uint64_t x34 = x33 >> 0x33;
  uint64_t x35 = x33 & 0x7ffffffffffff;
  uint64_t x36 = x34 + x23;
- bool x37 = (bool) (x36 >> 0x33);
+ uint64_t x37 = x36 >> 0x33;
  uint64_t x38 = x36 & 0x7ffffffffffff;
  return (Return x32, Return x29, x37 + x26, Return x38, Return x35))
 x
diff --git a/src/Specific/IntegrationTestSubDisplay.log b/src/Specific/IntegrationTestSubDisplay.log
index 1d8934686..ae675b0e7 100644
--- a/src/Specific/IntegrationTestSubDisplay.log
+++ b/src/Specific/IntegrationTestSubDisplay.log
@@ -22,10 +22,10 @@ Interp-η
  uint64_t x37 = x36 >> 0x33;
  uint64_t x38 = x36 & 0x7ffffffffffff;
  uint64_t x39 = x26 + 0x13 * x37;
- bool x40 = (bool) (x39 >> 0x33);
+ uint64_t x40 = x39 >> 0x33;
  uint64_t x41 = x39 & 0x7ffffffffffff;
  uint64_t x42 = x40 + x29;
- bool x43 = (bool) (x42 >> 0x33);
+ uint64_t x43 = x42 >> 0x33;
  uint64_t x44 = x42 & 0x7ffffffffffff;
  return (Return x38, Return x35, x43 + x32, Return x44, Return x41))
 (x, x0)%core