saymrwulf/dalek-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/dalek-ed25519-verified.git synced 2026-09-04 20:24:12 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Phase 2, brick 3 opened: decompress extracted for real (gen green)

Browse source 
extract.sh drops --opaque crate::edwards::decompress: step_1/step_2,
sqrt_ratio_i, pow_p58, and FieldElement51::from_bytes now extract as real
code (source aa0f6ab patches step_2's conditional_negate to the documented
negate-then-conditional-assign - the ConditionallyNegatable blanket impl
is the one thing the toolchain cannot translate). No new axioms: the
slice-level ct_eq the sqrt check needs was already a real def. Full
button green on the regenerated universe.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-05 18:04:04 +02:00
parent fe021b9486
commit a2803fe34e
8 changed files with 1001 additions and 972 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
verification/CurveField.llbc
View file

File diff suppressed because one or more lines are too long

2
verification/CurveSig.llbc
View file

File diff suppressed because one or more lines are too long

1
verification/extract.sh
View file

@ -54,7 +54,6 @@ charon cargo --preset=aeneas \
--opaque 'crate::backend::serial::scalar_mul::pippenger' \
--opaque 'crate::backend::vector' \
--opaque 'crate::backend::get_selected_backend' \
--opaque 'crate::edwards::decompress' \
--opaque 'crate::edwards::_::sum' \
--opaque 'crate::edwards::_::from_slice' \
--dest-file "$HERE/CurveField.llbc" \

1919
verification/gen/CurveField/Funs.lean
View file

File diff suppressed because it is too large Load diff

29
verification/gen/CurveField/FunsExternal_Template.lean
View file

@ -315,30 +315,13 @@ axiom edwards.affine.AffinePoint.Insts.CoreCmpEq.assert_fields_are_eq
: edwards.affine.AffinePoint → Result Unit
/-- [curve25519_dalek::edwards::{impl core::cmp::Eq for curve25519_dalek::edwards::CompressedEdwardsY}::assert_fields_are_eq]:
Source: 'curve25519-dalek/src/edwards.rs', lines 183:0-183:33
Source: 'curve25519-dalek/src/edwards.rs', lines 182:0-182:33
Visibility: public -/
axiom edwards.CompressedEdwardsY.Insts.CoreCmpEq.assert_fields_are_eq
: edwards.CompressedEdwardsY → Result Unit
/-- [curve25519_dalek::edwards::decompress::step_2]:
Source: 'curve25519-dalek/src/edwards.rs', lines 240:4-257:5 -/
axiom edwards.decompress.step_2
:
edwards.CompressedEdwardsY → backend.serial.u64.field.FieldElement51 →
backend.serial.u64.field.FieldElement51 →
backend.serial.u64.field.FieldElement51 → Result edwards.EdwardsPoint
/-- [curve25519_dalek::edwards::decompress::step_1]:
Source: 'curve25519-dalek/src/edwards.rs', lines 226:4-237:5 -/
axiom edwards.decompress.step_1
:
edwards.CompressedEdwardsY → Result (subtle.Choice ×
backend.serial.u64.field.FieldElement51 ×
backend.serial.u64.field.FieldElement51 ×
backend.serial.u64.field.FieldElement51)
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::from_slice]:
Source: 'curve25519-dalek/src/edwards.rs', lines 423:4-425:5
Source: 'curve25519-dalek/src/edwards.rs', lines 428:4-430:5
Visibility: public -/
axiom edwards.CompressedEdwardsY.from_slice
:
@ -346,7 +329,7 @@ axiom edwards.CompressedEdwardsY.from_slice
core.array.TryFromSliceError)
/-- [curve25519_dalek::edwards::{impl subtle::ConditionallySelectable for curve25519_dalek::edwards::EdwardsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/edwards.rs', lines 486:0-495:1
Source: 'curve25519-dalek/src/edwards.rs', lines 491:0-500:1
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
@ -354,7 +337,7 @@ axiom edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_swap
(edwards.EdwardsPoint × edwards.EdwardsPoint)
/-- [curve25519_dalek::edwards::{impl subtle::ConditionallySelectable for curve25519_dalek::edwards::EdwardsPoint}::conditional_assign]:
Source: 'curve25519-dalek/src/edwards.rs', lines 486:0-495:1
Source: 'curve25519-dalek/src/edwards.rs', lines 491:0-500:1
Visibility: public -/
axiom
edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_assign
@ -363,7 +346,7 @@ axiom
edwards.EdwardsPoint
/-- [curve25519_dalek::edwards::{impl core::cmp::Eq for curve25519_dalek::edwards::EdwardsPoint}::assert_fields_are_eq]:
Source: 'curve25519-dalek/src/edwards.rs', lines 520:0-520:27
Source: 'curve25519-dalek/src/edwards.rs', lines 525:0-525:27
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.CoreCmpEq.assert_fields_are_eq
: edwards.EdwardsPoint → Result Unit
@ -378,7 +361,7 @@ axiom field.FieldElement51.internal_invert_batch
backend.serial.u64.field.FieldElement51))
/-- [curve25519_dalek::edwards::{impl core::iter::traits::accum::Sum<T> for curve25519_dalek::edwards::EdwardsPoint}::sum]:
Source: 'curve25519-dalek/src/edwards.rs', lines 841:4-846:5
Source: 'curve25519-dalek/src/edwards.rs', lines 846:4-851:5
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.CoreIterTraitsAccumSum.sum
{T : Type} {I : Type} (coreborrowBorrowTEdwardsPointInst : core.borrow.Borrow

8
verification/gen/CurveField/Types.lean
View file

@ -161,7 +161,7 @@ structure traits.ValidityCheck (Self : Type) where
is_valid : Self → Result Bool
/-- [curve25519_dalek::edwards::EdwardsPoint]
Source: 'curve25519-dalek/src/edwards.rs', lines 390:0-395:1
Source: 'curve25519-dalek/src/edwards.rs', lines 395:0-400:1
Visibility: public -/
structure edwards.EdwardsPoint where
X : backend.serial.u64.field.FieldElement51
@ -200,7 +200,7 @@ structure edwards.affine.AffinePoint where
y : backend.serial.u64.field.FieldElement51
/-- [curve25519_dalek::edwards::CompressedEdwardsY]
Source: 'curve25519-dalek/src/edwards.rs', lines 175:0-175:44
Source: 'curve25519-dalek/src/edwards.rs', lines 174:0-174:44
Visibility: public -/
@[reducible]
def edwards.CompressedEdwardsY := Array Std.U8 32#usize
@ -212,13 +212,13 @@ def edwards.CompressedEdwardsY := Array Std.U8 32#usize
def montgomery.MontgomeryPoint := Array Std.U8 32#usize
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress_batch::closure#1]
Source: 'curve25519-dalek/src/edwards.rs', lines 625:29-629:9 -/
Source: 'curve25519-dalek/src/edwards.rs', lines 630:29-634:9 -/
def edwards.EdwardsPoint.compress_batch.closure_1 (N : Std.Usize) :=
Array edwards.EdwardsPoint N × Array backend.serial.u64.field.FieldElement51
N
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress_batch::closure]
Source: 'curve25519-dalek/src/edwards.rs', lines 622:50-622:65 -/
Source: 'curve25519-dalek/src/edwards.rs', lines 627:50-627:65 -/
@[reducible]
def edwards.EdwardsPoint.compress_batch.closure (N : Std.Usize) :=
Array edwards.EdwardsPoint N

