From 99077ade35acba69fd31932ffdb8c35b863bcb11 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 2 Nov 2016 00:23:24 -0400 Subject: Lift conversion correctness proofs to ModularBaseSystem by providing [pack_rep] and [unpack_rep] lemmas --- src/ModularArithmetic/ModularBaseSystemProofs.v | 39 +++++++++++++++++++++++++ 1 file changed, 39 insertions(+) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index b454daab6..59a6f33db 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -1095,3 +1095,42 @@ Section SquareRootProofs. End Sqrt5mod8. End SquareRootProofs. + +Section ConversionProofs. + Context `{prm :PseudoMersenneBaseParams}. + Context {target_widths} + (target_widths_nonneg : forall x, In x target_widths -> 0 <= x) + (bits_eq : sum_firstn limb_widths (length limb_widths) = + sum_firstn target_widths (length target_widths)). + Local Notation target_base := (base_from_limb_widths target_widths). + + Lemma pack_rep : forall w, + bounded limb_widths (to_list _ w) -> + bounded target_widths (to_list _ w) -> + rep w (F.of_Z modulus + (BaseSystem.decode + target_base + (to_list _ (pack target_widths_nonneg bits_eq w)))). + Proof. + intros; cbv [pack ModularBaseSystemList.pack rep]. + rewrite Tuple.to_list_from_list. + apply F.eq_to_Z_iff. + rewrite F.to_Z_of_Z. + rewrite <-Conversion.convert_correct; auto using length_to_list. + Qed. + + Lemma unpack_rep : forall w, + bounded target_widths (to_list _ w) -> + rep (unpack target_widths_nonneg bits_eq w) + (F.of_Z modulus (BaseSystem.decode target_base (to_list _ w))). + Proof. + intros; cbv [unpack ModularBaseSystemList.unpack rep]. + apply F.eq_to_Z_iff. + rewrite <-from_list_default_eq with (d := 0). + rewrite <-decode_mod_Fdecode by apply Conversion.length_convert. + rewrite F.to_Z_of_Z. + rewrite <-Conversion.convert_correct; auto using length_to_list. + Qed. + + +End ConversionProofs. -- cgit v1.2.3