mirror of
https://github.com/saymrwulf/betrusted-ed25519-verified.git
synced 2026-09-04 20:24:08 +00:00
mrwulf
ee52d50e20
(verify_accepts_iff_decompress, button-enforced)
Port of the risc0 decompress chain (identical v4 gen shape: same
instance naming, same RangeFrom+closure from_bytes extraction):
- source patch cee0e17: decompress step_2 negate-then-conditional-assign
(the documented sqrt_ratio_i rewrite); extract.sh: decompress
un-opaqued, re-extracted - the step_1/step_2 external axioms vanish
from the template, decompress is transparent.
- Proofs/DecompressSpec.lean: dalek port, instance rename
Shared0FieldElement51 -> SharedAFieldElement51.
- Proofs/FromBytesSpec.lean: the v4 closure-loader walk
(range_from_index_spec + closure_call_spec; window/telescope math
identical to dalek).
- Proofs/DecompressMain.lean: decompress_of_canonical (standard three)
+ verify_accepts_iff_decompress (corollary verbatim):
accept <=> decompress(R) = [k]*(-A) + [s]*B (as points).
check.sh: 4-tier Phase 3b; full-lift cone exactly [3 standard +
Signature + sha512_hash3 + to_bytes + Error + Error.new]. Full button
green fresh.
THE FULL POINT-LEVEL LIFT NOW HOLDS ON ALL FOUR PYRAMIDS.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
132 lines
6.7 KiB
Text
132 lines
6.7 KiB
Text
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
|
|
-- [ed25519_dalek]: external functions.
|
|
-- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
|
|
import Aeneas
|
|
import CurveSig.Types
|
|
open Aeneas Aeneas.Std Result ControlFlow Error
|
|
set_option linter.dupNamespace false
|
|
set_option linter.hashCommand false
|
|
set_option linter.unusedVariables false
|
|
|
|
/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
|
|
set_option maxHeartbeats 1000000
|
|
|
|
/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
|
|
set_option maxRecDepth 2048
|
|
open ed25519_dalek
|
|
|
|
/-- [core::result::{impl core::ops::try_trait::Try for core::result::Result<T, E>}::branch]:
|
|
Source: '/rustc/library/core/src/result.rs', lines 2177:4-2177:64
|
|
Name pattern: [core::result::{core::ops::try_trait::Try<core::result::Result<@T, @E>>}::branch]
|
|
Visibility: public -/
|
|
@[rust_fun
|
|
"core::result::{core::ops::try_trait::Try<core::result::Result<@T, @E>>}::branch"]
|
|
axiom core.result.Result.Insts.CoreOpsTry_traitTry.branch
|
|
{T : Type} {E : Type} :
|
|
core.result.Result T E → Result (core.ops.control_flow.ControlFlow
|
|
(core.result.Result core.convert.Infallible E) T)
|
|
|
|
/-- [core::result::{impl core::ops::try_trait::FromResidual<core::result::Result<core::convert::Infallible, E>> for core::result::Result<T, F>}::from_residual]:
|
|
Source: '/rustc/library/core/src/result.rs', lines 2192:4-2192:70
|
|
Name pattern: [core::result::{core::ops::try_trait::FromResidual<core::result::Result<@T, @F>, core::result::Result<core::convert::Infallible, @E>>}::from_residual]
|
|
Visibility: public -/
|
|
@[rust_fun
|
|
"core::result::{core::ops::try_trait::FromResidual<core::result::Result<@T, @F>, core::result::Result<core::convert::Infallible, @E>>}::from_residual"]
|
|
axiom
|
|
core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
|
|
(T : Type) {E : Type} {F : Type} (convertFromInst : core.convert.From F E) :
|
|
core.result.Result core.convert.Infallible E → Result (core.result.Result T
|
|
F)
|
|
|
|
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::as_bytes]:
|
|
Source: 'curve25519-dalek/src/edwards.rs', lines 180:4-180:45
|
|
Name pattern: [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::as_bytes]
|
|
Visibility: public -/
|
|
@[rust_fun
|
|
"curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::as_bytes"]
|
|
axiom curve25519_dalek.edwards.CompressedEdwardsY.as_bytes
|
|
:
|
|
curve25519_dalek.edwards.CompressedEdwardsY → Result (Array Std.U8
|
|
32#usize)
|
|
|
|
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress]:
|
|
Source: 'curve25519-dalek/src/edwards.rs', lines 571:4-571:48
|
|
Name pattern: [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress]
|
|
Visibility: public -/
|
|
@[rust_fun
|
|
"curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::compress"]
|
|
axiom curve25519_dalek.edwards.EdwardsPoint.compress
|
|
:
|
|
curve25519_dalek.edwards.EdwardsPoint → Result
|
|
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 704:4-704:32
|
|
Name pattern: [curve25519_dalek::edwards::{core::ops::arith::Neg<curve25519_dalek::edwards::EdwardsPoint, curve25519_dalek::edwards::EdwardsPoint>}::neg]
|
|
Visibility: public -/
|
|
@[rust_fun
|
|
"curve25519_dalek::edwards::{core::ops::arith::Neg<curve25519_dalek::edwards::EdwardsPoint, curve25519_dalek::edwards::EdwardsPoint>}::neg"]
|
|
axiom
|
|
curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
|
|
:
|
|
curve25519_dalek.edwards.EdwardsPoint → Result
|
|
curve25519_dalek.edwards.EdwardsPoint
|
|
|
|
/-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint]:
|
|
Source: 'curve25519-dalek/src/edwards.rs', lines 907:4-911:21
|
|
Name pattern: [curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint]
|
|
Visibility: public -/
|
|
@[rust_fun
|
|
"curve25519_dalek::edwards::{curve25519_dalek::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint"]
|
|
axiom curve25519_dalek.edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint
|
|
:
|
|
curve25519_dalek.scalar.Scalar → curve25519_dalek.edwards.EdwardsPoint →
|
|
curve25519_dalek.scalar.Scalar → Result
|
|
curve25519_dalek.edwards.EdwardsPoint
|
|
|
|
/-- [curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order]:
|
|
Source: 'curve25519-dalek/src/scalar.rs', lines 244:4-244:58
|
|
Name pattern: [curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order]
|
|
Visibility: public -/
|
|
@[rust_fun
|
|
"curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order"]
|
|
axiom curve25519_dalek.scalar.Scalar.from_bytes_mod_order
|
|
: Array Std.U8 32#usize → Result curve25519_dalek.scalar.Scalar
|
|
|
|
/-- [curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order_wide]:
|
|
Source: 'curve25519-dalek/src/scalar.rs', lines 257:4-257:64
|
|
Name pattern: [curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order_wide]
|
|
Visibility: public -/
|
|
@[rust_fun
|
|
"curve25519_dalek::scalar::{curve25519_dalek::scalar::Scalar}::from_bytes_mod_order_wide"]
|
|
axiom curve25519_dalek.scalar.Scalar.from_bytes_mod_order_wide
|
|
: Array Std.U8 64#usize → Result curve25519_dalek.scalar.Scalar
|
|
|
|
/-- [ed25519::{ed25519::Signature}::to_bytes]:
|
|
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ed25519-2.2.3/src/lib.rs', lines 351:4-351:44
|
|
Name pattern: [ed25519::{ed25519::Signature}::to_bytes]
|
|
Visibility: public -/
|
|
@[rust_fun "ed25519::{ed25519::Signature}::to_bytes"]
|
|
axiom ed25519.Signature.to_bytes
|
|
: ed25519.Signature → Result (Array Std.U8 64#usize)
|
|
|
|
/-- [signature::error::{signature::error::Error}::new]:
|
|
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/signature-2.2.0/src/error.rs', lines 34:4-34:24
|
|
Name pattern: [signature::error::{signature::error::Error}::new]
|
|
Visibility: public -/
|
|
@[rust_fun "signature::error::{signature::error::Error}::new"]
|
|
axiom signature.error.Error.new : Result signature.error.Error
|
|
|
|
/-- [ed25519_dalek::signature::compressed_from_bytes]:
|
|
Source: 'ed25519-dalek/src/signature.rs', lines 69:0-71:1 -/
|
|
axiom signature.compressed_from_bytes
|
|
:
|
|
Array Std.U8 32#usize → Result curve25519_dalek.edwards.CompressedEdwardsY
|
|
|
|
/-- [ed25519_dalek::verifying::sha512_hash3]:
|
|
Source: 'ed25519-dalek/src/verifying.rs', lines 708:0-714:1 -/
|
|
axiom verifying.sha512_hash3
|
|
:
|
|
Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result (Array Std.U8
|
|
64#usize)
|
|
|