From ce8862f3df1d7a9a961e8d0823fff2353e3ac7c2 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 28 Jun 2016 21:22:39 -0400 Subject: 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. --- src/BaseSystem.v | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'src/BaseSystem.v') 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. -- cgit v1.2.3