Verified secp256k1_laddermul

mit-plv · May 23, 2024 · d255ce2 · d255ce2
1 parent ad9b3f1
commit d255ce2
Show file tree

Hide file tree

Showing 3 changed files with 962 additions and 99 deletions.
diff --git a/src/Bedrock/End2End/Secp256k1/Addchain.v b/src/Bedrock/End2End/Secp256k1/Addchain.v
@@ -247,7 +247,6 @@ Section WithParameters.
     pose (inv := fun (v: nat) (t: trace) (m: @map.rep word byte BasicC32Semantics.mem) (l: @map.rep string word locals) => t = tr /\
                           exists i (Hi: 1 <= i <= to),
                           v = Z.to_nat (to - i) /\
-                            (* TODO: automate how to recover the frame *)
                           (exists vx, ((FElem pvar vx) * R)%sep m /\
                                    feval vx = F.pow (feval vvar) (N.pow 2%N (Z.to_N (i - 1))) /\
                                    bounded_by un_outbounds vx) /\