Add testbit_add_shiftl_full

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
5m41.93s | Total                                           | 5m42.43s || -0m00.50s
----------------------------------------------------------------------------------
1m34.78s | Test/Curve25519SpecTestVectors                  | 1m34.04s || +0m00.74s
0m34.74s | ModularArithmetic/Conversion                    | 0m35.23s || -0m00.48s
0m27.39s | ModularArithmetic/ModularBaseSystemProofs       | 0m27.12s || +0m00.26s
0m21.67s | ModularArithmetic/Pow2BaseProofs                | 0m21.30s || +0m00.37s
0m20.51s | BoundedArithmetic/DoubleBoundedProofs           | 0m20.75s || -0m00.23s
0m19.42s | EdDSARepChange                                  | 0m19.76s || -0m00.33s
0m14.36s | Specific/GF25519                                | 0m14.30s || +0m00.05s
0m12.32s | Util/ZUtil                                      | 0m12.23s || +0m00.08s
0m09.36s | Testbit                                         | 0m09.15s || +0m00.20s
0m08.41s | ModularArithmetic/Montgomery/ZProofs            | 0m08.39s || +0m00.01s
0m08.35s | BoundedArithmetic/ArchitectureToZLikeProofs     | 0m08.48s || -0m00.13s
0m08.05s | Encoding/PointEncoding                          | 0m08.02s || +0m00.03s
0m07.51s | Specific/GF1305                                 | 0m07.54s || -0m00.03s
0m03.86s | BaseSystemProofs                                | 0m03.84s || +0m00.02s
0m03.57s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m03.69s || -0m00.12s
0m03.46s | ModularArithmetic/ModularBaseSystemListProofs   | 0m03.47s || -0m00.01s
0m03.44s | ModularArithmetic/Tutorial                      | 0m03.59s || -0m00.14s
0m03.26s | BoundedArithmetic/InterfaceProofs               | 0m03.16s || +0m00.09s
0m02.87s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.87s || +0m00.00s
0m02.80s | Encoding/PointEncodingPre                       | 0m02.94s || -0m00.14s
0m02.53s | ModularArithmetic/ModularArithmeticTheorems     | 0m02.58s || -0m00.05s
0m02.25s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.28s || -0m00.02s
0m02.24s | ModularArithmetic/BarrettReduction/ZBounded     | 0m02.29s || -0m00.04s
0m02.07s | Specific/FancyMachine256/Montgomery             | 0m02.22s || -0m00.15s
0m02.02s | Specific/FancyMachine256/Barrett                | 0m02.16s || -0m00.14s
0m01.83s | ModularArithmetic/Montgomery/ZBounded           | 0m01.74s || +0m00.09s
0m01.66s | Specific/FancyMachine256/Core                   | 0m01.73s || -0m00.07s
0m01.48s | ModularArithmetic/BarrettReduction/Z            | 0m01.40s || +0m00.08s
0m01.28s | BaseSystem                                      | 0m01.20s || +0m00.08s
0m01.27s | ModularArithmetic/PrimeFieldTheorems            | 0m01.56s || -0m00.29s
0m01.16s | ModularArithmetic/ExtendedBaseVector            | 0m01.19s || -0m00.03s
0m00.95s | Util/NumTheoryUtil                              | 0m00.91s || +0m00.03s
0m00.87s | Experiments/EncodingLemmas                      | 0m00.96s || -0m00.08s
0m00.70s | ModularArithmetic/ModularBaseSystem             | 0m00.62s || +0m00.07s
0m00.67s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.66s || +0m00.01s
0m00.65s | BoundedArithmetic/Interface                     | 0m00.64s || +0m00.01s
0m00.64s | Encoding/ModularWordEncodingPre                 | 0m00.62s || +0m00.02s
0m00.64s | Spec/EdDSA                                      | 0m00.70s || -0m00.05s
0m00.61s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.60s || +0m00.01s
0m00.61s | Encoding/ModularWordEncodingTheorems            | 0m00.63s || -0m00.02s
0m00.56s | Spec/ModularWordEncoding                        | 0m00.56s || +0m00.00s
0m00.56s | ModularArithmetic/ModularBaseSystemList         | 0m00.62s || -0m00.05s
0m00.52s | BoundedArithmetic/DoubleBounded                 | 0m00.43s || +0m00.09s
0m00.52s | ModularArithmetic/ZBounded                      | 0m00.58s || -0m00.05s
0m00.51s | BoundedArithmetic/ArchitectureToZLike           | 0m00.45s || +0m00.06s
0m00.50s | Spec/Ed25519                                    | 0m00.56s || -0m00.06s
0m00.47s | BoundedArithmetic/StripCF                       | 0m00.46s || +0m00.00s
0m00.45s | ModularArithmetic/Pre                           | 0m00.67s || -0m00.22s
0m00.43s | ModularArithmetic/Pow2Base                      | 0m00.44s || -0m00.01s
0m00.42s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.36s || +0m00.06s
0m00.39s | ModularArithmetic/Montgomery/Z                  | 0m00.38s || +0m00.01s
0m00.34s | Spec/ModularArithmetic                          | 0m00.36s || -0m00.01s

1 files changed, 11 insertions, 0 deletions

diff --git a/src/BoundedArithmetic/DoubleBounded.v b/src/BoundedArithmetic/DoubleBounded.v
index d11adb153..aa87e756e 100644
--- a/src/BoundedArithmetic/DoubleBounded.v
+++ b/src/BoundedArithmetic/DoubleBounded.v
@@ -84,6 +84,17 @@ Section tuple2.
       := { ldi := load_immediate_double }.
   End load_immediate.
 
+  Section bitwise_or.
+    Context {W}
+            {or : bitwise_or W}.
+
+    Definition bitwise_or_double (x : tuple W 2) (y : tuple W 2) : tuple W 2
+      := (or (fst x) (fst y), or (snd x) (snd y)).
+
+    Global Instance or_double : bitwise_or (tuple W 2)
+      := { or := bitwise_or_double }.
+  End bitwise_or.
+
   Section spread_left.
     Context (n : Z) {W}
             {ldi : load_immediate W}