diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-08-26 16:31:33 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-08-26 16:31:33 -0700 |
| commit | 7f918337e0ea4c05276ad2825873e9363fcf50e6 (patch) | |
| tree | 919b3d8a5a98dfdade9ec25f53313ba882893d61 /src/Experiments | |
| parent | 70f3ef7025b327adb798e5e9dc0e4c346e10d0fb (diff) | |
Merge into rsloan-phoas
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/SpecificCurve25519.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Experiments/SpecificCurve25519.v b/src/Experiments/SpecificCurve25519.v index 4e523e661..b5878825f 100644 --- a/src/Experiments/SpecificCurve25519.v +++ b/src/Experiments/SpecificCurve25519.v @@ -131,7 +131,7 @@ Module Input. Proof. reflexivity. Qed. Example interp_example_range : - RangeInterp (ZToRange 32 example_Expr) = Some (range N 28%N 32%N). + RangeInterp (ZToRange 32 example_Expr) = Some (range N 28%N 28%N). Proof. reflexivity. Qed. (* Reification assumes the argument type is Z *) @@ -505,10 +505,10 @@ Definition KeepAddingOne (n : nat) : Expr (T := Z) TT := Definition testCase := Eval vm_compute in KeepAddingOne 5. -Eval vm_compute in RangeInterp (ZToRange 32 testCase). +Eval vm_compute in RangeInterp (ZToRange 8 testCase). (* This example wasn't starting with a term at the right abstraction level. - * We don't need to handle tuples in bounds checking. + * We don't need to handle tuples in bounds checking. *) Section Curve25519. Local Infix ">>" := Z.shiftr. Local Infix "&" := (fun x y => Z.land x (Z.of_nat (Z.to_nat y))). |