saymrwulf/anza-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/anza-ed25519-verified.git synced 2026-09-04 20:24:06 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
anza-ed25519-verified/verification/gen/CurveScalar/Funs.lean
mrwulf 8440b53bdc Add scalar-layer foundation (Scalar52 arithmetic mod ℓ) 
Transpile the Scalar52 limb backend (backend::serial::u64::scalar
add/sub/mul/square/montgomery_*) from Rust to Lean via Charon/Aeneas,
scoped at the function level to the iterator-free arithmetic core.

  - verification/extract-scalar.sh: function-level Charon/Aeneas extraction
  - verification/gen/CurveScalar/{Types,Funs}.lean: transpiled model (28 defs)
  - verification/gen/CurveScalar/{TypesExternal,FunsExternal}.lean: hand-written
    external models (subtle.Choice + 2 subtle fns; namespace = curve25519)
  - verification/Proofs/ScalarDenote.lean: semantic foundation — Scalar52
    denotation into ℤ/ℓℤ, limb-bound invariant, and L_val (the transpiled
    constants::L denotes exactly the group order ℓ, kernel-checked)
  - verification/check-scalar.sh: guarded compile of the four gen modules
    plus the denotation foundation

check-scalar.sh passes: gen compiles; denotation + L = ℓ proven.
add/sub/mul remain in progress.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-02 21:19:58 +02:00

