aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--_CoqProject6
-rw-r--r--src/SpecificGen/GF2213_32Reflective/Common9_4Op.v108
-rw-r--r--src/SpecificGen/GF2519_32Reflective/Common9_4Op.v108
-rw-r--r--src/SpecificGen/GF25519_32Reflective/Common9_4Op.v108
-rw-r--r--src/SpecificGen/GF25519_64Reflective/Common9_4Op.v108
-rw-r--r--src/SpecificGen/GF41417_32Reflective/Common9_4Op.v108
-rw-r--r--src/SpecificGen/GF5211_32Reflective/Common9_4Op.v108
7 files changed, 654 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 1412edfdf..f1e41cd49 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -203,6 +203,7 @@ src/SpecificGen/GF5211_32BoundedCommon.v
src/SpecificGen/GF5211_32ExtendedAddCoordinates.v
src/SpecificGen/GF5211_32Reflective.v
src/SpecificGen/GF2213_32Reflective/Common.v
+src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
src/SpecificGen/GF2213_32Reflective/CommonBinOp.v
src/SpecificGen/GF2213_32Reflective/CommonUnOp.v
src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v
@@ -222,6 +223,7 @@ src/SpecificGen/GF2213_32Reflective/Reified/PreFreeze.v
src/SpecificGen/GF2213_32Reflective/Reified/Sub.v
src/SpecificGen/GF2213_32Reflective/Reified/Unpack.v
src/SpecificGen/GF2519_32Reflective/Common.v
+src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
src/SpecificGen/GF2519_32Reflective/CommonUnOp.v
src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v
@@ -241,6 +243,7 @@ src/SpecificGen/GF2519_32Reflective/Reified/PreFreeze.v
src/SpecificGen/GF2519_32Reflective/Reified/Sub.v
src/SpecificGen/GF2519_32Reflective/Reified/Unpack.v
src/SpecificGen/GF25519_32Reflective/Common.v
+src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
src/SpecificGen/GF25519_32Reflective/CommonBinOp.v
src/SpecificGen/GF25519_32Reflective/CommonUnOp.v
src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v
@@ -260,6 +263,7 @@ src/SpecificGen/GF25519_32Reflective/Reified/PreFreeze.v
src/SpecificGen/GF25519_32Reflective/Reified/Sub.v
src/SpecificGen/GF25519_32Reflective/Reified/Unpack.v
src/SpecificGen/GF25519_64Reflective/Common.v
+src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
src/SpecificGen/GF25519_64Reflective/CommonBinOp.v
src/SpecificGen/GF25519_64Reflective/CommonUnOp.v
src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v
@@ -279,6 +283,7 @@ src/SpecificGen/GF25519_64Reflective/Reified/PreFreeze.v
src/SpecificGen/GF25519_64Reflective/Reified/Sub.v
src/SpecificGen/GF25519_64Reflective/Reified/Unpack.v
src/SpecificGen/GF41417_32Reflective/Common.v
+src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
src/SpecificGen/GF41417_32Reflective/CommonBinOp.v
src/SpecificGen/GF41417_32Reflective/CommonUnOp.v
src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v
@@ -298,6 +303,7 @@ src/SpecificGen/GF41417_32Reflective/Reified/PreFreeze.v
src/SpecificGen/GF41417_32Reflective/Reified/Sub.v
src/SpecificGen/GF41417_32Reflective/Reified/Unpack.v
src/SpecificGen/GF5211_32Reflective/Common.v
+src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
src/SpecificGen/GF5211_32Reflective/CommonBinOp.v
src/SpecificGen/GF5211_32Reflective/CommonUnOp.v
src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v
diff --git a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
new file mode 100644
index 000000000..ddfe6c329
--- /dev/null
+++ b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
@@ -0,0 +1,108 @@
+Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr9_4Op_correct_and_bounded
+ ropW op (ropZ_sig : rexpr_9_4op_sig op)
+ (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+ (H0 : forall x012345678
+ (x012345678
+ := (eta_fe2213_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe2213_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe2213_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe2213_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe2213_32W (snd (fst (fst x012345678))),
+ eta_fe2213_32W (snd (fst x012345678)),
+ eta_fe2213_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe2213_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe2213_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+ (LiftOption.to' (Some args)))
+ with
+ | Some _ => True
+ | None => False
+ end)
+ (H1 : forall x012345678
+ (x012345678
+ := (eta_fe2213_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe2213_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe2213_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe2213_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe2213_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe2213_32W (snd (fst (fst x012345678))),
+ eta_fe2213_32W (snd (fst x012345678)),
+ eta_fe2213_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe2213_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe2213_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe2213_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+ with
+ | Some bounds => op9_4_bounds_good bounds = true
+ | None => False
+ end)
+ : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+ intros x0 x1 x2 x3 x4 x5 x6 x7 x8.
+ intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8.
+ pose x0 as x0'.
+ pose x1 as x1'.
+ pose x2 as x2'.
+ pose x3 as x3'.
+ pose x4 as x4'.
+ pose x5 as x5'.
+ pose x6 as x6'.
+ pose x7 as x7'.
+ pose x8 as x8'.
+ hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8; destruct_head' prod.
+ specialize (H0 (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))))))))).
+ 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.
diff --git a/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
new file mode 100644
index 000000000..fa2debfad
--- /dev/null
+++ b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
@@ -0,0 +1,108 @@
+Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr9_4Op_correct_and_bounded
+ ropW op (ropZ_sig : rexpr_9_4op_sig op)
+ (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+ (H0 : forall x012345678
+ (x012345678
+ := (eta_fe2519_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe2519_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe2519_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe2519_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe2519_32W (snd (fst (fst x012345678))),
+ eta_fe2519_32W (snd (fst x012345678)),
+ eta_fe2519_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe2519_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+ (LiftOption.to' (Some args)))
+ with
+ | Some _ => True
+ | None => False
+ end)
+ (H1 : forall x012345678
+ (x012345678
+ := (eta_fe2519_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe2519_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe2519_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe2519_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe2519_32W (snd (fst (fst x012345678))),
+ eta_fe2519_32W (snd (fst x012345678)),
+ eta_fe2519_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe2519_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe2519_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+ with
+ | Some bounds => op9_4_bounds_good bounds = true
+ | None => False
+ end)
+ : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+ intros x0 x1 x2 x3 x4 x5 x6 x7 x8.
+ intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8.
+ pose x0 as x0'.
+ pose x1 as x1'.
+ pose x2 as x2'.
+ pose x3 as x3'.
+ pose x4 as x4'.
+ pose x5 as x5'.
+ pose x6 as x6'.
+ pose x7 as x7'.
+ pose x8 as x8'.
+ hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8; destruct_head' prod.
+ specialize (H0 (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))))))))).
+ 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.
diff --git a/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
new file mode 100644
index 000000000..4a369cce6
--- /dev/null
+++ b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
@@ -0,0 +1,108 @@
+Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr9_4Op_correct_and_bounded
+ ropW op (ropZ_sig : rexpr_9_4op_sig op)
+ (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+ (H0 : forall x012345678
+ (x012345678
+ := (eta_fe25519_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe25519_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe25519_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe25519_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe25519_32W (snd (fst (fst x012345678))),
+ eta_fe25519_32W (snd (fst x012345678)),
+ eta_fe25519_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe25519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe25519_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+ (LiftOption.to' (Some args)))
+ with
+ | Some _ => True
+ | None => False
+ end)
+ (H1 : forall x012345678
+ (x012345678
+ := (eta_fe25519_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe25519_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe25519_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe25519_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe25519_32W (snd (fst (fst x012345678))),
+ eta_fe25519_32W (snd (fst x012345678)),
+ eta_fe25519_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe25519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe25519_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe25519_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+ with
+ | Some bounds => op9_4_bounds_good bounds = true
+ | None => False
+ end)
+ : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+ intros x0 x1 x2 x3 x4 x5 x6 x7 x8.
+ intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8.
+ pose x0 as x0'.
+ pose x1 as x1'.
+ pose x2 as x2'.
+ pose x3 as x3'.
+ pose x4 as x4'.
+ pose x5 as x5'.
+ pose x6 as x6'.
+ pose x7 as x7'.
+ pose x8 as x8'.
+ hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8; destruct_head' prod.
+ specialize (H0 (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))))))))).
+ 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.
diff --git a/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
new file mode 100644
index 000000000..33a02ceea
--- /dev/null
+++ b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
@@ -0,0 +1,108 @@
+Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
+Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations128.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr9_4Op_correct_and_bounded
+ ropW op (ropZ_sig : rexpr_9_4op_sig op)
+ (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+ (H0 : forall x012345678
+ (x012345678
+ := (eta_fe25519_64W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe25519_64W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe25519_64W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe25519_64W (snd (fst (fst (fst x012345678)))),
+ eta_fe25519_64W (snd (fst (fst x012345678))),
+ eta_fe25519_64W (snd (fst x012345678)),
+ eta_fe25519_64W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe25519_64WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe25519_64WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+ (LiftOption.to' (Some args)))
+ with
+ | Some _ => True
+ | None => False
+ end)
+ (H1 : forall x012345678
+ (x012345678
+ := (eta_fe25519_64W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe25519_64W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe25519_64W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe25519_64W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe25519_64W (snd (fst (fst (fst x012345678)))),
+ eta_fe25519_64W (snd (fst (fst x012345678))),
+ eta_fe25519_64W (snd (fst x012345678)),
+ eta_fe25519_64W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe25519_64WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe25519_64WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe25519_64WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+ with
+ | Some bounds => op9_4_bounds_good bounds = true
+ | None => False
+ end)
+ : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+ intros x0 x1 x2 x3 x4 x5 x6 x7 x8.
+ intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8.
+ pose x0 as x0'.
+ pose x1 as x1'.
+ pose x2 as x2'.
+ pose x3 as x3'.
+ pose x4 as x4'.
+ pose x5 as x5'.
+ pose x6 as x6'.
+ pose x7 as x7'.
+ pose x8 as x8'.
+ hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8; destruct_head' prod.
+ specialize (H0 (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))))))))).
+ 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.
diff --git a/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
new file mode 100644
index 000000000..a7807eb7a
--- /dev/null
+++ b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
@@ -0,0 +1,108 @@
+Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr9_4Op_correct_and_bounded
+ ropW op (ropZ_sig : rexpr_9_4op_sig op)
+ (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+ (H0 : forall x012345678
+ (x012345678
+ := (eta_fe41417_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe41417_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe41417_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe41417_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe41417_32W (snd (fst (fst x012345678))),
+ eta_fe41417_32W (snd (fst x012345678)),
+ eta_fe41417_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe41417_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe41417_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+ (LiftOption.to' (Some args)))
+ with
+ | Some _ => True
+ | None => False
+ end)
+ (H1 : forall x012345678
+ (x012345678
+ := (eta_fe41417_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe41417_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe41417_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe41417_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe41417_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe41417_32W (snd (fst (fst x012345678))),
+ eta_fe41417_32W (snd (fst x012345678)),
+ eta_fe41417_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe41417_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe41417_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe41417_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+ with
+ | Some bounds => op9_4_bounds_good bounds = true
+ | None => False
+ end)
+ : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+ intros x0 x1 x2 x3 x4 x5 x6 x7 x8.
+ intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8.
+ pose x0 as x0'.
+ pose x1 as x1'.
+ pose x2 as x2'.
+ pose x3 as x3'.
+ pose x4 as x4'.
+ pose x5 as x5'.
+ pose x6 as x6'.
+ pose x7 as x7'.
+ pose x8 as x8'.
+ hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8; destruct_head' prod.
+ specialize (H0 (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))))))))).
+ 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.
diff --git a/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
new file mode 100644
index 000000000..31d8eba85
--- /dev/null
+++ b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
@@ -0,0 +1,108 @@
+Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
+Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
+Require Import Crypto.Reflection.Z.Interpretations64.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Application.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Util.Tactics.
+
+Local Opaque Interp.
+Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
+Lemma Expr9_4Op_correct_and_bounded
+ ropW op (ropZ_sig : rexpr_9_4op_sig op)
+ (Hbounds : correct_and_bounded_genT ropW ropZ_sig)
+ (H0 : forall x012345678
+ (x012345678
+ := (eta_fe5211_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe5211_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe5211_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe5211_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe5211_32W (snd (fst (fst x012345678))),
+ eta_fe5211_32W (snd (fst x012345678)),
+ eta_fe5211_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe5211_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe5211_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+ (LiftOption.to' (Some args)))
+ with
+ | Some _ => True
+ | None => False
+ end)
+ (H1 : forall x012345678
+ (x012345678
+ := (eta_fe5211_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
+ eta_fe5211_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
+ eta_fe5211_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
+ eta_fe5211_32W (snd (fst (fst (fst (fst x012345678))))),
+ eta_fe5211_32W (snd (fst (fst (fst x012345678)))),
+ eta_fe5211_32W (snd (fst (fst x012345678))),
+ eta_fe5211_32W (snd (fst x012345678)),
+ eta_fe5211_32W (snd x012345678)))
+ (Hx012345678
+ : is_bounded (fe5211_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst (fst x012345678))))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst (fst x012345678)))) = true
+ /\ is_bounded (fe5211_32WToZ (snd (fst x012345678))) = true
+ /\ is_bounded (fe5211_32WToZ (snd x012345678)) = true),
+ let (Hx0, Hx12345678) := (eta_and Hx012345678) in
+ let (Hx1, Hx2345678) := (eta_and Hx12345678) in
+ let (Hx2, Hx345678) := (eta_and Hx2345678) in
+ let (Hx3, Hx45678) := (eta_and Hx345678) in
+ let (Hx4, Hx5678) := (eta_and Hx45678) in
+ let (Hx5, Hx678) := (eta_and Hx5678) in
+ let (Hx6, Hx78) := (eta_and Hx678) in
+ let (Hx7, Hx8) := (eta_and Hx78) in
+ let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
+ let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
+ match LiftOption.of'
+ (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+ with
+ | Some bounds => op9_4_bounds_good bounds = true
+ | None => False
+ end)
+ : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+Proof.
+ intros x0 x1 x2 x3 x4 x5 x6 x7 x8.
+ intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8.
+ pose x0 as x0'.
+ pose x1 as x1'.
+ pose x2 as x2'.
+ pose x3 as x3'.
+ pose x4 as x4'.
+ pose x5 as x5'.
+ pose x6 as x6'.
+ pose x7 as x7'.
+ pose x8 as x8'.
+ hnf in x0, x1, x2, x3, x4, x5, x6, x7, x8; destruct_head' prod.
+ specialize (H0 (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))))))))).
+ 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 10:14:34 +0000