8
verification/gen/CurveSig/FunsExternal_Template.lean
View file

@ -39,7 +39,7 @@ axiom
F)
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::as_bytes]:
Source: 'curve25519-dalek/src/edwards.rs', lines 198:4-198:45
Source: 'curve25519-dalek/src/edwards.rs', lines 197:4-197:45
Name pattern: [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::as_bytes]
Visibility: public -/
@[rust_fun
@ -50,7 +50,7 @@ axiom curve25519_dalek.edwards.CompressedEdwardsY.as_bytes
32#usize)
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress]:
Source: 'curve25519-dalek/src/edwards.rs', lines 615:4-615:48
Source: 'curve25519-dalek/src/edwards.rs', lines 620:4-620:48
Name pattern: [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress]
Visibility: public -/
@[rust_fun
@ -61,7 +61,7 @@ axiom curve25519_dalek.edwards.EdwardsPoint.compress
curve25519_dalek.edwards.CompressedEdwardsY
/-- [curve25519_dalek::edwards::{impl core::ops::arith::Neg<curve25519_dalek::edwards::EdwardsPoint> for curve25519_dalek::edwards::EdwardsPoint}::neg]:
Source: 'curve25519-dalek/src/edwards.rs', lines 869:4-869:32
Source: 'curve25519-dalek/src/edwards.rs', lines 874:4-874:32
Name pattern: [curve25519_dalek::edwards::{core::ops::arith::Neg<curve25519_dalek::edwards::EdwardsPoint, curve25519_dalek::edwards::EdwardsPoint>}::neg]
Visibility: public -/
@[rust_fun
@ -73,7 +73,7 @@ axiom
curve25519_dalek.edwards.EdwardsPoint
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint]:
Source: 'curve25519-dalek/src/edwards.rs', lines 1080:4-1084:21
Source: 'curve25519-dalek/src/edwards.rs', lines 1085:4-1089:21
Name pattern: [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint]
Visibility: public -/
@[rust_fun

4
verification/gen/CurveSig/TypesExternal_Template.lean
View file

@ -14,14 +14,14 @@ set_option maxHeartbeats 1000000
set_option maxRecDepth 2048
/-- [curve25519_dalek::edwards::CompressedEdwardsY]
Source: 'curve25519-dalek/src/edwards.rs', lines 175:0-175:29
Source: 'curve25519-dalek/src/edwards.rs', lines 174:0-174:29
Name pattern: [curve25519_dalek::edwards::CompressedEdwardsY]
Visibility: public -/
@[rust_type "curve25519_dalek::edwards::CompressedEdwardsY"]
axiom curve25519_dalek.edwards.CompressedEdwardsY : Type
/-- [curve25519_dalek::edwards::EdwardsPoint]
Source: 'curve25519-dalek/src/edwards.rs', lines 390:0-390:23
Source: 'curve25519-dalek/src/edwards.rs', lines 395:0-395:23
Name pattern: [curve25519_dalek::edwards::EdwardsPoint]
Visibility: public -/
@[rust_type "curve25519_dalek::edwards::EdwardsPoint"]