651 lines
27 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]: function definitions
import Aeneas
import CurveScalar.Types
import CurveScalar.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 curve25519
/-- [curve25519::backend::serial::u64::constants::L]
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/constants.rs', lines 129:0-135:3 -/
@[global_simps, irreducible]
def backend.serial.u64.constants.L : backend.serial.u64.scalar.Scalar52 :=
Array.make 5#usize [
671914833335277#u64, 3916664325105025#u64, 1367801#u64, 0#u64,
17592186044416#u64
]
/-- [curve25519::backend::serial::u64::constants::LFACTOR]
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/constants.rs', lines 138:0-138:48 -/
@[global_simps, irreducible]
def backend.serial.u64.constants.LFACTOR : Std.U64 := 1439961107955227#u64
/-- [curve25519::backend::serial::u64::constants::RR]
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/constants.rs', lines 150:0-156:3 -/
@[global_simps, irreducible]
def backend.serial.u64.constants.RR : backend.serial.u64.scalar.Scalar52 :=
Array.make 5#usize [
2764609938444603#u64, 3768881411696287#u64, 1616719297148420#u64,
1087343033131391#u64, 10175238647962#u64
]
/-- [curve25519::backend::serial::u64::scalar::{impl core::ops::index::Index<usize, u64> for curve25519::backend::serial::u64::scalar::Scalar52}::index]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 39:4-41:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
(self : backend.serial.u64.scalar.Scalar52) (_index : Std.Usize) :
Result Std.U64
:= do
Array.index_usize self _index
/-- [curve25519::backend::serial::u64::scalar::{impl core::ops::index::IndexMut<usize, u64> for curve25519::backend::serial::u64::scalar::Scalar52}::index_mut]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 45:4-47:5
Visibility: public -/
def
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexMutUsizeU64.index_mut
(self : backend.serial.u64.scalar.Scalar52) (_index : Std.Usize) :
Result (Std.U64 × (Std.U64 → backend.serial.u64.scalar.Scalar52))
:= do
let (i, index_mut_back) ← Array.index_mut_usize self _index
let back := fun i1 => let a := index_mut_back i1
a
ok (i, back)
/-- [curve25519::backend::serial::u64::scalar::m]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 52:0-54:1 -/
def backend.serial.u64.scalar.m
(x : Std.U64) (y : Std.U64) : Result Std.U128 := do
let i ← lift (UScalar.cast .U128 x)
let i1 ← lift (UScalar.cast .U128 y)
i * i1
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::ZERO]
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 58:4-58:57
Visibility: public -/
@[global_simps, irreducible]
def backend.serial.u64.scalar.Scalar52.ZERO
: backend.serial.u64.scalar.Scalar52 :=
let a := Array.repeat 5#usize 0#u64
a
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::conditional_add_l]: loop body 0:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 0:0-209:9 -/
@[rust_loop_body]
def backend.serial.u64.scalar.Scalar52.conditional_add_l_loop.body
(condition : subtle.Choice) (mask : Std.U64)
(iter : core.ops.range.Range Std.Usize)
(self : backend.serial.u64.scalar.Scalar52) (carry : Std.U64) :
Result (ControlFlow ((core.ops.range.Range Std.Usize) ×
backend.serial.u64.scalar.Scalar52 × Std.U64) (Std.U64 ×
backend.serial.u64.scalar.Scalar52))
:= do
let (o, iter1) ←
core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
match o with
| none => ok (done (carry, self))
| some i =>
let i1 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
backend.serial.u64.constants.L i
let addend ←
U64.Insts.SubtleConditionallySelectable.conditional_select 0#u64 i1
condition
let i2 ← carry >>> 52#i32
let i3 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
self i
let i4 ← i2 + i3
let carry1 ← i4 + addend
let (_, index_mut_back) ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexMutUsizeU64.index_mut
self i
let i5 ← lift (carry1 &&& mask)
let self1 := index_mut_back i5
ok (cont (iter1, self1, carry1))
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::conditional_add_l]: loop 0:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 0:0-209:9 -/
@[rust_loop]
def backend.serial.u64.scalar.Scalar52.conditional_add_l_loop
(iter : core.ops.range.Range Std.Usize)
(self : backend.serial.u64.scalar.Scalar52) (condition : subtle.Choice)
(carry : Std.U64) (mask : Std.U64) :
Result (Std.U64 × backend.serial.u64.scalar.Scalar52)
:= do
loop
(fun (iter1, self1, carry1) =>
backend.serial.u64.scalar.Scalar52.conditional_add_l_loop.body condition
mask iter1 self1 carry1)
(iter, self, carry)
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::conditional_add_l]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 201:4-212:5 -/
def backend.serial.u64.scalar.Scalar52.conditional_add_l
(self : backend.serial.u64.scalar.Scalar52) (condition : subtle.Choice) :
Result (Std.U64 × backend.serial.u64.scalar.Scalar52)
:= do
let i ← 1#u64 <<< 52#i32
let mask ← i - 1#u64
backend.serial.u64.scalar.Scalar52.conditional_add_l_loop
{ start := 0#usize, «end» := 5#usize } self condition 0#u64 mask
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::sub]: loop body 0:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 191:8-194:9
Visibility: public -/
@[rust_loop_body]
def backend.serial.u64.scalar.Scalar52.sub_loop.body
(a : backend.serial.u64.scalar.Scalar52)
(b : backend.serial.u64.scalar.Scalar52) (mask : Std.U64)
(iter : core.ops.range.Range Std.Usize)
(difference : backend.serial.u64.scalar.Scalar52) (borrow : Std.U64) :
Result (ControlFlow ((core.ops.range.Range Std.Usize) ×
backend.serial.u64.scalar.Scalar52 × Std.U64)
(backend.serial.u64.scalar.Scalar52 × Std.U64))
:= do
let (o, iter1) ←
core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
match o with
| none => ok (done (difference, borrow))
| some i =>
let i1 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
a i
let i2 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
b i
let i3 ← borrow >>> 63#i32
let i4 ← i2 + i3
let borrow1 ← lift (core.num.U64.wrapping_sub i1 i4)
let (_, index_mut_back) ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexMutUsizeU64.index_mut
difference i
let i5 ← lift (borrow1 &&& mask)
let difference1 := index_mut_back i5
ok (cont (iter1, difference1, borrow1))
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::sub]: loop 0:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 191:8-194:9
Visibility: public -/
@[rust_loop]
def backend.serial.u64.scalar.Scalar52.sub_loop
(iter : core.ops.range.Range Std.Usize)
(a : backend.serial.u64.scalar.Scalar52)
(b : backend.serial.u64.scalar.Scalar52)
(difference : backend.serial.u64.scalar.Scalar52) (mask : Std.U64)
(borrow : Std.U64) :
Result (backend.serial.u64.scalar.Scalar52 × Std.U64)
:= do
loop
(fun (iter1, difference1, borrow1) =>
backend.serial.u64.scalar.Scalar52.sub_loop.body a b mask iter1
difference1 borrow1)
(iter, difference, borrow)
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::sub]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 185:4-199:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.sub
(a : backend.serial.u64.scalar.Scalar52)
(b : backend.serial.u64.scalar.Scalar52) :
Result backend.serial.u64.scalar.Scalar52
:= do
let i ← 1#u64 <<< 52#i32
let mask ← i - 1#u64
let (difference, borrow) ←
backend.serial.u64.scalar.Scalar52.sub_loop
{ start := 0#usize, «end» := 5#usize } a b
backend.serial.u64.scalar.Scalar52.ZERO mask 0#u64
let i1 ← borrow >>> 63#i32
let i2 ← lift (UScalar.cast .U8 i1)
let c ← subtle.Choice.Insts.CoreConvertFromU8.from i2
let (_, difference1) ←
backend.serial.u64.scalar.Scalar52.conditional_add_l difference c
ok difference1
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::add]: loop body 0:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 175:8-178:9
Visibility: public -/
@[rust_loop_body]
def backend.serial.u64.scalar.Scalar52.add_loop.body
(a : backend.serial.u64.scalar.Scalar52)
(b : backend.serial.u64.scalar.Scalar52) (mask : Std.U64)
(iter : core.ops.range.Range Std.Usize)
(sum : backend.serial.u64.scalar.Scalar52) (carry : Std.U64) :
Result (ControlFlow ((core.ops.range.Range Std.Usize) ×
backend.serial.u64.scalar.Scalar52 × Std.U64)
backend.serial.u64.scalar.Scalar52)
:= do
let (o, iter1) ←
core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
match o with
| none => ok (done sum)
| some i =>
let i1 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
a i
let i2 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
b i
let i3 ← i1 + i2
let i4 ← carry >>> 52#i32
let carry1 ← i3 + i4
let (_, index_mut_back) ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexMutUsizeU64.index_mut
sum i
let i5 ← lift (carry1 &&& mask)
let sum1 := index_mut_back i5
ok (cont (iter1, sum1, carry1))
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::add]: loop 0:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 175:8-178:9
Visibility: public -/
@[rust_loop]
def backend.serial.u64.scalar.Scalar52.add_loop
(iter : core.ops.range.Range Std.Usize)
(a : backend.serial.u64.scalar.Scalar52)
(b : backend.serial.u64.scalar.Scalar52)
(sum : backend.serial.u64.scalar.Scalar52) (mask : Std.U64) (carry : Std.U64)
:
Result backend.serial.u64.scalar.Scalar52
:= do
loop
(fun (iter1, sum1, carry1) =>
backend.serial.u64.scalar.Scalar52.add_loop.body a b mask iter1 sum1
carry1)
(iter, sum, carry)
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::add]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 169:4-182:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.add
(a : backend.serial.u64.scalar.Scalar52)
(b : backend.serial.u64.scalar.Scalar52) :
Result backend.serial.u64.scalar.Scalar52
:= do
let i ← 1#u64 <<< 52#i32
let mask ← i - 1#u64
let sum ←
backend.serial.u64.scalar.Scalar52.add_loop
{ start := 0#usize, «end» := 5#usize } a b
backend.serial.u64.scalar.Scalar52.ZERO mask 0#u64
backend.serial.u64.scalar.Scalar52.sub sum backend.serial.u64.constants.L
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::mul_internal]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 230:4-244:5 -/
def backend.serial.u64.scalar.Scalar52.mul_internal
(a : backend.serial.u64.scalar.Scalar52)
(b : backend.serial.u64.scalar.Scalar52) :
Result (Array Std.U128 9#usize)
:= do
let z := Array.repeat 9#usize 0#u128
let i ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
0#usize
let i1 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
0#usize
let i2 ← backend.serial.u64.scalar.m i i1
let z1 ← Array.update z 0#usize i2
let i3 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
1#usize
let i4 ← backend.serial.u64.scalar.m i i3
let i5 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
1#usize
let i6 ← backend.serial.u64.scalar.m i5 i1
let i7 ← i4 + i6
let z2 ← Array.update z1 1#usize i7
let i8 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
2#usize
let i9 ← backend.serial.u64.scalar.m i i8
let i10 ← backend.serial.u64.scalar.m i5 i3
let i11 ← i9 + i10
let i12 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
2#usize
let i13 ← backend.serial.u64.scalar.m i12 i1
let i14 ← i11 + i13
let z3 ← Array.update z2 2#usize i14
let i15 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
3#usize
let i16 ← backend.serial.u64.scalar.m i i15
let i17 ← backend.serial.u64.scalar.m i5 i8
let i18 ← i16 + i17
let i19 ← backend.serial.u64.scalar.m i12 i3
let i20 ← i18 + i19
let i21 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
3#usize
let i22 ← backend.serial.u64.scalar.m i21 i1
let i23 ← i20 + i22
let z4 ← Array.update z3 3#usize i23
let i24 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index b
4#usize
let i25 ← backend.serial.u64.scalar.m i i24
let i26 ← backend.serial.u64.scalar.m i5 i15
let i27 ← i25 + i26
let i28 ← backend.serial.u64.scalar.m i12 i8
let i29 ← i27 + i28
let i30 ← backend.serial.u64.scalar.m i21 i3
let i31 ← i29 + i30
let i32 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
4#usize
let i33 ← backend.serial.u64.scalar.m i32 i1
let i34 ← i31 + i33
let z5 ← Array.update z4 4#usize i34
let i35 ← backend.serial.u64.scalar.m i5 i24
let i36 ← backend.serial.u64.scalar.m i12 i15
let i37 ← i35 + i36
let i38 ← backend.serial.u64.scalar.m i21 i8
let i39 ← i37 + i38
let i40 ← backend.serial.u64.scalar.m i32 i3
let i41 ← i39 + i40
let z6 ← Array.update z5 5#usize i41
let i42 ← backend.serial.u64.scalar.m i12 i24
let i43 ← backend.serial.u64.scalar.m i21 i15
let i44 ← i42 + i43
let i45 ← backend.serial.u64.scalar.m i32 i8
let i46 ← i44 + i45
let z7 ← Array.update z6 6#usize i46
let i47 ← backend.serial.u64.scalar.m i21 i24
let i48 ← backend.serial.u64.scalar.m i32 i15
let i49 ← i47 + i48
let z8 ← Array.update z7 7#usize i49
let i50 ← backend.serial.u64.scalar.m i32 i24
Array.update z8 8#usize i50
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::square_internal]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 249:4-268:5 -/
def backend.serial.u64.scalar.Scalar52.square_internal
(a : backend.serial.u64.scalar.Scalar52) :
Result (Array Std.U128 9#usize)
:= do
let i ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
0#usize
let i1 ← i * 2#u64
let i2 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
1#usize
let i3 ← i2 * 2#u64
let i4 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
2#usize
let i5 ← i4 * 2#u64
let i6 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
3#usize
let i7 ← i6 * 2#u64
let i8 ← backend.serial.u64.scalar.m i i
let i9 ← Array.index_usize (Array.make 4#usize [ i1, i3, i5, i7 ]) 0#usize
let i10 ← backend.serial.u64.scalar.m i9 i2
let i11 ← backend.serial.u64.scalar.m i9 i4
let i12 ← backend.serial.u64.scalar.m i2 i2
let i13 ← i11 + i12
let i14 ← backend.serial.u64.scalar.m i9 i6
let i15 ← Array.index_usize (Array.make 4#usize [ i1, i3, i5, i7 ]) 1#usize
let i16 ← backend.serial.u64.scalar.m i15 i4
let i17 ← i14 + i16
let i18 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index a
4#usize
let i19 ← backend.serial.u64.scalar.m i9 i18
let i20 ← backend.serial.u64.scalar.m i15 i6
let i21 ← i19 + i20
let i22 ← backend.serial.u64.scalar.m i4 i4
let i23 ← i21 + i22
let i24 ← backend.serial.u64.scalar.m i15 i18
let i25 ← Array.index_usize (Array.make 4#usize [ i1, i3, i5, i7 ]) 2#usize
let i26 ← backend.serial.u64.scalar.m i25 i6
let i27 ← i24 + i26
let i28 ← backend.serial.u64.scalar.m i25 i18
let i29 ← backend.serial.u64.scalar.m i6 i6
let i30 ← i28 + i29
let i31 ← Array.index_usize (Array.make 4#usize [ i1, i3, i5, i7 ]) 3#usize
let i32 ← backend.serial.u64.scalar.m i31 i18
let i33 ← backend.serial.u64.scalar.m i18 i18
ok (Array.make 9#usize [ i8, i10, i13, i17, i23, i27, i30, i32, i33 ])
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::montgomery_reduce::part2]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 282:8-285:9 -/
def backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2
(sum : Std.U128) : Result (Std.U128 × Std.U64) := do
let i ← lift (UScalar.cast .U64 sum)
let i1 ← 1#u64 <<< 52#i32
let i2 ← i1 - 1#u64
let w ← lift (i &&& i2)
let i3 ← sum >>> 52#i32
ok (i3, w)
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::montgomery_reduce::part1]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 276:8-279:9 -/
def backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1
(sum : Std.U128) : Result (Std.U128 × Std.U64) := do
let i ← lift (UScalar.cast .U64 sum)
let i1 ←
lift (core.num.U64.wrapping_mul i backend.serial.u64.constants.LFACTOR)
let i2 ← 1#u64 <<< 52#i32
let i3 ← i2 - 1#u64
let p ← lift (i1 &&& i3)
let i4 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
backend.serial.u64.constants.L 0#usize
let i5 ← backend.serial.u64.scalar.m p i4
let i6 ← sum + i5
let i7 ← i6 >>> 52#i32
ok (i7, p)
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::montgomery_reduce]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 273:4-306:5 -/
def backend.serial.u64.scalar.Scalar52.montgomery_reduce
(limbs : Array Std.U128 9#usize) :
Result backend.serial.u64.scalar.Scalar52
:= do
let i ← Array.index_usize limbs 0#usize
let (carry, n0) ←
backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i
let i1 ← Array.index_usize limbs 1#usize
let i2 ← carry + i1
let i3 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
backend.serial.u64.constants.L 1#usize
let i4 ← backend.serial.u64.scalar.m n0 i3
let i5 ← i2 + i4
let (carry1, n1) ←
backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i5
let i6 ← Array.index_usize limbs 2#usize
let i7 ← carry1 + i6
let i8 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
backend.serial.u64.constants.L 2#usize
let i9 ← backend.serial.u64.scalar.m n0 i8
let i10 ← i7 + i9
let i11 ← backend.serial.u64.scalar.m n1 i3
let i12 ← i10 + i11
let (carry2, n2) ←
backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i12
let i13 ← Array.index_usize limbs 3#usize
let i14 ← carry2 + i13
let i15 ← backend.serial.u64.scalar.m n1 i8
let i16 ← i14 + i15
let i17 ← backend.serial.u64.scalar.m n2 i3
let i18 ← i16 + i17
let (carry3, n3) ←
backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i18
let i19 ← Array.index_usize limbs 4#usize
let i20 ← carry3 + i19
let i21 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
backend.serial.u64.constants.L 4#usize
let i22 ← backend.serial.u64.scalar.m n0 i21
let i23 ← i20 + i22
let i24 ← backend.serial.u64.scalar.m n2 i8
let i25 ← i23 + i24
let i26 ← backend.serial.u64.scalar.m n3 i3
let i27 ← i25 + i26
let (carry4, n4) ←
backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 i27
let i28 ← Array.index_usize limbs 5#usize
let i29 ← carry4 + i28
let i30 ← backend.serial.u64.scalar.m n1 i21
let i31 ← i29 + i30
let i32 ← backend.serial.u64.scalar.m n3 i8
let i33 ← i31 + i32
let i34 ← backend.serial.u64.scalar.m n4 i3
let i35 ← i33 + i34
let (carry5, r0) ←
backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i35
let i36 ← Array.index_usize limbs 6#usize
let i37 ← carry5 + i36
let i38 ← backend.serial.u64.scalar.m n2 i21
let i39 ← i37 + i38
let i40 ← backend.serial.u64.scalar.m n4 i8
let i41 ← i39 + i40
let (carry6, r1) ←
backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i41
let i42 ← Array.index_usize limbs 7#usize
let i43 ← carry6 + i42
let i44 ← backend.serial.u64.scalar.m n3 i21
let i45 ← i43 + i44
let (carry7, r2) ←
backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i45
let i46 ← Array.index_usize limbs 8#usize
let i47 ← carry7 + i46
let i48 ← backend.serial.u64.scalar.m n4 i21
let i49 ← i47 + i48
let (carry8, r3) ←
backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i49
let r4 ← lift (UScalar.cast .U64 carry8)
backend.serial.u64.scalar.Scalar52.sub
(Array.make 5#usize [ r0, r1, r2, r3, r4 ]) backend.serial.u64.constants.L
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::mul]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 311:4-325:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.mul
(a : backend.serial.u64.scalar.Scalar52)
(b : backend.serial.u64.scalar.Scalar52) :
Result backend.serial.u64.scalar.Scalar52
:= do
let ab_limbs ← backend.serial.u64.scalar.Scalar52.mul_internal a b
let ab ← backend.serial.u64.scalar.Scalar52.montgomery_reduce ab_limbs
let rr_limbs ←
backend.serial.u64.scalar.Scalar52.mul_internal ab
backend.serial.u64.constants.RR
backend.serial.u64.scalar.Scalar52.montgomery_reduce rr_limbs
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::square]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 331:4-345:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.square
(self : backend.serial.u64.scalar.Scalar52) :
Result backend.serial.u64.scalar.Scalar52
:= do
let aa_limbs ← backend.serial.u64.scalar.Scalar52.square_internal self
let aa ← backend.serial.u64.scalar.Scalar52.montgomery_reduce aa_limbs
let rr_limbs ←
backend.serial.u64.scalar.Scalar52.mul_internal aa
backend.serial.u64.constants.RR
backend.serial.u64.scalar.Scalar52.montgomery_reduce rr_limbs
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::montgomery_mul]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 350:4-358:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.montgomery_mul
(a : backend.serial.u64.scalar.Scalar52)
(b : backend.serial.u64.scalar.Scalar52) :
Result backend.serial.u64.scalar.Scalar52
:= do
let limbs ← backend.serial.u64.scalar.Scalar52.mul_internal a b
backend.serial.u64.scalar.Scalar52.montgomery_reduce limbs
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::montgomery_square]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 363:4-371:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.montgomery_square
(self : backend.serial.u64.scalar.Scalar52) :
Result backend.serial.u64.scalar.Scalar52
:= do
let limbs ← backend.serial.u64.scalar.Scalar52.square_internal self
backend.serial.u64.scalar.Scalar52.montgomery_reduce limbs
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::as_montgomery]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 375:4-377:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.as_montgomery
(self : backend.serial.u64.scalar.Scalar52) :
Result backend.serial.u64.scalar.Scalar52
:= do
backend.serial.u64.scalar.Scalar52.montgomery_mul self
backend.serial.u64.constants.RR
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::from_montgomery]: loop body 0:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 384:8-386:9
Visibility: public -/
@[rust_loop_body]
def backend.serial.u64.scalar.Scalar52.from_montgomery_loop.body
(self : backend.serial.u64.scalar.Scalar52)
(iter : core.ops.range.Range Std.Usize) (limbs : Array Std.U128 9#usize) :
Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Array Std.U128
9#usize)) (Array Std.U128 9#usize))
:= do
let (o, iter1) ←
core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
match o with
| none => ok (done limbs)
| some i =>
let i1 ←
backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index
self i
let i2 ← lift (UScalar.cast .U128 i1)
let a ← Array.update limbs i i2
ok (cont (iter1, a))
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::from_montgomery]: loop 0:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 384:8-386:9
Visibility: public -/
@[rust_loop]
def backend.serial.u64.scalar.Scalar52.from_montgomery_loop
(iter : core.ops.range.Range Std.Usize)
(self : backend.serial.u64.scalar.Scalar52) (limbs : Array Std.U128 9#usize)
:
Result (Array Std.U128 9#usize)
:= do
loop
(fun (iter1, limbs1) =>
backend.serial.u64.scalar.Scalar52.from_montgomery_loop.body self iter1
limbs1)
(iter, limbs)
/-- [curve25519::backend::serial::u64::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::from_montgomery]:
Source: 'curve25519/solana-ed25519/src/backend/serial/u64/scalar.rs', lines 382:4-393:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.from_montgomery
(self : backend.serial.u64.scalar.Scalar52) :
Result backend.serial.u64.scalar.Scalar52
:= do
let limbs := Array.repeat 9#usize 0#u128
let limbs1 ←
backend.serial.u64.scalar.Scalar52.from_montgomery_loop
{ start := 0#usize, «end» := 5#usize } self limbs
backend.serial.u64.scalar.Scalar52.montgomery_reduce limbs1
end curve25519
Reference in a new issue View git blame Copy permalink