refactor of Basesystem and ModularBaseSystem; includes general code organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division

1 files changed, 490 insertions, 0 deletions

diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v
new file mode 100644
index 000000000..84374fe8f
--- /dev/null
+++ b/src/BaseSystemProofs.v
@@ -0,0 +1,490 @@
+Require Import List.
+Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
+Require Import ZArith.ZArith ZArith.Zdiv.
+Require Import Omega NPeano Arith.
+Require Import Crypto.BaseSystem.
+Local Open Scope Z.
+
+Local Infix ".+" := add (at level 50).
+
+Local Hint Extern 1 (@eq Z _ _) => ring.
+
+Section BaseSystemProofs.
+  Context `(base_vector : BaseVector).
+
+  Lemma decode'_truncate : forall bs us, decode' bs us = decode' bs (firstn (length bs) us).
+  Proof.
+    unfold decode'; intros; f_equal; apply combine_truncate_l.
+  Qed.
+
+  Lemma add_rep : forall bs us vs, decode' bs (add us vs) = decode' bs us + decode' bs vs.
+  Proof.
+    unfold decode', accumulate; induction bs; destruct us, vs; boring; ring.
+  Qed.
+
+  Lemma decode_nil : forall bs, decode' bs nil = 0.
+    auto.
+  Qed.
+  Hint Rewrite decode_nil.
+
+  Lemma decode_base_nil : forall us, decode' nil us = 0.
+  Proof.
+    intros; rewrite decode'_truncate; auto.
+  Qed.
+  Hint Rewrite decode_base_nil.
+
+  Lemma mul_each_rep : forall bs u vs,
+    decode' bs (mul_each u vs) = u * decode' bs vs.
+  Proof.
+    unfold decode', accumulate; induction bs; destruct vs; boring; ring.
+  Qed.
+
+  Lemma base_eq_1cons: base = 1 :: skipn 1 base.
+  Proof.
+    pose proof (b0_1 0) as H.
+    destruct base; compute in H; try discriminate; boring.
+  Qed.
+
+  Lemma decode'_cons : forall x1 x2 xs1 xs2,
+    decode' (x1 :: xs1) (x2 :: xs2) = x1 * x2 + decode' xs1 xs2.
+  Proof.
+    unfold decode', accumulate; boring; ring.
+  Qed.
+  Hint Rewrite decode'_cons.
+
+  Lemma decode_cons : forall x us,
+    decode base (x :: us) = x + decode base (0 :: us).
+  Proof.
+    unfold decode; intros.
+    rewrite base_eq_1cons.
+    autorewrite with core; ring_simplify; auto.
+  Qed.
+
+  Lemma sub_rep : forall bs us vs, decode' bs (sub us vs) = decode' bs us - decode' bs vs.
+  Proof.
+    induction bs; destruct us; destruct vs; boring; ring.
+  Qed.
+
+  Lemma encode_rep : forall z, decode base (encode z) = z.
+  Proof.
+    pose proof base_eq_1cons.
+    unfold decode, encode; destruct z; boring.
+  Qed.
+
+  Lemma mul_each_base : forall us bs c, 
+      decode' bs (mul_each c us) = decode' (mul_each c bs) us.
+  Proof.
+    induction us; destruct bs; boring; ring.
+  Qed.
+
+  Hint Rewrite (@nth_default_nil Z).
+  Hint Rewrite (@firstn_nil Z).
+  Hint Rewrite (@skipn_nil Z).
+
+  Lemma base_app : forall us low high,
+      decode' (low ++ high) us = decode' low (firstn (length low) us) + decode' high (skipn (length low) us).
+  Proof.
+    induction us; destruct low; boring.
+  Qed.
+
+  Lemma base_mul_app : forall low c us, 
+      decode' (low ++ mul_each c low) us = decode' low (firstn (length low) us) + 
+      c * decode' low (skipn (length low) us).
+  Proof.
+    intros.
+    rewrite base_app; f_equal.
+    rewrite <- mul_each_rep.
+    rewrite mul_each_base.
+    reflexivity.
+  Qed.
+
+  Lemma zeros_rep : forall bs n, decode' bs (zeros n) = 0.
+    induction bs; destruct n; boring.
+  Qed.
+  Lemma length_zeros : forall n, length (zeros n) = n.
+    induction n; boring.
+  Qed.
+  Hint Rewrite length_zeros.
+
+  Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m).
+  Proof.
+    induction n; boring.
+  Qed.
+  Hint Rewrite app_zeros_zeros.
+
+  Lemma zeros_app0 : forall m, zeros m ++ 0 :: nil = zeros (S m).
+  Proof.
+    induction m; boring.
+  Qed.
+  Hint Rewrite zeros_app0.
+
+  Lemma rev_zeros : forall n, rev (zeros n) = zeros n.
+  Proof.
+    induction n; boring.
+  Qed.
+  Hint Rewrite rev_zeros.
+
+  Hint Unfold nth_default.
+
+  Lemma decode_single : forall n bs x,
+    decode' bs (zeros n ++ x :: nil) = nth_default 0 bs n * x.
+  Proof.
+    induction n; destruct bs; boring.
+  Qed.
+  Hint Rewrite decode_single.
+
+  Lemma peel_decode : forall xs ys x y, decode' (x::xs) (y::ys) = x*y + decode' xs ys.
+  Proof.
+    boring.
+  Qed.
+  Hint Rewrite zeros_rep peel_decode.
+
+  Lemma decode_highzeros : forall xs bs n, decode' bs (xs ++ zeros n) = decode' bs xs.
+  Proof.
+    induction xs; destruct bs; boring.
+  Qed.
+
+  Lemma mul_bi'_zeros : forall n m, mul_bi' base n (zeros m) = zeros m.
+    induction m; boring.
+  Qed.
+  Hint Rewrite mul_bi'_zeros.
+
+  Lemma nth_error_base_nonzero : forall n x,
+    nth_error base n = Some x -> x <> 0.
+  Proof.
+    eauto using (@nth_error_value_In Z), Zgt0_neq0, base_positive.
+  Qed.
+
+  Hint Rewrite plus_0_r.
+
+  Lemma mul_bi_single : forall m n x,
+    (n + m < length base)%nat ->
+    decode base (mul_bi base n (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n.
+  Proof.
+    unfold mul_bi, decode.
+    destruct m; simpl; simpl_list; simpl; intros. {
+      pose proof nth_error_base_nonzero as nth_nonzero.
+      case_eq base; [intros; boring | intros z l base_eq].
+      specialize (b0_1 0); intro b0_1'.
+      rewrite base_eq in *.
+      rewrite nth_default_cons in b0_1'.
+      rewrite b0_1' in *.
+      unfold crosscoef.
+      autounfold; autorewrite with core.
+      unfold nth_default.
+      nth_tac.
+      rewrite Z.mul_1_r.
+      rewrite Z_div_same_full.
+      destruct x; ring.
+      eapply nth_nonzero; eauto.
+    } {
+      ssimpl_list.
+      autorewrite with core.
+      rewrite app_assoc.
+      autorewrite with core.
+      unfold crosscoef; simpl; ring_simplify.
+      rewrite Nat.add_1_r.
+      rewrite base_good by auto.
+      rewrite Z_div_mult by (apply base_positive; rewrite nth_default_eq; apply nth_In; auto).
+      rewrite <- Z.mul_assoc.
+      rewrite <- Z.mul_comm.
+      rewrite <- Z.mul_assoc.
+      rewrite <- Z.mul_assoc.
+      destruct (Z.eq_dec x 0); subst; try ring.
+      rewrite Z.mul_cancel_l by auto.
+      rewrite <- base_good by auto.
+      ring.
+      }
+  Qed.
+
+  Lemma set_higher' : forall vs x, vs++x::nil = vs .+ (zeros (length vs) ++ x :: nil).
+    induction vs; boring; f_equal; ring.
+  Qed.
+
+  Lemma set_higher : forall bs vs x,
+    decode' bs (vs++x::nil) = decode' bs vs + nth_default 0 bs (length vs) * x.
+  Proof.
+    intros.
+    rewrite set_higher'.
+    rewrite add_rep.
+    f_equal.
+    apply decode_single.
+  Qed.
+
+  Lemma zeros_plus_zeros : forall n, zeros n = zeros n .+ zeros n.
+    induction n; auto.
+    simpl; f_equal; auto. 
+  Qed.
+
+  Lemma mul_bi'_n_nil : forall n, mul_bi' base n nil = nil.
+  Proof.
+    unfold mul_bi; auto.
+  Qed.
+  Hint Rewrite mul_bi'_n_nil.
+
+  Lemma add_nil_l : forall us, nil .+ us = us.
+    induction us; auto.
+  Qed.
+  Hint Rewrite add_nil_l.
+
+  Lemma add_nil_r : forall us, us .+ nil = us.
+    induction us; auto.
+  Qed.
+  Hint Rewrite add_nil_r.
+  
+  Lemma add_first_terms : forall us vs a b,
+    (a :: us) .+ (b :: vs) = (a + b) :: (us .+ vs).
+    auto.
+  Qed.
+  Hint Rewrite add_first_terms.
+ 
+  Lemma mul_bi'_cons : forall n x us,
+    mul_bi' base n (x :: us) = x * crosscoef base n (length us) :: mul_bi' base n us.
+  Proof.
+    unfold mul_bi'; auto.
+  Qed.
+
+  Lemma add_same_length : forall us vs l, (length us = l) -> (length vs = l) ->
+    length (us .+ vs) = l.
+  Proof.
+    induction us, vs; boring.
+    erewrite (IHus vs (pred l)); boring.
+  Qed.
+
+  Hint Rewrite app_nil_l.
+  Hint Rewrite app_nil_r.
+
+  Lemma add_snoc_same_length : forall l us vs a b, 
+    (length us = l) -> (length vs = l) ->
+    (us ++ a :: nil) .+ (vs ++ b :: nil) = (us .+ vs) ++ (a + b) :: nil.
+  Proof.
+    induction l, us, vs; boring; discriminate.
+  Qed.
+
+  Lemma mul_bi'_add : forall us n vs l
+    (Hlus: length us = l)
+    (Hlvs: length vs = l),
+    mul_bi' base n (rev (us .+ vs)) = 
+    mul_bi' base n (rev us) .+ mul_bi' base n (rev vs).
+  Proof.
+    (* TODO(adamc): please help prettify this *)
+    induction us using rev_ind;
+      try solve [destruct vs; boring; congruence].
+    destruct vs using rev_ind; boring; clear IHvs; simpl_list.
+    erewrite (add_snoc_same_length (pred l) us vs _ _); simpl_list.
+    repeat rewrite mul_bi'_cons; rewrite add_first_terms; simpl_list.
+    rewrite (IHus n vs (pred l)).
+    replace (length us) with (pred l).
+    replace (length vs) with (pred l).
+    rewrite (add_same_length us vs (pred l)).
+    f_equal; ring.
+
+    erewrite length_snoc; eauto.
+    erewrite length_snoc; eauto.
+    erewrite length_snoc; eauto.
+    erewrite length_snoc; eauto.
+    erewrite length_snoc; eauto.
+    erewrite length_snoc; eauto.
+    erewrite length_snoc; eauto.
+    erewrite length_snoc; eauto.
+   Qed.
+
+  Lemma zeros_cons0 : forall n, 0 :: zeros n = zeros (S n).
+    auto.
+  Qed.
+
+  Lemma add_leading_zeros : forall n us vs,
+    (zeros n ++ us) .+ (zeros n ++ vs) = zeros n ++ (us .+ vs).
+  Proof.
+    induction n; boring.
+  Qed.
+  
+  Lemma rev_add_rev : forall us vs l, (length us = l) -> (length vs = l) ->
+    (rev us) .+ (rev vs) = rev (us .+ vs).
+  Proof.
+    induction us, vs; boring; try solve [subst; discriminate].
+    rewrite (add_snoc_same_length (pred l) _ _ _ _) by (subst; simpl_list; omega).
+    rewrite (IHus vs (pred l)) by omega; auto.
+  Qed.
+  Hint Rewrite rev_add_rev.
+
+  Lemma mul_bi'_length : forall us n, length (mul_bi' base n us) = length us.
+  Proof.
+    induction us, n; boring.
+  Qed.
+  Hint Rewrite mul_bi'_length.
+
+  Lemma add_comm : forall us vs, us .+ vs = vs .+ us.
+  Proof.
+    induction us, vs; boring; f_equal; auto.
+  Qed.
+
+  Hint Rewrite rev_length.
+
+  Lemma mul_bi_add_same_length : forall n us vs l,
+    (length us = l) -> (length vs = l) ->
+    mul_bi base n (us .+ vs) = mul_bi base n us .+ mul_bi base n vs.
+  Proof.
+    unfold mul_bi; boring.
+    rewrite add_leading_zeros.
+    erewrite mul_bi'_add; boring.
+    erewrite rev_add_rev; boring.
+  Qed.
+
+  Lemma add_zeros_same_length : forall us, us .+ (zeros (length us)) = us.
+  Proof.
+    induction us; boring; f_equal; omega.
+  Qed.
+
+  Hint Rewrite add_zeros_same_length.
+  Hint Rewrite minus_diag.
+
+  Lemma add_trailing_zeros : forall us vs, (length us >= length vs)%nat ->
+    us .+ vs = us .+ (vs ++ (zeros (length us - length vs))).
+  Proof.
+    induction us, vs; boring; f_equal; boring.
+  Qed.
+
+  Lemma length_add_ge : forall us vs, (length us >= length vs)%nat ->
+    (length (us .+ vs) <= length us)%nat.
+  Proof.
+    intros.
+    rewrite add_trailing_zeros by trivial.
+    erewrite add_same_length by (pose proof app_length; boring); omega.
+  Qed.
+
+  Lemma add_length_le_max : forall us vs,
+      (length (us .+ vs) <= max (length us) (length vs))%nat.
+  Proof.
+    intros; case_max; (rewrite add_comm; apply length_add_ge; omega) ||
+                                        (apply length_add_ge; omega) .
+  Qed.
+
+  Lemma sub_nil_length: forall us : digits, length (sub nil us) = length us.
+  Proof.
+     induction us; boring.
+  Qed.
+
+  Lemma sub_length_le_max : forall us vs,
+      (length (sub us vs) <= max (length us) (length vs))%nat.
+  Proof.
+    induction us, vs; boring.
+    rewrite sub_nil_length; auto.
+  Qed.
+
+  Lemma mul_bi_length : forall us n, length (mul_bi base n us) = (length us + n)%nat.
+  Proof.
+    pose proof mul_bi'_length; unfold mul_bi.
+    destruct us; repeat progress (simpl_list; boring).
+  Qed.
+  Hint Rewrite mul_bi_length.
+
+  Lemma mul_bi_trailing_zeros : forall m n us,
+    mul_bi base n us ++ zeros m = mul_bi base n (us ++ zeros m).
+  Proof.
+    unfold mul_bi.
+    induction m; intros; try solve [boring].
+    rewrite <- zeros_app0.
+    rewrite app_assoc.
+    repeat progress (boring; rewrite rev_app_distr).
+  Qed.
+
+  Lemma mul_bi_add_longer : forall n us vs,
+    (length us >= length vs)%nat ->
+    mul_bi base n (us .+ vs) = mul_bi base n us .+ mul_bi base n vs.
+  Proof.
+    boring.
+    rewrite add_trailing_zeros by auto.
+    rewrite (add_trailing_zeros (mul_bi base n us) (mul_bi base n vs))
+      by (repeat (rewrite mul_bi_length); omega).
+    erewrite mul_bi_add_same_length by
+      (eauto; simpl_list; rewrite length_zeros; omega).
+    rewrite mul_bi_trailing_zeros.
+    repeat (f_equal; boring).
+  Qed.
+
+  Lemma mul_bi_add : forall n us vs,
+    mul_bi base n (us .+ vs) = (mul_bi base n  us) .+ (mul_bi base n vs).
+  Proof.
+    intros; pose proof mul_bi_add_longer.
+    destruct (le_ge_dec (length us) (length vs)). {
+      rewrite add_comm.
+      rewrite (add_comm (mul_bi base n us)).
+      boring.
+    } {
+      boring.
+    }
+  Qed.
+
+  Lemma mul_bi_rep : forall i vs,
+    (i + length vs < length base)%nat ->
+    decode base (mul_bi base i vs) = decode base vs * nth_default 0 base i.
+  Proof.
+    unfold decode.
+    induction vs using rev_ind; intros; try solve [unfold mul_bi; boring].
+    assert (i + length vs < length base)%nat by
+      (rewrite app_length in *; boring).
+
+    rewrite set_higher.
+    ring_simplify.
+    rewrite <- IHvs by auto; clear IHvs.
+    rewrite <- mul_bi_single by auto.
+    rewrite <- add_rep.
+    rewrite <- mul_bi_add.
+    rewrite set_higher'.
+    auto.
+  Qed.
+
+  (* mul' is multiplication with the FIRST ARGUMENT REVERSED *)
+  Fixpoint mul' (usr vs:digits) : digits :=
+    match usr with
+      | u::usr' => 
+        mul_each u (mul_bi base (length usr') vs) .+ mul' usr' vs
+      | _ => nil
+    end.
+  Definition mul us := mul' (rev us).
+
+  Lemma mul'_rep : forall us vs,
+    (length us + length vs <= length base)%nat ->
+    decode base (mul' (rev us) vs) = decode base us * decode base vs.
+  Proof.
+    unfold decode.
+    induction us using rev_ind; boring.
+
+    assert (length us + length vs < length base)%nat by
+      (rewrite app_length in *; boring).
+
+    ssimpl_list.
+    rewrite add_rep.
+    boring.
+    rewrite set_higher.
+    rewrite mul_each_rep.
+    rewrite mul_bi_rep by auto.
+    unfold decode; ring.
+  Qed.
+
+  Lemma mul_rep : forall us vs,
+    (length us + length vs <= length base)%nat ->
+    decode base (mul us vs) = decode base us * decode base vs.
+  Proof.
+    exact mul'_rep.
+  Qed.
+
+  Lemma mul'_length: forall us vs,
+      (length (mul' us vs) <= length us + length vs)%nat.
+  Proof.
+    pose proof add_length_le_max.
+    induction us; boring.
+    unfold mul_each.
+    simpl_list; case_max; boring; omega.
+  Qed.
+
+  Lemma mul_length: forall us vs,
+      (length (mul us vs) <= length us + length vs)%nat.
+  Proof.
+    intros; unfold mul.
+    rewrite mul'_length.
+    rewrite rev_length; omega.
+  Qed.
+
+End BaseSystemProofs.