saymrwulf/betrusted-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/betrusted-ed25519-verified.git synced 2026-09-04 20:24:08 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
betrusted-ed25519-verified/verification/gen/CurveField/FunsExternal_Template.lean
mrwulf dee1554d8e Merge scalar into CurveField: one type universe, serial-only backend 
Replicates dalek's gen merge: extract.sh co-extracts the Scalar52 backend
and scalar::from_bytes_mod_order[_wide] into the CurveField model, pins
RUSTFLAGS --cfg curve25519_dalek_backend="serial" (SIMD dispatch compiles
out; get_selected_backend becomes a real definition), and upgrades
unwrap_u8 to the documented Choice-model definition. ScalarDenote repoints
by one import line; both buttons green over the merged gen.

Prepares the verify-glue integration (CurveSig) on this fork.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-04 22:20:26 +02:00

335 lines
18 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [curve25519_dalek]: external functions.
-- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
import Aeneas
import CurveField.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 curve25519_dalek
/-- [core::array::{impl core::hash::Hash for [T; N]}::hash]:
Source: '/rustc/library/core/src/array/mod.rs', lines 349:4-349:50
Name pattern: [core::array::{core::hash::Hash<[@T; @N]>}::hash]
Visibility: public -/
@[rust_fun "core::array::{core::hash::Hash<[@T; @N]>}::hash"]
axiom Array.Insts.CoreHashHash.hash
{T : Type} {H : Type} {N : Std.Usize} (hashHashInst : core.hash.Hash T)
(hashHasherInst : core.hash.Hasher H) :
Array T N → H → Result H
/-- [core::fmt::{impl core::fmt::Debug for [T]}::fmt]:
Source: '/rustc/library/core/src/fmt/mod.rs', lines 3122:4-3122:50
Name pattern: [core::fmt::{core::fmt::Debug<[@T]>}::fmt]
Visibility: public -/
@[rust_fun "core::fmt::{core::fmt::Debug<[@T]>}::fmt"]
axiom Slice.Insts.CoreFmtDebug.fmt
{T : Type} (DebugInst : core.fmt.Debug T) :
Slice T → core.fmt.Formatter → Result ((core.result.Result Unit
core.fmt.Error) × core.fmt.Formatter)
/-- [core::hash::impls::{impl core::hash::Hash for u8}::hash]:
Source: '/rustc/library/core/src/hash/mod.rs', lines 812:16-812:56
Name pattern: [core::hash::impls::{core::hash::Hash<u8>}::hash]
Visibility: public -/
@[rust_fun "core::hash::impls::{core::hash::Hash<u8>}::hash"]
axiom U8.Insts.CoreHashHash.hash
{H : Type} (HasherInst : core.hash.Hasher H) : Std.U8 → H → Result H
/-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::backward_checked]
Visibility: public -/
@[rust_fun
"core::iter::range::{core::iter::range::Step<u32>}::backward_checked"]
axiom U32.Insts.CoreIterRangeStep.backward_checked
: Std.U32 → Std.Usize → Result (Option Std.U32)
/-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_checked]:
Source: '/rustc/library/core/src/iter/range.rs', lines 282:16-282:73
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::forward_checked]
Visibility: public -/
@[rust_fun
"core::iter::range::{core::iter::range::Step<u32>}::forward_checked"]
axiom U32.Insts.CoreIterRangeStep.forward_checked
: Std.U32 → Std.Usize → Result (Option Std.U32)
/-- [core::iter::range::{impl core::iter::range::Step for u32}::steps_between]:
Source: '/rustc/library/core/src/iter/range.rs', lines 271:16-271:84
Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::steps_between]
Visibility: public -/
@[rust_fun "core::iter::range::{core::iter::range::Step<u32>}::steps_between"]
axiom U32.Insts.CoreIterRangeStep.steps_between
: Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize))
/-- [core::slice::index::{impl core::slice::index::SliceIndex<[T], [T]> for core::ops::range::RangeFull}::index_mut]:
Source: '/rustc/library/core/src/slice/index.rs', lines 660:4-660:51
Name pattern: [core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::index_mut]
Visibility: public -/
@[rust_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::index_mut"]
axiom
core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index_mut
{T : Type} :
core.ops.range.RangeFull → Slice T → Result ((Slice T) × (Slice T →
Slice T))
/-- [core::slice::index::{impl core::slice::index::SliceIndex<[T], [T]> for core::ops::range::RangeFull}::index]:
Source: '/rustc/library/core/src/slice/index.rs', lines 655:4-655:39
Name pattern: [core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::index]
Visibility: public -/
@[rust_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::index"]
axiom core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index
{T : Type} : core.ops.range.RangeFull → Slice T → Result (Slice T)
/-- [core::slice::index::{impl core::slice::index::SliceIndex<[T], [T]> for core::ops::range::RangeFull}::get_unchecked_mut]:
Source: '/rustc/library/core/src/slice/index.rs', lines 650:4-650:66
Name pattern: [core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get_unchecked_mut]
Visibility: public -/
@[rust_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get_unchecked_mut"]
axiom
core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked_mut
{T : Type} :
core.ops.range.RangeFull → MutRawPtr (Slice T) → Result (MutRawPtr (Slice
T))
/-- [core::slice::index::{impl core::slice::index::SliceIndex<[T], [T]> for core::ops::range::RangeFull}::get_unchecked]:
Source: '/rustc/library/core/src/slice/index.rs', lines 645:4-645:66
Name pattern: [core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get_unchecked]
Visibility: public -/
@[rust_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get_unchecked"]
axiom
core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked
{T : Type} :
core.ops.range.RangeFull → ConstRawPtr (Slice T) → Result (ConstRawPtr
(Slice T))
/-- [core::slice::index::{impl core::slice::index::SliceIndex<[T], [T]> for core::ops::range::RangeFull}::get_mut]:
Source: '/rustc/library/core/src/slice/index.rs', lines 640:4-640:57
Name pattern: [core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get_mut]
Visibility: public -/
@[rust_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get_mut"]
axiom core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_mut
{T : Type} :
core.ops.range.RangeFull → Slice T → Result ((Option (Slice T)) ×
(Option (Slice T) → Slice T))
/-- [core::slice::index::{impl core::slice::index::SliceIndex<[T], [T]> for core::ops::range::RangeFull}::get]:
Source: '/rustc/library/core/src/slice/index.rs', lines 635:4-635:45
Name pattern: [core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get]
Visibility: public -/
@[rust_fun
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get"]
axiom core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
{T : Type} :
core.ops.range.RangeFull → Slice T → Result (Option (Slice T))
/-- [subtle::{subtle::Choice}::unwrap_u8]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 133:4-133:33
Name pattern: [subtle::{subtle::Choice}::unwrap_u8]
Visibility: public -/
@[rust_fun "subtle::{subtle::Choice}::unwrap_u8"]
axiom subtle.Choice.unwrap_u8 : subtle.Choice → Result Std.U8
/-- [subtle::{impl core::convert::From<subtle::Choice> for bool}::from]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 153:4-153:35
Name pattern: [subtle::{core::convert::From<bool, subtle::Choice>}::from]
Visibility: public -/
@[rust_fun "subtle::{core::convert::From<bool, subtle::Choice>}::from"]
axiom Bool.Insts.CoreConvertFromChoice.from : subtle.Choice → Result Bool
/-- [subtle::{impl core::ops::bit::BitAnd<subtle::Choice, subtle::Choice> for subtle::Choice}::bitand]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 162:4-162:42
Name pattern: [subtle::{core::ops::bit::BitAnd<subtle::Choice, subtle::Choice, subtle::Choice>}::bitand]
Visibility: public -/
@[rust_fun
"subtle::{core::ops::bit::BitAnd<subtle::Choice, subtle::Choice, subtle::Choice>}::bitand"]
axiom subtle.Choice.Insts.CoreOpsBitBitAndChoiceChoice.bitand
: subtle.Choice → subtle.Choice → Result subtle.Choice
/-- [subtle::{impl core::ops::bit::BitOr<subtle::Choice, subtle::Choice> for subtle::Choice}::bitor]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 177:4-177:41
Name pattern: [subtle::{core::ops::bit::BitOr<subtle::Choice, subtle::Choice, subtle::Choice>}::bitor]
Visibility: public -/
@[rust_fun
"subtle::{core::ops::bit::BitOr<subtle::Choice, subtle::Choice, subtle::Choice>}::bitor"]
axiom subtle.Choice.Insts.CoreOpsBitBitOrChoiceChoice.bitor
: subtle.Choice → subtle.Choice → Result subtle.Choice
/-- [subtle::{impl core::convert::From<u8> for subtle::Choice}::from]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 238:4-238:32
Name pattern: [subtle::{core::convert::From<subtle::Choice, u8>}::from]
Visibility: public -/
@[rust_fun "subtle::{core::convert::From<subtle::Choice, u8>}::from"]
axiom subtle.Choice.Insts.CoreConvertFromU8.from
: Std.U8 → Result subtle.Choice
/-- [subtle::{impl subtle::ConstantTimeEq for [T]}::ct_eq]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 313:4-313:41
Name pattern: [subtle::{subtle::ConstantTimeEq<[@T]>}::ct_eq]
Visibility: public -/
@[rust_fun "subtle::{subtle::ConstantTimeEq<[@T]>}::ct_eq"]
axiom Slice.Insts.SubtleConstantTimeEq.ct_eq
{T : Type} (ConstantTimeEqInst : subtle.ConstantTimeEq T) :
Slice T → Slice T → Result subtle.Choice
/-- [subtle::{impl subtle::ConstantTimeEq for u8}::ct_eq]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 348:12-348:51
Name pattern: [subtle::{subtle::ConstantTimeEq<u8>}::ct_eq]
Visibility: public -/
@[rust_fun "subtle::{subtle::ConstantTimeEq<u8>}::ct_eq"]
axiom U8.Insts.SubtleConstantTimeEq.ct_eq
: Std.U8 → Std.U8 → Result subtle.Choice
/-- [subtle::ConditionallySelectable::conditional_assign]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 442:4-442:66
Name pattern: [subtle::ConditionallySelectable::conditional_assign]
Visibility: public -/
@[rust_fun "subtle::ConditionallySelectable::conditional_assign"]
axiom subtle.ConditionallySelectable.conditional_assign.default
{Self : Type} (ConditionallySelectableInst : subtle.ConditionallySelectable
Self) :
Self → Self → subtle.Choice → Result Self
/-- [subtle::ConditionallySelectable::conditional_swap]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 469:4-469:67
Name pattern: [subtle::ConditionallySelectable::conditional_swap]
Visibility: public -/
@[rust_fun "subtle::ConditionallySelectable::conditional_swap"]
axiom subtle.ConditionallySelectable.conditional_swap.default
{Self : Type} (ConditionallySelectableInst : subtle.ConditionallySelectable
Self) :
Self → Self → subtle.Choice → Result (Self × Self)
/-- [subtle::{impl subtle::ConditionallySelectable for u64}::conditional_select]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 513:12-513:77
Name pattern: [subtle::{subtle::ConditionallySelectable<u64>}::conditional_select]
Visibility: public -/
@[rust_fun
"subtle::{subtle::ConditionallySelectable<u64>}::conditional_select"]
axiom U64.Insts.SubtleConditionallySelectable.conditional_select
: Std.U64 → Std.U64 → subtle.Choice → Result Std.U64
/-- [subtle::{impl subtle::ConditionallySelectable for u64}::conditional_assign]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 521:12-521:74
Name pattern: [subtle::{subtle::ConditionallySelectable<u64>}::conditional_assign]
Visibility: public -/
@[rust_fun
"subtle::{subtle::ConditionallySelectable<u64>}::conditional_assign"]
axiom U64.Insts.SubtleConditionallySelectable.conditional_assign
: Std.U64 → Std.U64 → subtle.Choice → Result Std.U64
/-- [subtle::{impl subtle::ConditionallySelectable for u64}::conditional_swap]:
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 529:12-529:75
Name pattern: [subtle::{subtle::ConditionallySelectable<u64>}::conditional_swap]
Visibility: public -/
@[rust_fun "subtle::{subtle::ConditionallySelectable<u64>}::conditional_swap"]
axiom U64.Insts.SubtleConditionallySelectable.conditional_swap
: Std.U64 → Std.U64 → subtle.Choice → Result (Std.U64 × Std.U64)
/-- [curve25519_dalek::backend::get_selected_backend]:
Source: 'curve25519-dalek/src/backend/mod.rs', lines 55:0-75:1 -/
axiom backend.get_selected_backend : Result backend.BackendKind
/-- [curve25519_dalek::backend::serial::scalar_mul::variable_base::mul]:
Source: 'curve25519-dalek/src/backend/serial/scalar_mul/variable_base.rs', lines 11:0-48:1 -/
axiom backend.serial.scalar_mul.variable_base.mul
: edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
/-- [curve25519_dalek::backend::serial::curve_models::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::curve_models::ProjectiveNielsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 295:0-311:1
Visibility: public -/
axiom
backend.serial.curve_models.ProjectiveNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
backend.serial.curve_models.ProjectiveNielsPoint →
backend.serial.curve_models.ProjectiveNielsPoint → subtle.Choice →
Result (backend.serial.curve_models.ProjectiveNielsPoint ×
backend.serial.curve_models.ProjectiveNielsPoint)
/-- [curve25519_dalek::backend::serial::curve_models::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::curve_models::AffineNielsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 313:0-327:1
Visibility: public -/
axiom
backend.serial.curve_models.AffineNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
backend.serial.curve_models.AffineNielsPoint →
backend.serial.curve_models.AffineNielsPoint → subtle.Choice → Result
(backend.serial.curve_models.AffineNielsPoint ×
backend.serial.curve_models.AffineNielsPoint)
/-- [curve25519_dalek::edwards::decompress::step_2]:
Source: 'curve25519-dalek/src/edwards.rs', lines 223:4-240: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 209:4-220: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 404:4-406:5
Visibility: public -/
axiom edwards.CompressedEdwardsY.from_slice
:
Slice Std.U8 → Result (core.result.Result edwards.CompressedEdwardsY
core.array.TryFromSliceError)
/-- [curve25519_dalek::edwards::{impl subtle::ConditionallySelectable for curve25519_dalek::edwards::EdwardsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/edwards.rs', lines 467:0-476:1
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_swap
:
edwards.EdwardsPoint → edwards.EdwardsPoint → subtle.Choice → Result
(edwards.EdwardsPoint × edwards.EdwardsPoint)
/-- [curve25519_dalek::edwards::{impl subtle::ConditionallySelectable for curve25519_dalek::edwards::EdwardsPoint}::conditional_assign]:
Source: 'curve25519-dalek/src/edwards.rs', lines 467:0-476:1
Visibility: public -/
axiom
edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_assign
:
edwards.EdwardsPoint → edwards.EdwardsPoint → subtle.Choice → Result
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 501:0-501:27
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.CoreCmpEq.assert_fields_are_eq
: edwards.EdwardsPoint → Result Unit
/-- [curve25519_dalek::edwards::{impl core::iter::traits::accum::Sum<T> for curve25519_dalek::edwards::EdwardsPoint}::sum]:
Source: 'curve25519-dalek/src/edwards.rs', lines 671:4-676:5
Visibility: public -/
axiom edwards.EdwardsPoint.Insts.CoreIterTraitsAccumSum.sum
{T : Type} {I : Type} (coreborrowBorrowTEdwardsPointInst : core.borrow.Borrow
T edwards.EdwardsPoint) (coreitertraitsiteratorIteratorInst :
core.iter.traits.iterator.Iterator I T) :
I → Result edwards.EdwardsPoint
/-- [curve25519_dalek::field::{impl core::cmp::Eq for curve25519_dalek::backend::serial::u64::field::FieldElement51}::assert_fields_are_eq]:
Source: 'curve25519-dalek/src/field.rs', lines 84:0-84:27
Visibility: public -/
axiom
backend.serial.u64.field.FieldElement51.Insts.CoreCmpEq.assert_fields_are_eq
: backend.serial.u64.field.FieldElement51 → Result Unit
Reference in a new issue View git blame Copy permalink