diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-08-04 00:31:26 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-08-04 20:00:53 -0400 |
| commit | 016035f962de0666786e84b03cfc20e02b227011 (patch) | |
| tree | 64c4b8b89efe519edc7888afd73c0961e858895a /src/Experiments/NewPipeline/Toplevel2.v | |
| parent | 4871dfda627597bcee92fc94edf2e37cdfd0ef49 (diff) | |
Finish AbsInt Wf proofs
After | File Name | Before || Change | % Change
-----------------------------------------------------------------------------------------------------
12m43.49s | Total | 11m54.85s || +0m48.63s | +6.80%
-----------------------------------------------------------------------------------------------------
0m44.25s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m00.49s || +0m43.75s | +8930.61%
4m31.51s | Experiments/NewPipeline/Toplevel1 | 4m29.26s || +0m02.25s | +0.83%
5m50.40s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m48.62s || +0m01.77s | +0.51%
1m33.52s | Experiments/NewPipeline/Toplevel2 | 1m32.77s || +0m00.75s | +0.80%
0m01.38s | Experiments/NewPipeline/CLI | 0m01.34s || +0m00.03s | +2.98%
0m01.22s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.13s || +0m00.09s | +7.96%
0m01.21s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.24s || -0m00.03s | -2.41%
Diffstat (limited to 'src/Experiments/NewPipeline/Toplevel2.v')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel2.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index 83afb62fb..54d6cbac8 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -2464,7 +2464,7 @@ Module Barrett256. Proof. intros. rewrite <-barrett_reduce_correct_specialized by assumption. - destruct (barrett_red256_correct (xLow, (xHigh, tt)) (xLow, (xHigh, tt))) as [H1 H2]. + destruct (proj1 barrett_red256_correct (xLow, (xHigh, tt)) (xLow, (xHigh, tt))) as [H1 H2]. { repeat split. } { cbn -[Z.pow]. rewrite !andb_true_iff. @@ -2931,7 +2931,7 @@ Module Montgomery256. Proof. intros. rewrite <-montred'_correct_specialized by assumption. - destruct (montred256_correct ((lo, hi), tt) ((lo, hi), tt)) as [H2 H3]. + destruct (proj1 montred256_correct ((lo, hi), tt) ((lo, hi), tt)) as [H2 H3]. { repeat split. } { cbn -[Z.pow]. rewrite !andb_true_iff. |