Some work on x86 and bounded repeated things

7 files changed, 344 insertions, 0 deletions

diff --git a/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v
index da0dced66..c2b87d5a4 100644
--- a/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v
+++ b/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v
@@ -147,6 +147,10 @@ End ripple_carry_adc.
 
 Hint Extern 2 (@is_add_with_carry _ (tuple ?W ?k) (@tuple_decoder ?n _ ?decode _) (@ripple_carry_adc _ ?adc _))
 => apply (@ripple_carry_is_add_with_carry n W decode adc k) : typeclass_instances.
+Hint Resolve (fun n W decode adc isdecode isadc
+              => @ripple_carry_is_add_with_carry n W decode adc 2 isdecode isadc
+                 : @is_add_with_carry (Z.of_nat 2 * n) (W * W) (@tuple_decoder n W decode 2) (@ripple_carry_adc W adc 2))
+  : typeclass_instances.
 
 Section ripple_carry_subc.
   Context {n W} {decode : decoder n W} (subc : sub_with_carry W).
@@ -187,3 +191,7 @@ End ripple_carry_subc.
 
 Hint Extern 2 (@is_sub_with_carry _ (tuple ?W ?k) (@tuple_decoder ?n _ ?decode _) (@ripple_carry_subc _ ?subc _))
 => apply (@ripple_carry_is_sub_with_carry n W decode subc k) : typeclass_instances.
