Defined real versions of [pow] and [inv] in ModularBaseSystem, replacing placeholders, and proved their correctness. In the process, reorganized early parts of ModularBaseSystemProofs.v by moving some lemmas to PseudoMersenneBaseParamProofs.v and introducing lemmas about the algebraic properties of ModularBaseSystem operations.

1 files changed, 7 insertions, 2 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index e771e7eb4..2f264fa6c 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -11,6 +11,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystemList.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs.
 Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.AdditionChainExponentiation.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Tactics.VerdiTactics.
 Local Open Scope Z_scope.
@@ -45,8 +46,12 @@ Section ModularBaseSystem.
   (* Placeholder *)
   Definition opp (x : digits) : digits := encode (F.opp (decode x)).
 
-  (* Placeholder *)
-  Definition inv (x : digits) : digits := encode (F.inv (decode x)).
+  Definition pow (x : digits) (chain : list (nat * nat)) : digits :=
+    fold_chain one mul chain (x :: nil).
+
+  Definition inv (chain : list (nat * nat))
+                 (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus - 2))
+                 (x : digits) : digits := pow x chain.
 
   (* Placeholder *)
   Definition div (x y : digits) : digits := encode (F.div (decode x) (decode y)).