Commit ac89c1a8 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

reran the proofs on sandor

parent 97e9a094
......@@ -222,7 +222,7 @@
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="WP_parameter ladder_is_functional.8.3" expl="VC for ladder_is_functional">
<proof prover="2"><result status="valid" time="7.91"/></proof>
<proof prover="2"><result status="valid" time="6.76"/></proof>
</goal>
</transf>
</goal>
......
......@@ -435,7 +435,7 @@
<proof prover="2"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="WP_parameter mladder.36.16" expl="VC for mladder">
<proof prover="2"><result status="valid" time="0.75"/></proof>
<proof prover="2"><result status="valid" time="0.57"/></proof>
</goal>
<goal name="WP_parameter mladder.36.17" expl="VC for mladder">
<proof prover="2"><result status="valid" time="0.72"/></proof>
......@@ -601,7 +601,7 @@
<proof prover="1"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="WP_parameter mladder.53" expl="loop invariant preservation">
<proof prover="1"><result status="valid" time="0.50"/></proof>
<proof prover="1"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="WP_parameter mladder.54" expl="loop invariant preservation">
<proof prover="1"><result status="valid" time="0.46"/></proof>
......
This diff is collapsed.
......@@ -139,11 +139,6 @@ f6e043357cc7582c4c814b8004b77f8e type invariantainfix <amixfix []V7V8c256Aainfix
a70c3e20b957c84a5c245f2ac9df03cf postconditionainfix =asumaTuple2amk address_spaceV7c0c0c32amodasumaTuple2V2c0c0c32ap25519Iainfix <amixfix []V7V8c256Aainfix <=c0amixfix []V7V8FIainfix =agetV7V9agetV6V9Iainfix <V9ainfix +c31c1Aainfix <=c0V9FAainfix <=agetV7V10c255Aainfix <=c0agetV7V10FFIainfix <=
01a054a80460c847ceb3cc52480ead99 postconditionainfix =ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +
189d656671551f84ac43572b5acc3c58 VC for fe25519_mulainfix ===asumaTuple2V8c0c0c32ainfix *asumaTuple2V4c0c0c32asumaTuple2V3c0c0c32Iainfix <asumaTuple2V8c0c0c32ainfix +apow2c255ainfix *c38ainfix +apow2c248c37Aainfix ===asumaTuple2V8c0c0c32asumaTuple2amk address_spaceV6c0c0c64Aainfix <amixfix []
0fa3f42543a9141d1957b9c825c34c39 VC for fe25519_mul121666ainfix ===asumaTuple2V7c0c0c32ainfix *asumaTuple2V2c0c0c32c121666Iainfix <asumaTuple2V7c0c0c32ainfix +apow2c255ainfix *c38ainfix +apow2c248c37Aainfix ===asumaTuple2V7c0c0c32asumaTuple2amk address_spaceV5c0c0c64Aainfix <amixfix []V6V
139abc3a39c7792a779c06fc1b4f00a9 type invariantainfix <amixfix []V4V5c256Aainfix <=c0amixfix []V4V5FIainfix <amixfix []V4V6c256Aainfix <=c0amixfix []V4V6FFIainfix =agetV3V7c0Iainfix <V7c32Aainfix <=c3V7FAainfix =agetV3c2c0x01Aainfix =agetV3c1c0xDBAainfix =agetV3c0c0x42Aainfix <amixfix []V
4a9f7495d049ec0a95693389b39cabcd type invariantainfix <amixfix []V5V6c256Aainfix <=c0amixfix []V5V6FIainfix =asumaTuple2amk address_spaceV5c0c0c64ainfix *asumaTuple2V2c0c0c32asumaTuple2amk address_spaceV3c0c0c32Aainfix <amixfix []V5V7c256Aainfix <=c0amixfix []V5V7FFIainfix <amixfix []V4V8
28bb889913a544f49cf70a66d8a5d025 postconditionainfix ===asumaTuple2V7c0c0c32ainfix *asumaTuple2V2c0c0c32c121666Iainfix <asumaTuple2V7c0c0c32ainfix +apow2c255ainfix *c38ainfix +apow2c248c37Aainfix ===asumaTuple2V7c0c0c32asumaTuple2amk address_spaceV5c0c0c64Aainfix <amixfix []V6V8c256Aainfix <=
aeff5e3295baaf27ea4140883f7e893d postconditionainfix =amodainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +ainfix +
d5bc2f22fdb0b26fc0981e9ef0f30db7 VC for fe25519_squareainfix ===asumaTuple2V6c0c0c32ainfix *asumaTuple2V2c0c0c32asumaTuple2V2c0c0c32Iainfix <asumaTuple2V6c0c0c32ainfix +apow2c255ainfix *c38ainfix +apow2c248c37Aainfix ===asumaTuple2V6c0c0c32asumaTuple2amk address_spaceV4c0c0c64Aainfix <amixfix []
98368704bea13b194f5dede97b8309d1 VC for fe25519_mul_rxainfix <asumaTuple2V7c0c0c32ainfix +apow2c255ainfix *c38ainfix +apow2c248c37Aainfix ===asumaTuple2V7c0c0c32ainfix *asumaTuple2V3c0c0c32asumaTuple2V2c0c0c32Iainfix <asumaTuple2V7c0c0c32ainfix +apow2c255ainfix *c38ainfix +apow2c248c37Aainfix ===
223acca1f8f3d7568da893a9a7521462 VC for fe25519_mul_ryainfix ===asumaTuple2V7c0c0c32ainfix *asumaTuple2V2c0c0c32asumaTuple2V3c0c0c32Iainfix <asumaTuple2V7c0c0c32ainfix +apow2c255ainfix *c38ainfix +apow2c248c37Aainfix ===asumaTuple2V7c0c0c32asumaTuple2amk address_spaceV5c0c0c64Aainfix <amixfix []
......
......@@ -33,7 +33,7 @@
<proof prover="1" memlimit="8000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter inverse.6" expl="loop invariant preservation">
<proof prover="6"><result status="valid" time="1.23"/></proof>
<proof prover="6"><result status="valid" time="0.99"/></proof>
</goal>
<goal name="WP_parameter inverse.7" expl="loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -171,7 +171,7 @@
<goal name="WP_parameter fermat" expl="VC for fermat">
<transf name="split_goal_wp">
<goal name="WP_parameter fermat.1" expl="precondition">
<proof prover="0" timelimit="30"><result status="valid" time="1.75"/></proof>
<proof prover="0" timelimit="30"><result status="valid" time="1.44"/></proof>
</goal>
<goal name="WP_parameter fermat.2" expl="assertion">
<proof prover="1"><result status="valid" time="0.08"/></proof>
......@@ -229,7 +229,7 @@
<goal name="WP_parameter fermat.14" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter fermat.14.1" expl="VC for fermat">
<proof prover="0" timelimit="30" memlimit="8000"><result status="valid" time="15.43"/></proof>
<proof prover="0" timelimit="30" memlimit="8000"><result status="valid" time="13.55"/></proof>
</goal>
<goal name="WP_parameter fermat.14.2" expl="VC for fermat">
<proof prover="0" timelimit="30" memlimit="8000"><result status="valid" time="0.03"/></proof>
......@@ -239,7 +239,7 @@
<goal name="WP_parameter fermat.15" expl="assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter fermat.15.1" expl="VC for fermat">
<proof prover="0" memlimit="8000"><result status="valid" time="2.55"/></proof>
<proof prover="0" memlimit="8000"><result status="valid" time="2.02"/></proof>
</goal>
<goal name="WP_parameter fermat.15.2" expl="VC for fermat">
<proof prover="0"><result status="valid" time="0.10"/></proof>
......@@ -346,7 +346,7 @@
<goal name="WP_parameter fermat.27.1" expl="assertion">
<transf name="compute_in_goal">
<goal name="WP_parameter fermat.27.1.1" expl="assertion">
<proof prover="0" timelimit="30"><result status="valid" time="0.90"/></proof>
<proof prover="0" timelimit="30"><result status="valid" time="0.75"/></proof>
</goal>
</transf>
</goal>
......@@ -359,7 +359,7 @@
<goal name="WP_parameter fermat.27.4" expl="VC for fermat">
<transf name="compute_in_goal">
<goal name="WP_parameter fermat.27.4.1" expl="VC for fermat">
<proof prover="0"><result status="valid" time="0.56"/></proof>
<proof prover="0"><result status="valid" time="0.36"/></proof>
</goal>
</transf>
</goal>
......@@ -378,7 +378,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter fermat.30" expl="precondition">
<proof prover="0"><result status="valid" time="1.53"/></proof>
<proof prover="0"><result status="valid" time="1.23"/></proof>
</goal>
<goal name="WP_parameter fermat.31" expl="postcondition">
<proof prover="0"><result status="valid" time="0.06"/></proof>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment