add printing of inverse code.

raaz-crypto · May 12, 2023 · fb21725 · fb21725
1 parent e4fb973
commit fb21725
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/src/Verse/CryptoLib/curve25519/c/field.v b/src/Verse/CryptoLib/curve25519/c/field.v
@@ -1037,6 +1037,19 @@ Compute snd (inverse cp' z' cp z).
 
 Goal to_print (inverse cp' z' cp z).
   unfold inverse.
+  unfold ibitsRep.
+  lazy [repSteps repStep swapStep repeatIt step2 step multStep squareStep Nat.modulo Nat.div Nat.divmod ibitsRep fst snd Nat.sub swapVar].
+
+  unfold repSteps.
+  unfold repStep.
+  unfold repeatIt.
+  Locate "mod".
+  unfold Nat.modulo.
+  unfold Nat.div.
+  unfold Nat.divmod.
+
+
+  unfold swapStep.
   simpl.
 Abort.