BaseSystem encode function is no longer naive; it does a mod/div loop rather than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.

1 files changed, 11 insertions, 2 deletions

diff --git a/src/BaseSystem.v b/src/BaseSystem.v
index 1985520f0..a37932de0 100644
--- a/src/BaseSystem.v
+++ b/src/BaseSystem.v
@@ -34,8 +34,17 @@ Section BaseSystem.
   Definition accumulate p acc := fst p * snd p + acc.
   Definition decode' bs u  := fold_right accumulate 0 (combine u bs).
   Definition decode := decode' base.
-  (* Does not carry; z becomes the lowest and only digit. *)
-  Definition encode (z : Z) := z :: nil.
+
+  (* i is current index, counts down *)
+  Fixpoint encode' z max i : digits :=
+    match i with
+    | O => nil
+    | S i' => let b := nth_default max base in 
+       encode' z max i' ++ ((z mod (b i)) / (b i')) :: nil
+    end.
+
+  (* max must be greater than input; this is used to truncate last digit *)
+  Definition encode z max := encode' z max (length base).
 
   Lemma decode'_truncate : forall bs us, decode' bs us = decode' bs (firstn (length bs) us).
   Proof.