Admit Common9_4Op.v

7 files changed, 21 insertions, 21 deletions

diff --git a/src/Specific/GF25519Reflective/Common9_4Op.v b/src/Specific/GF25519Reflective/Common9_4Op.v
index d2366932e..5754b8c54 100644
--- a/src/Specific/GF25519Reflective/Common9_4Op.v
+++ b/src/Specific/GF25519Reflective/Common9_4Op.v
@@ -103,6 +103,6 @@ Proof.
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
   specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8')
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
-  let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
+  Time let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
diff --git a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
index ddfe6c329..d8d55ca04 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
@@ -103,6 +103,6 @@ Proof.
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
   specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8')
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
-  let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
+  Time let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
diff --git a/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
index fa2debfad..1cedb55ac 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
@@ -103,6 +103,6 @@ Proof.
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
   specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8')
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
-  let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
+  Time let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
diff --git a/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
index 4a369cce6..c163fa18a 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
@@ -103,6 +103,6 @@ Proof.
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
   specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8')
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
-  let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
+  Time let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
diff --git a/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
index 33a02ceea..634ec3388 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
@@ -103,6 +103,6 @@ Proof.
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
   specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8')
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
-  let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
+  Time let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.128s) (successful) *)*)
diff --git a/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
index a7807eb7a..d7916c957 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
@@ -103,6 +103,6 @@ Proof.
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
   specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8')
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
-  let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
+  Time let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
diff --git a/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
index 31d8eba85..627b8849d 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
@@ -103,6 +103,6 @@ Proof.
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
   specialize (H1 (x0', x1', x2', x3', x4', x5', x6', x7', x8')
                  (conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
-  let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
-  t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
-Qed.
+  Time let args := constr:(op9_args_to_bounded (x0', x1', x2', x3', x4', x5', x6', x7', x8') Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
+       admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
+Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)