+Hint Resolve (fun n W decode subc isdecode issubc
+              => @ripple_carry_is_sub_with_carry n W decode subc 2 isdecode issubc
+                 : @is_sub_with_carry (Z.of_nat 2 * n) (W * W) (@tuple_decoder n W decode 2) (@ripple_carry_subc W subc 2))
+  : typeclass_instances.
diff --git a/src/BoundedArithmetic/Double/Repeated/Core.v b/src/BoundedArithmetic/Double/Repeated/Core.v
new file mode 100644
index 000000000..e19b702aa
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Repeated/Core.v
@@ -0,0 +1,127 @@
+(*** Implementing Large Bounded Arithmetic via pairs *)
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.BoundedArithmetic.Double.Core.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.Notations.
+
+Local Open Scope nat_scope.
+Local Open Scope Z_scope.
+Local Open Scope type_scope.
+
+Local Coercion Z.of_nat : nat >-> Z.
+
+Fixpoint repeated_tuple W (base : nat) (exp : nat)
+  := match exp with
+     | O => W
+     | S exp' => tuple (repeated_tuple W base exp') base
+     end.
+
+Local Arguments Z.mul !_ !_.
+Local Opaque tuple_decoder.
+
+Section decode.
+  Context {n W}
+          {decode : decoder n W}
+          {base : nat}.
+
+  Fixpoint repeated_tuple_decoder {exp : nat}
+    : decoder (base^exp * n) (repeated_tuple W base exp)
+    := {| Interface.decode
+          := match exp return repeated_tuple W base exp -> Z with
+             | O => decode
+             | S exp' => Interface.decode : tuple (repeated_tuple W base exp') base -> Z
+             end |}.
+  Global Existing Instance repeated_tuple_decoder.
+End decode.
+
+Section all.
+  Context {n W}
+          {decode : decoder n W}
+          {ldi : load_immediate W}
+          {shrd : shift_right_doubleword_immediate W}
+          {sprl : spread_left_immediate W}
+          {shl : shift_left_immediate W}
+          {shr : shift_right_immediate W}
+          {mkl : mask_keep_low W}
+          {and : bitwise_and W}
+          {or : bitwise_or W}
+          {adc : add_with_carry W}
+          {subc : sub_with_carry W}
+          {mul : multiply W}
+          {mulhwll : multiply_low_low W}
+          {mulhwhl : multiply_high_low W}
+          {mulhwhh : multiply_high_high W}
+          {muldw : multiply_double W}
+          {selc : select_conditional W}
+          {addm : add_modulo W}.
+
+  Local Notation repeated_tuple_cls cls exp
+    := (match exp%nat as exp0 return cls (repeated_tuple W 2 exp0) with
+        | O => _ : cls W
+        | S exp' => _ : cls (tuple (repeated_tuple W 2 exp') 2)
+        end) (only parsing).
+
+  Fixpoint load_immediate_repeated_double {exp : nat}
+    := repeated_tuple_cls load_immediate exp.
+  Global Existing Instance load_immediate_repeated_double.
+  Fixpoint shift_right_doubleword_immediate_repeated_double {exp : nat}
+    := repeated_tuple_cls shift_right_doubleword_immediate exp.
+  Global Existing Instance shift_right_doubleword_immediate_repeated_double.
+  (*Fixpoint spread_left_immediate_repeated_double {exp : nat}
+    := repeated_tuple_cls spread_left_immediate exp.
+  Global Existing Instance spread_left_immediate_repeated_double.*)
+  Fixpoint bitwise_or_repeated_double {exp : nat}
+    := repeated_tuple_cls bitwise_or exp.
+  Global Existing Instance bitwise_or_repeated_double.
+  Local Hint Extern 1 =>
+  match goal with
+  | [ H : forall n, (_ * _)%type |- _ ]
+    => pose proof (fun n => fst (H n));
+         pose proof (fun n => snd (H n));
+         clear H
+  end : typeclass_instances.
+  Fixpoint shlr_repeated_double {exp : nat} : (shift_left_immediate (repeated_tuple W 2 exp) * shift_right_immediate (repeated_tuple W 2 exp))%type.
+  Proof.
+    refine (repeated_tuple_cls (fun T => shift_left_immediate T * shift_right_immediate T)%type exp);
+      split; exact _.
+  Defined.
+  Global Instance shift_left_immediate_repeated_double {exp : nat} : shift_left_immediate (repeated_tuple W 2 exp)
+    := fst (@shlr_repeated_double exp).
+  Global Instance shift_right_immediate_repeated_double {exp : nat} : shift_right_immediate (repeated_tuple W 2 exp)
+    := snd (@shlr_repeated_double exp).
+  (*Fixpoint mask_keep_low_repeated_double {exp : nat}
+    := repeated_tuple_cls mask_keep_low exp.
+  Global Existing Instance mask_keep_low_repeated_double.*)
+  Fixpoint bitwise_and_repeated_double {exp : nat}
+    := repeated_tuple_cls bitwise_and exp.
+  Global Existing Instance bitwise_and_repeated_double.
+  Fixpoint add_with_carry_repeated_double {exp : nat}
+    := repeated_tuple_cls add_with_carry exp.
+  Global Existing Instance add_with_carry_repeated_double.
+  Fixpoint sub_with_carry_repeated_double {exp : nat}
+    := repeated_tuple_cls sub_with_carry exp.
+  Global Existing Instance sub_with_carry_repeated_double.
+  (*Fixpoint multiply_repeated_double {exp : nat}
+    := repeated_tuple_cls multiply exp.
+  Global Existing Instance multiply_repeated_double.*)
+  Fixpoint multiply_double_repeated_double {exp : nat}
+    := repeated_tuple_cls multiply_double exp.
+  Global Existing Instance multiply_double_repeated_double.
+  Fixpoint multiply_low_low_repeated_double {exp : nat}
+    := repeated_tuple_cls multiply_low_low exp.
+  Global Existing Instance multiply_low_low_repeated_double.
+  Fixpoint multiply_high_low_repeated_double {exp : nat}
+    := repeated_tuple_cls multiply_high_low exp.
+  Global Existing Instance multiply_high_low_repeated_double.
+  Fixpoint multiply_high_high_repeated_double {exp : nat}
+    := repeated_tuple_cls multiply_high_high exp.
+  Global Existing Instance multiply_high_high_repeated_double.
+  Fixpoint select_conditional_repeated_double {exp : nat}
+    := repeated_tuple_cls select_conditional exp.
+  Global Existing Instance select_conditional_repeated_double.
+  (*Fixpoint add_modulo_repeated_double {exp : nat}
+    := repeated_tuple_cls add_modulo exp.
+  Global Existing Instance add_modulo_repeated_double.*)
+End all.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v b/src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v
new file mode 100644
index 000000000..7996dbca5
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v
@@ -0,0 +1,26 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.BoundedArithmetic.Double.Core.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.BitwiseOr.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
+Require Import Crypto.Util.ZUtil.
+
+Local Open Scope Z_scope.
+Local Arguments Z.mul !_ !_.
+Local Arguments Z.pow : simpl never.
+Local Arguments Z.of_nat : simpl never.
+Local Opaque tuple_decoder.
+
+Section bitwise_or.
+  Context {n W}
+          {decode : decoder n W}
+          {is_decode : is_decode decode}
+          {or : bitwise_or W}
+          {is_or : is_bitwise_or or}.
+
+  Fixpoint is_bitwise_or_repeated_double {exp : nat} : is_bitwise_or (bitwise_or_repeated_double (exp:=exp)).
+  Proof. is_cls_fixpoint_t decode n exp is_or (@is_bitwise_or_repeated_double). Qed.
+  Global Existing Instance is_bitwise_or_repeated_double.
+End bitwise_or.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v b/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
new file mode 100644
index 000000000..666d4593b
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
@@ -0,0 +1,93 @@
+Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.BoundedArithmetic.InterfaceProofs.
+Require Import Crypto.BoundedArithmetic.Double.Core.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
+Require Import Crypto.Util.ZUtil.
+
+Local Arguments Z.mul !_ !_.
+Local Opaque tuple_decoder.
+Local Coercion Z.of_nat : nat >-> Z.
+Local Open Scope Z_scope.
+
+Fixpoint project_repeated_tuple {W base exp} : repeated_tuple W base exp -> match base, exp with
+                                                                            | S _, _ => W
+                                                                            | O, O => W
+                                                                            | O, S _ => unit
+                                                                            end
+  := match exp, base
+           return repeated_tuple W base exp -> match base, exp with
+                                               | S _, _ => W
+                                               | O, O => W
+                                               | O, S _ => unit
+                                               end
+     with
+     | O, O
+     | O, S _
+       => fun x => x
+     | S exp', S O => @project_repeated_tuple W (S O) exp'
+     | S exp', S (S base') => fun x => @project_repeated_tuple W (S (S base')) exp' (snd x)
+     | S _, O => fun _ => tt
+     end.
+
+Lemma mul_1_l_decode {W} (P : forall n, decoder n W -> Prop)
+      {n} (decode : decoder n W)
+  : P n decode -> P (1 * n) {| Interface.decode := @Interface.decode n W decode |}.
+Proof.
+  pose proof (Z.mul_1_l n).
+  set (n' := 1 * n) in *; clearbody n'.
+  induction H.
+  destruct decode.
+  exact (fun x => x).
+Qed.
+
+Section decode.
+  Context {n W}
+          {decode : decoder n W}
+          {isdecode : is_decode decode}
+          {base : nat}.
+
+  Fixpoint is_repeated_tuple_decode {exp : nat}
+    : is_decode (@repeated_tuple_decoder n W decode base exp).
+  Proof.
+    refine match exp return is_decode (repeated_tuple_decoder (exp:=exp)) with
+           | O => fun x => _
+           | S exp' => fun x => _
+           end.
+    { clear is_repeated_tuple_decode.
+      simpl; rewrite Z.mul_1_l; apply isdecode. }
+    { specialize (is_repeated_tuple_decode exp').
+      change (base^S exp') with (base^(1 + exp')%nat) at 3.
+      rewrite (Nat2Z.inj_add 1 exp'), Z.pow_add_r, Z.pow_1_r by omega.
+      simpl.
+      destruct base as [|[| base' ]]; autorewrite with simpl_tuple_decoder.
+      { simpl; omega. }
+      { apply is_repeated_tuple_decode. }
+      { assert (0 <= n) by exact (decode_exponent_nonnegative _ (project_repeated_tuple x)).
+        assert (0 <= S (S base') ^ exp' * n) by zero_bounds.
+        assert (0 <= (S base' * (S (S base') ^ exp' * n))) by zero_bounds.
+        rewrite <- Z.mul_assoc.
+        change (2 ^ (S (S base') * (S (S base') ^ exp' * n)))
+        with (2 ^ (((1 + S base')%nat) * (S (S base') ^ exp' * n))).
+        rewrite (Nat2Z.inj_add 1 (S base')), Z.mul_add_distr_r, Z.mul_1_l, Z.pow_add_r by omega.
+        autorewrite with simpl_tuple_decoder Zshift_to_pow; generalize_decode; nia. } }
+  Qed.
+  Global Existing Instance is_repeated_tuple_decode.
+End decode.
+
+Ltac is_cls_fixpoint_t decode n exp is_clsv IH :=
+  let exp' := fresh exp in
+  destruct exp as [|exp'];
+  [ clear IH;
+    destruct decode; generalize is_clsv;
+    simpl;
+    change (Z.of_nat 2 ^ Z.of_nat 0) with 1;
+    generalize (Z.mul_1_l n); generalize (1 * n);
+    intro; clear; induction 1;
+    exact (fun x => x)
+  | specialize (IH exp');
+    simpl @repeated_tuple_decoder; simpl;
+    change (Z.of_nat (S exp')) with (Z.of_nat (1 + exp'));
+    rewrite (Nat2Z.inj_add 1 exp'), Z.pow_add_r, Z.pow_1_r, <- !Z.mul_assoc, <- decoder_eta by omega;
+    try exact _ ].
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v b/src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v
new file mode 100644
index 000000000..91b0c3ce7
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v
@@ -0,0 +1,26 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.BoundedArithmetic.Double.Core.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.LoadImmediate.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
+Require Import Crypto.Util.ZUtil.
+
+Local Open Scope Z_scope.
+Local Arguments Z.mul !_ !_.
+Local Arguments Z.pow : simpl never.
+Local Arguments Z.of_nat : simpl never.
+Local Opaque tuple_decoder.
+
+Section load_immediate.
+  Context {n W}
+          {decode : decoder n W}
+          {is_decode : is_decode decode}
+          {ldi : load_immediate W}
+          {is_ldi : is_load_immediate ldi}.
+
+  Fixpoint is_load_immediate_repeated_double {exp : nat} : is_load_immediate (load_immediate_repeated_double (exp:=exp)).
+  Proof. is_cls_fixpoint_t decode n exp is_ldi (@is_load_immediate_repeated_double). Qed.
+  Global Existing Instance is_load_immediate_repeated_double.
+End load_immediate.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v b/src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v
new file mode 100644
index 000000000..07bc65c84
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v
@@ -0,0 +1,38 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.BoundedArithmetic.Double.Core.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.RippleCarryAddSub.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
+Require Import Crypto.Util.ZUtil.
+
+Local Open Scope Z_scope.
+Local Arguments Z.mul !_ !_.
+Local Arguments Z.pow : simpl never.
+Local Arguments Z.of_nat : simpl never.
+Local Opaque tuple_decoder.
+
+Section add_with_carry.
+  Context {n W}
+          {decode : decoder n W}
+          {is_decode : is_decode decode}
+          {adc : add_with_carry W}
+          {is_adc : is_add_with_carry adc}.
+
+  Fixpoint is_add_with_carry_repeated_double {exp : nat} : is_add_with_carry (add_with_carry_repeated_double (exp:=exp)).
+  Proof. is_cls_fixpoint_t decode n exp is_adc (@is_add_with_carry_repeated_double). Qed.
+  Global Existing Instance is_add_with_carry_repeated_double.
+End add_with_carry.
+
+Section sub_with_carry.
+  Context {n W}
+          {decode : decoder n W}
+          {is_decode : is_decode decode}
+          {subc : sub_with_carry W}
+          {is_subc : is_sub_with_carry subc}.
+
+  Fixpoint is_sub_with_carry_repeated_double {exp : nat} : is_sub_with_carry (sub_with_carry_repeated_double (exp:=exp)).
+  Proof. is_cls_fixpoint_t decode n exp is_subc (@is_sub_with_carry_repeated_double). Qed.
+  Global Existing Instance is_sub_with_carry_repeated_double.
+End sub_with_carry.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v b/src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v
new file mode 100644
index 000000000..05ff40cd3
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v
@@ -0,0 +1,26 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.BoundedArithmetic.Double.Core.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.SelectConditional.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
+Require Import Crypto.Util.ZUtil.
+
+Local Open Scope Z_scope.
+Local Arguments Z.mul !_ !_.
+Local Arguments Z.pow : simpl never.
+Local Arguments Z.of_nat : simpl never.
+Local Opaque tuple_decoder.
+
+Section select_conditional.
+  Context {n W}
+          {decode : decoder n W}
+          {is_decode : is_decode decode}
+          {selc : select_conditional W}
+          {is_selc : is_select_conditional selc}.
+
+  Fixpoint is_select_conditional_repeated_double {exp : nat} : is_select_conditional (select_conditional_repeated_double (exp:=exp)).
+  Proof. is_cls_fixpoint_t decode n exp is_selc (@is_select_conditional_repeated_double). Qed.
+  Global Existing Instance is_select_conditional_repeated_double.
+End select_conditional.