Add SubWithGetBorrow to reflective machinery

After     | File Name                                                    | Before    || Change
-------------------------------------------------------------------------------------------------
12m37.09s | Total                                                        | 12m23.52s || +0m13.56s
-------------------------------------------------------------------------------------------------
0m12.09s  | Compilers/Z/Syntax/Equality                                  | 0m06.70s  || +0m05.38s
0m56.82s  | Compilers/Z/Named/RewriteAddToAdcInterp                      | 0m54.12s  || +0m02.70s
2m20.25s  | Specific/IntegrationTestLadderstep                           | 2m18.79s  || +0m01.46s
0m13.83s  | Compilers/Z/ArithmeticSimplifierInterp                       | 0m12.56s  || +0m01.26s
1m38.90s  | Spec/Test/X25519                                             | 1m38.46s  || +0m00.43s
0m53.83s  | Specific/IntegrationTestLadderstep130                        | 0m53.93s  || -0m00.10s
0m48.70s  | Compilers/Z/ArithmeticSimplifierWf                           | 0m49.10s  || -0m00.39s
0m39.72s  | Spec/Ed25519                                                 | 0m39.65s  || +0m00.07s
0m22.19s  | Primitives/EdDSARepChange                                    | 0m22.08s  || +0m00.11s
0m19.69s  | Compilers/Named/MapCastWf                                    | 0m19.63s  || +0m00.06s
0m15.09s  | Specific/IntegrationTestFreeze                               | 0m15.28s  || -0m00.18s
0m11.78s  | Specific/IntegrationTestMul                                  | 0m11.61s  || +0m00.16s
0m10.54s  | Specific/IntegrationTestSub                                  | 0m10.48s  || +0m00.05s
0m10.46s  | Specific/ArithmeticSynthesisTest                             | 0m10.47s  || -0m00.00s
0m09.30s  | Util/ZUtil                                                   | 0m09.21s  || +0m00.08s
0m09.15s  | Compilers/Named/MapCastInterp                                | 0m09.19s  || -0m00.03s
0m09.14s  | Specific/IntegrationTestSquare                               | 0m09.28s  || -0m00.13s
0m08.82s  | Arithmetic/MontgomeryReduction/Proofs                        | 0m08.78s  || +0m00.04s
0m08.46s  | LegacyArithmetic/ArchitectureToZLikeProofs                   | 0m08.38s  || +0m00.08s
0m08.23s  | LegacyArithmetic/Double/Proofs/Multiply                      | 0m08.16s  || +0m00.07s
0m07.80s  | Arithmetic/Core                                              | 0m07.71s  || +0m00.08s
0m07.70s  | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m07.78s  || -0m00.08s
0m06.72s  | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate           | 0m06.79s  || -0m00.07s
0m06.37s  | Util/FixedWordSizesEquality                                  | 0m06.33s  || +0m00.04s
0m06.06s  | Arithmetic/Saturated                                         | 0m05.84s  || +0m00.21s
0m05.43s  | LegacyArithmetic/Double/Proofs/RippleCarryAddSub             | 0m05.38s  || +0m00.04s
0m05.41s  | LegacyArithmetic/Pow2BaseProofs                              | 0m05.31s  || +0m00.10s
0m05.05s  | Specific/ArithmeticSynthesisTest130                          | 0m05.09s  || -0m00.04s
0m04.98s  | Compilers/Z/Bounds/InterpretationLemmas/PullCast             | 0m04.80s  || +0m00.18s
0m03.94s  | Arithmetic/BarrettReduction/HAC                              | 0m03.84s  || +0m00.10s
0m03.79s  | Util/ForLoop/Unrolling                                       | 0m03.80s  || -0m00.00s
0m03.45s  | LegacyArithmetic/InterfaceProofs                             | 0m03.40s  || +0m00.05s
0m03.23s  | Arithmetic/BarrettReduction/Generalized                      | 0m03.07s  || +0m00.16s
0m03.02s  | Specific/FancyMachine256/Montgomery                          | 0m03.20s  || -0m00.18s
0m03.00s  | Compilers/Z/RewriteAddToAdcInterp                            | 0m02.94s  || +0m00.06s
0m02.98s  | Arithmetic/ModularArithmeticTheorems                         | 0m03.02s  || -0m00.04s
0m02.94s  | LegacyArithmetic/ZBoundedZ                                   | 0m02.88s  || +0m00.06s
0m02.82s  | Specific/FancyMachine256/Barrett                             | 0m02.82s  || +0m00.00s
0m02.64s  | LegacyArithmetic/Double/Proofs/ShiftLeft                     | 0m02.54s  || +0m00.10s
0m02.63s  | LegacyArithmetic/Double/Proofs/Decode                        | 0m02.53s  || +0m00.10s
0m02.62s  | LegacyArithmetic/Double/Proofs/ShiftRight                    | 0m02.72s  || -0m00.10s
0m02.56s  | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy          | 0m02.25s  || +0m00.31s
0m02.34s  | Compilers/Z/Bounds/Relax                                     | 0m02.40s  || -0m00.06s
0m02.26s  | LegacyArithmetic/BarretReduction                             | 0m02.25s  || +0m00.00s
0m02.21s  | Compilers/Z/Bounds/Pipeline/Definition                       | 0m02.13s  || +0m00.08s
0m02.10s  | Util/WordUtil                                                | 0m02.07s  || +0m00.03s
0m02.00s  | Util/ForLoop/InvariantFramework                              | 0m01.98s  || +0m00.02s
0m01.86s  | Specific/FancyMachine256/Core                                | 0m01.82s  || +0m00.04s
0m01.82s  | Util/ZUtil/AddGetCarry                                       | 0m01.61s  || +0m00.20s
0m01.60s  | Arithmetic/PrimeFieldTheorems                                | 0m01.45s  || +0m00.15s
0m01.56s  | Arithmetic/BarrettReduction/Wikipedia                        | 0m01.50s  || +0m00.06s
0m01.55s  | LegacyArithmetic/MontgomeryReduction                         | 0m01.53s  || +0m00.02s
0m01.25s  | Util/NumTheoryUtil                                           | 0m00.96s  || +0m00.29s
0m01.03s  | Compilers/Z/RewriteAddToAdcWf                                | 0m01.02s  || +0m00.01s
0m00.99s  | Arithmetic/Karatsuba                                         | 0m00.81s  || +0m00.17s
0m00.98s  | LegacyArithmetic/Double/Proofs/BitwiseOr                     | 0m00.99s  || -0m00.01s
0m00.98s  | Util/ZUtil/Pow2Mod                                           | 0m00.97s  || +0m00.01s
0m00.90s  | LegacyArithmetic/Double/Proofs/LoadImmediate                 | 0m00.95s  || -0m00.04s
0m00.80s  | LegacyArithmetic/BaseSystemProofs                            | 0m00.88s  || -0m00.07s
0m00.80s  | Util/ZUtil/Testbit                                           | 0m00.74s  || +0m00.06s
0m00.79s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics                | 0m00.65s  || +0m00.14s
0m00.76s  | Compilers/Z/CNotations                                       | 0m00.78s  || -0m00.02s
0m00.76s  | Util/ZUtil/Stabilization                                     | 0m00.64s  || +0m00.12s
0m00.68s  | Util/IterAssocOp                                             | 0m00.69s  || -0m00.00s
0m00.66s  | Compilers/Z/Syntax/Util                                      | 0m00.66s  || +0m00.00s
0m00.66s  | Compilers/MapCastByDeBruijnInterp                            | 0m00.78s  || -0m00.12s
0m00.64s  | Compilers/Z/CommonSubexpressionElimination                   | 0m00.58s  || +0m00.06s
0m00.63s  | LegacyArithmetic/Interface                                   | 0m00.56s  || +0m00.06s
0m00.62s  | Compilers/Z/Bounds/Pipeline                                  | 0m00.53s  || +0m00.08s
0m00.62s  | Arithmetic/MontgomeryReduction/WordByWord/Definition         | 0m00.67s  || -0m00.05s
0m00.62s  | LegacyArithmetic/Double/Proofs/SelectConditional             | 0m00.58s  || +0m00.04s
0m00.55s  | Compilers/MapCastByDeBruijnWf                                | 0m00.62s  || -0m00.06s
0m00.52s  | Compilers/Z/Reify                                            | 0m00.56s  || -0m00.04s
0m00.52s  | Compilers/Z/JavaNotations                                    | 0m00.50s  || +0m00.02s
0m00.52s  | LegacyArithmetic/ZBounded                                    | 0m00.54s  || -0m00.02s
0m00.51s  | Compilers/Z/Bounds/RoundUpLemmas                             | 0m00.44s  || +0m00.07s
0m00.51s  | Compilers/Z/Bounds/Pipeline/Glue                             | 0m00.47s  || +0m00.04s
0m00.50s  | Compilers/Z/Syntax                                           | 0m00.44s  || +0m00.06s
0m00.50s  | Compilers/Z/ArithmeticSimplifier                             | 0m00.47s  || +0m00.03s
0m00.50s  | LegacyArithmetic/Double/Core                                 | 0m00.53s  || -0m00.03s
0m00.49s  | Compilers/Z/Bounds/MapCastByDeBruijnInterp                   | 0m00.48s  || +0m00.01s
0m00.48s  | Arithmetic/ModularArithmeticPre                              | 0m00.47s  || +0m00.01s
0m00.47s  | Util/NUtil                                                   | 0m00.51s  || -0m00.04s
0m00.47s  | Compilers/Z/Bounds/MapCastByDeBruijnWf                       | 0m00.40s  || +0m00.06s
0m00.47s  | Spec/EdDSA                                                   | 0m00.51s  || -0m00.04s
0m00.46s  | Compilers/Z/Bounds/InterpretationLemmas/Tactics              | 0m00.48s  || -0m00.01s
0m00.46s  | Compilers/Z/Named/RewriteAddToAdc                            | 0m00.49s  || -0m00.02s
0m00.45s  | Spec/ModularArithmetic                                       | 0m00.45s  || +0m00.00s
0m00.45s  | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic          | 0m00.54s  || -0m00.09s
0m00.44s  | Arithmetic/MontgomeryReduction/Definition                    | 0m00.45s  || -0m00.01s
0m00.44s  | Util/ForLoop/Tests                                           | 0m00.43s  || +0m00.01s
0m00.44s  | Compilers/Z/MapCastByDeBruijn                                | 0m00.49s  || -0m00.04s
0m00.44s  | LegacyArithmetic/ArchitectureToZLike                         | 0m00.44s  || +0m00.00s
0m00.43s  | LegacyArithmetic/BaseSystem                                  | 0m00.41s  || +0m00.02s
0m00.43s  | Compilers/Z/InlineInterp                                     | 0m00.36s  || +0m00.07s
0m00.43s  | Compilers/Z/MapCastByDeBruijnWf                              | 0m00.40s  || +0m00.02s
0m00.42s  | LegacyArithmetic/Pow2Base                                    | 0m00.48s  || -0m00.06s
0m00.42s  | Compilers/Z/CommonSubexpressionEliminationWf                 | 0m00.40s  || +0m00.01s
0m00.42s  | Compilers/Z/Bounds/Interpretation                            | 0m00.46s  || -0m00.04s
0m00.42s  | Specific/IntegrationTestDisplayCommon                        | 0m00.36s  || +0m00.06s
0m00.42s  | Compilers/Z/RewriteAddToAdc                                  | 0m00.41s  || +0m00.01s
0m00.42s  | Util/ZUtil/Morphisms                                         | 0m00.38s  || +0m00.03s
0m00.42s  | Compilers/Z/InlineWf                                         | 0m00.44s  || -0m00.02s
0m00.41s  | Compilers/Z/CommonSubexpressionEliminationInterp             | 0m00.39s  || +0m00.01s
0m00.41s  | Compilers/Z/HexNotationConstants                             | 0m00.38s  || +0m00.02s
0m00.40s  | Compilers/Z/Bounds/MapCastByDeBruijn                         | 0m00.36s  || +0m00.04s
0m00.39s  | Compilers/Z/Named/DeadCodeElimination                        | 0m00.36s  || +0m00.03s
0m00.38s  | Compilers/Z/Named/DeadCodeEliminationInterp                  | 0m00.40s  || -0m00.02s
0m00.37s  | Compilers/Z/MapCastByDeBruijnInterp                          | 0m00.40s  || -0m00.03s
0m00.36s  | Compilers/Z/OpInversion                                      | 0m00.36s  || +0m00.00s
0m00.36s  | Compilers/Z/FoldTypes                                        | 0m00.36s  || +0m00.00s
0m00.35s  | Compilers/Z/Bounds/Pipeline/OutputType                       | 0m00.33s  || +0m00.01s
0m00.34s  | Compilers/Z/BinaryNotationConstants                          | 0m00.36s  || -0m00.01s
0m00.34s  | Compilers/Z/Inline                                           | 0m00.41s  || -0m00.06s
0m00.34s  | Compilers/Z/ArithmeticSimplifierUtil                         | 0m00.35s  || -0m00.00s
0m00.31s  | Util/ZUtil/Tactics/Ztestbit                                  | 0m00.30s  || +0m00.01s
0m00.31s  | Util/ZUtil/Tactics                                           | 0m00.30s  || +0m00.01s
0m00.30s  | Util/ZUtil/Definitions                                       | 0m00.27s  || +0m00.02s
0m00.30s  | Util/ZUtil/Zselect                                           | 0m00.30s  || +0m00.00s

1 files changed, 10 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 4a5d3a0ab..6fc969dfd 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -18,6 +18,16 @@ Module Z.
   Definition add_get_carry (bitwidth : Z) (x y : Z) : Z * Z
     := add_with_get_carry bitwidth 0 x y.
 
+  Definition get_borrow (bitwidth : Z) (v : Z) : Z * Z
+    := let '(v, c) := get_carry bitwidth v in
+       (v, -c).
+  Definition sub_with_borrow (c : Z) (x y : Z) : Z
+    := add_with_carry (-c) x (-y).
+  Definition sub_with_get_borrow (bitwidth : Z) (c : Z) (x y : Z) : Z * Z
+    := get_borrow bitwidth (sub_with_borrow c x y).
+  Definition sub_get_borrow (bitwidth : Z) (x y : Z) : Z * Z
+    := sub_with_get_borrow bitwidth 0 x y.
+
   (* splits at [bound], not [2^bitwidth]; wrapper to make add_getcarry
   work if input is not known to be a power of 2 *)
   Definition add_get_carry_full (bound : Z) (x y : Z) : Z * Z