mirror of
https://github.com/saymrwulf/betrusted-ed25519-verified.git
synced 2026-09-04 20:24:08 +00:00
mrwulf
9620cf5dd4
Third pyramid capped. Identical shape to the risc0 fork (both are sha2-0.10 stacks): the hash oracle is the single monomorphic sha512_hash3(R, A, m) call, extraction runs --no-default-features. - gen/CurveSig: extracted verify glue, definitionally welded to the proven CurveField model (every curve and scalar call resolves to a certified definition; only the hash and wire formats are opaque). - Proofs/SigApexSpec.lean (unchanged from dalek): verify_loop_full with the standard three-axiom cone, and verify_accepts_iff — the verifier accepts IFF compress([s]B - [k]A) = R byte-for-byte. - check.sh Phase 3b enforces the apex cone to be EXACTLY [propext, Classical.choice, Quot.sound, ed25519.Signature, verifying.sha512_hash3, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new]. - extract.sh gains the reproducible CurveSig stanza (same recipe verified byte-exact on the risc0 fork this session). Full check.sh green: all standard certificates + the apex audit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
257 lines
9.9 KiB
Text
257 lines
9.9 KiB
Text
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
|
||
-- [ed25519_dalek]: function definitions
|
||
import Aeneas
|
||
import CurveSig.Types
|
||
import CurveSig.FunsExternal
|
||
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
|
||
|
||
/- You can remove the following line by using the CLI option `-all-computable`: -/
|
||
noncomputable section
|
||
|
||
namespace ed25519_dalek
|
||
|
||
/-- [ed25519_dalek::errors::{impl core::convert::From<ed25519_dalek::errors::InternalError> for signature::error::Error}::from]:
|
||
Source: 'ed25519-dalek/src/errors.rs', lines 111:4-113:5
|
||
Visibility: public -/
|
||
def signature.error.Error.Insts.CoreConvertFromInternalError.from
|
||
(_err : errors.InternalError) : Result signature.error.Error := do
|
||
signature.error.Error.new
|
||
|
||
/-- Trait implementation: [ed25519_dalek::errors::{impl core::convert::From<ed25519_dalek::errors::InternalError> for signature::error::Error}]
|
||
Source: 'ed25519-dalek/src/errors.rs', lines 109:0-119:1 -/
|
||
@[reducible]
|
||
def signature.error.Error.Insts.CoreConvertFromInternalError :
|
||
core.convert.From signature.error.Error errors.InternalError := {
|
||
from_ := signature.error.Error.Insts.CoreConvertFromInternalError.from
|
||
}
|
||
|
||
/-- [ed25519_dalek::signature::check_scalar::L_BYTES]
|
||
Source: 'ed25519-dalek/src/signature.rs', lines 108:4-111:6 -/
|
||
@[global_simps, irreducible]
|
||
def signature.check_scalar.L_BYTES : Array Std.U8 32#usize :=
|
||
Array.make 32#usize [
|
||
237#u8, 211#u8, 245#u8, 92#u8, 26#u8, 99#u8, 18#u8, 88#u8, 214#u8, 156#u8,
|
||
247#u8, 162#u8, 222#u8, 249#u8, 222#u8, 20#u8, 0#u8, 0#u8, 0#u8, 0#u8,
|
||
0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 16#u8
|
||
]
|
||
|
||
/-- [ed25519_dalek::signature::check_scalar]: loop body 0:
|
||
Source: 'ed25519-dalek/src/signature.rs', lines 116:4-127:5 -/
|
||
@[rust_loop_body]
|
||
def signature.check_scalar_loop.body
|
||
(bytes : Array Std.U8 32#usize) (lt : Bool) (decided : Bool) (i : Std.Usize)
|
||
:
|
||
Result (ControlFlow (Bool × Bool × Std.Usize) Bool)
|
||
:= do
|
||
if i > 0#usize
|
||
then
|
||
let j ← i - 1#usize
|
||
let (lt1, decided1) ←
|
||
if decided
|
||
then ok (lt, true)
|
||
else
|
||
do
|
||
let i1 ← Array.index_usize bytes j
|
||
let i2 ← Array.index_usize signature.check_scalar.L_BYTES j
|
||
if i1 < i2
|
||
then ok (true, true)
|
||
else let b ← if i1 > i2
|
||
then ok true
|
||
else ok false
|
||
ok (lt, b)
|
||
ok (cont (lt1, decided1, j))
|
||
else ok (done lt)
|
||
|
||
/-- [ed25519_dalek::signature::check_scalar]: loop 0:
|
||
Source: 'ed25519-dalek/src/signature.rs', lines 116:4-127:5 -/
|
||
@[rust_loop]
|
||
def signature.check_scalar_loop
|
||
(bytes : Array Std.U8 32#usize) (lt : Bool) (decided : Bool) (i : Std.Usize)
|
||
:
|
||
Result Bool
|
||
:= do
|
||
loop
|
||
(fun (lt1, decided1, i1) => signature.check_scalar_loop.body bytes lt1
|
||
decided1 i1)
|
||
(lt, decided, i)
|
||
|
||
/-- [ed25519_dalek::signature::check_scalar]:
|
||
Source: 'ed25519-dalek/src/signature.rs', lines 106:0-133:1 -/
|
||
def signature.check_scalar
|
||
(bytes : Array Std.U8 32#usize) :
|
||
Result (core.result.Result curve25519_dalek.scalar.Scalar
|
||
signature.error.Error)
|
||
:= do
|
||
let lt ← signature.check_scalar_loop bytes false false 32#usize
|
||
if lt
|
||
then
|
||
let s ← curve25519_dalek.scalar.Scalar.from_bytes_mod_order bytes
|
||
ok (core.result.Result.Ok s)
|
||
else
|
||
let e ←
|
||
core.convert.IntoFrom.into
|
||
signature.error.Error.Insts.CoreConvertFromInternalError
|
||
errors.InternalError.ScalarFormat
|
||
ok (core.result.Result.Err e)
|
||
|
||
/-- [ed25519_dalek::signature::{ed25519_dalek::signature::InternalSignature}::from_bytes]: loop body 0:
|
||
Source: 'ed25519-dalek/src/signature.rs', lines 196:8-200:9
|
||
Visibility: public -/
|
||
@[rust_loop_body]
|
||
def signature.InternalSignature.from_bytes_loop.body
|
||
(bytes : Array Std.U8 64#usize) (R_bytes : Array Std.U8 32#usize)
|
||
(s_bytes : Array Std.U8 32#usize) (i : Std.Usize) :
|
||
Result (ControlFlow ((Array Std.U8 32#usize) × (Array Std.U8 32#usize) ×
|
||
Std.Usize) ((Array Std.U8 32#usize) × (Array Std.U8 32#usize)))
|
||
:= do
|
||
if i < 32#usize
|
||
then
|
||
let i1 ← Array.index_usize bytes i
|
||
let a ← Array.update R_bytes i i1
|
||
let i2 ← i + 32#usize
|
||
let i3 ← Array.index_usize bytes i2
|
||
let a1 ← Array.update s_bytes i i3
|
||
let i4 ← i + 1#usize
|
||
ok (cont (a, a1, i4))
|
||
else ok (done (R_bytes, s_bytes))
|
||
|
||
/-- [ed25519_dalek::signature::{ed25519_dalek::signature::InternalSignature}::from_bytes]: loop 0:
|
||
Source: 'ed25519-dalek/src/signature.rs', lines 196:8-200:9
|
||
Visibility: public -/
|
||
@[rust_loop]
|
||
def signature.InternalSignature.from_bytes_loop
|
||
(bytes : Array Std.U8 64#usize) (R_bytes : Array Std.U8 32#usize)
|
||
(s_bytes : Array Std.U8 32#usize) (i : Std.Usize) :
|
||
Result ((Array Std.U8 32#usize) × (Array Std.U8 32#usize))
|
||
:= do
|
||
loop
|
||
(fun (R_bytes1, s_bytes1, i1) =>
|
||
signature.InternalSignature.from_bytes_loop.body bytes R_bytes1 s_bytes1
|
||
i1)
|
||
(R_bytes, s_bytes, i)
|
||
|
||
/-- [ed25519_dalek::signature::{ed25519_dalek::signature::InternalSignature}::from_bytes]:
|
||
Source: 'ed25519-dalek/src/signature.rs', lines 188:4-206:5
|
||
Visibility: public -/
|
||
def signature.InternalSignature.from_bytes
|
||
(bytes : Array Std.U8 64#usize) :
|
||
Result (core.result.Result signature.InternalSignature signature.error.Error)
|
||
:= do
|
||
let R_bytes := Array.repeat 32#usize 0#u8
|
||
let s_bytes := Array.repeat 32#usize 0#u8
|
||
let (R_bytes1, s_bytes1) ←
|
||
signature.InternalSignature.from_bytes_loop bytes R_bytes s_bytes 0#usize
|
||
let cey ← signature.compressed_from_bytes R_bytes1
|
||
let r ← signature.check_scalar s_bytes1
|
||
let cf ← core.result.Result.Insts.CoreOpsTry_traitTry.branch r
|
||
match cf with
|
||
| core.ops.control_flow.ControlFlow.Continue val =>
|
||
ok (core.result.Result.Ok { R := cey, s := val })
|
||
| core.ops.control_flow.ControlFlow.Break residual =>
|
||
core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
|
||
signature.InternalSignature (core.convert.FromSame signature.error.Error)
|
||
residual
|
||
|
||
/-- [ed25519_dalek::signature::{impl core::convert::TryFrom<&'_0 ed25519::Signature, signature::error::Error> for ed25519_dalek::signature::InternalSignature}::try_from]:
|
||
Source: 'ed25519-dalek/src/signature.rs', lines 212:4-214:5
|
||
Visibility: public -/
|
||
def
|
||
signature.InternalSignature.Insts.CoreConvertTryFromShared0SignatureError.try_from
|
||
(sig : ed25519.Signature) :
|
||
Result (core.result.Result signature.InternalSignature signature.error.Error)
|
||
:= do
|
||
let a ← ed25519.Signature.to_bytes sig
|
||
signature.InternalSignature.from_bytes a
|
||
|
||
/-- [ed25519_dalek::verifying::recompute_r_sha512]:
|
||
Source: 'ed25519-dalek/src/verifying.rs', lines 717:0-730:1 -/
|
||
def verifying.recompute_r_sha512
|
||
(key : verifying.VerifyingKey) (sig : signature.InternalSignature)
|
||
(message : Slice Std.U8) :
|
||
Result curve25519_dalek.edwards.CompressedEdwardsY
|
||
:= do
|
||
let a ← curve25519_dalek.edwards.CompressedEdwardsY.as_bytes sig.R
|
||
let s ← lift (Array.to_slice a)
|
||
let a1 ←
|
||
curve25519_dalek.edwards.CompressedEdwardsY.as_bytes key.compressed
|
||
let s1 ← lift (Array.to_slice a1)
|
||
let a2 ← verifying.sha512_hash3 s s1 message
|
||
let k ← curve25519_dalek.scalar.Scalar.from_bytes_mod_order_wide a2
|
||
let minus_A ←
|
||
curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
|
||
key.point
|
||
let ep ←
|
||
curve25519_dalek.edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint k
|
||
minus_A sig.s
|
||
curve25519_dalek.edwards.EdwardsPoint.compress ep
|
||
|
||
/-- [ed25519_dalek::verifying::verify_sha512]: loop body 0:
|
||
Source: 'ed25519-dalek/src/verifying.rs', lines 749:4-754:5 -/
|
||
@[rust_loop_body]
|
||
def verifying.verify_sha512_loop.body
|
||
(e : Array Std.U8 32#usize) (r : Array Std.U8 32#usize) (equal : Bool)
|
||
(i : Std.Usize) :
|
||
Result (ControlFlow (Bool × Std.Usize) Bool)
|
||
:= do
|
||
if i < 32#usize
|
||
then
|
||
let i1 ← Array.index_usize e i
|
||
let i2 ← Array.index_usize r i
|
||
let equal1 ← if i1 != i2
|
||
then ok false
|
||
else ok equal
|
||
let i3 ← i + 1#usize
|
||
ok (cont (equal1, i3))
|
||
else ok (done equal)
|
||
|
||
/-- [ed25519_dalek::verifying::verify_sha512]: loop 0:
|
||
Source: 'ed25519-dalek/src/verifying.rs', lines 749:4-754:5 -/
|
||
@[rust_loop]
|
||
def verifying.verify_sha512_loop
|
||
(e : Array Std.U8 32#usize) (r : Array Std.U8 32#usize) (equal : Bool)
|
||
(i : Std.Usize) :
|
||
Result Bool
|
||
:= do
|
||
loop
|
||
(fun (equal1, i1) => verifying.verify_sha512_loop.body e r equal1 i1)
|
||
(equal, i)
|
||
|
||
/-- [ed25519_dalek::verifying::verify_sha512]:
|
||
Source: 'ed25519-dalek/src/verifying.rs', lines 733:0-760:1 -/
|
||
def verifying.verify_sha512
|
||
(key : verifying.VerifyingKey) (message : Slice Std.U8)
|
||
(sig : ed25519.Signature) :
|
||
Result (core.result.Result Unit signature.error.Error)
|
||
:= do
|
||
let r ←
|
||
signature.InternalSignature.Insts.CoreConvertTryFromShared0SignatureError.try_from
|
||
sig
|
||
let cf ← core.result.Result.Insts.CoreOpsTry_traitTry.branch r
|
||
match cf with
|
||
| core.ops.control_flow.ControlFlow.Continue val =>
|
||
let expected_R ← verifying.recompute_r_sha512 key val message
|
||
let e ← curve25519_dalek.edwards.CompressedEdwardsY.as_bytes expected_R
|
||
let r1 ← curve25519_dalek.edwards.CompressedEdwardsY.as_bytes val.R
|
||
let equal ← verifying.verify_sha512_loop e r1 true 0#usize
|
||
if equal
|
||
then ok (core.result.Result.Ok ())
|
||
else
|
||
let e1 ←
|
||
core.convert.IntoFrom.into
|
||
signature.error.Error.Insts.CoreConvertFromInternalError
|
||
errors.InternalError.Verify
|
||
ok (core.result.Result.Err e1)
|
||
| core.ops.control_flow.ControlFlow.Break residual =>
|
||
core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
|
||
Unit (core.convert.FromSame signature.error.Error) residual
|
||
|
||
end ed25519_dalek
|