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
dalek-ed25519-verified/verification/gen/CurveScalar/Funs.lean
mrwulf 3a10206600 Hash-to-scalar PROVEN: from_bytes_wide_spec - Scalar::from_hash's reduction is exact mod l 
The apex brick of the scalar layer: for any 64 bytes (the opaque SHA-512
digest), [from_bytes_wide bytes] = (LE 512-bit value) mod l, with
canonical 52-bit-bounded output. Composition: bytes_unpack_spec (8x8
loops) -> split_words_lo/hi_spec (exact div/mod per limb, disjoint ORs
as additions) -> wide_split_telescope (isolated omega) -> montgomery_mul
by R and RR (R cancels as a unit, RR restores it) -> the canonical add.

The two kernel-capacity walls found and crossed en route (control repo
FAILURES.md updated):
- a montgomery_mul inside any walk motive replays its 400-line body at
  every kernel step (fix: named prefix functions in the pinned source);
- straight-line IndexMut closure chains make kernel defeq exponential in
  depth (fix: struct-literal construction - the split halves now build
  Scalar52([...]) directly). Full certificate: 77 s kernel-inclusive.

Regenerated gen (sources factor from_bytes_wide -> from_bytes_wide_parts
-> split_words_lo/hi; documented pure refactors, cargo-checked).
check-scalar.sh: 13 proof files, 13 kernel audits, all exactly
[propext, Classical.choice, Quot.sound]. Button pressed fresh: green.
2026-07-04 10:31:32 +02:00

826 lines
34 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]: 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_dalek
/-- [curve25519_dalek::backend::serial::u64::constants::L]
Source: 'curve25519-dalek/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_dalek::backend::serial::u64::constants::LFACTOR]
Source: 'curve25519-dalek/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_dalek::backend::serial::u64::constants::R]
Source: 'curve25519-dalek/src/backend/serial/u64/constants.rs', lines 141:0-147:3 -/
@[global_simps, irreducible]
def backend.serial.u64.constants.R : backend.serial.u64.scalar.Scalar52 :=
Array.make 5#usize [
4302102966953709#u64, 1049714374468698#u64, 4503599278581019#u64,
4503599627370495#u64, 17592186044415#u64
]
/-- [curve25519_dalek::backend::serial::u64::constants::RR]
Source: 'curve25519-dalek/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_dalek::backend::serial::u64::scalar::{impl core::ops::index::Index<usize, u64> for curve25519_dalek::backend::serial::u64::scalar::Scalar52}::index]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 43:4-45: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_dalek::backend::serial::u64::scalar::{impl core::ops::index::IndexMut<usize, u64> for curve25519_dalek::backend::serial::u64::scalar::Scalar52}::index_mut]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 49:4-51: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_dalek::backend::serial::u64::scalar::m]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 56:0-58: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::ZERO]
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 62:4-62: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::split_words_lo]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 96:4-105:5 -/
def backend.serial.u64.scalar.Scalar52.split_words_lo
(words : Array Std.U64 8#usize) :
Result backend.serial.u64.scalar.Scalar52
:= do
let i ← 1#u64 <<< 52#i32
let mask ← i - 1#u64
let i1 ← Array.index_usize words 0#usize
let i2 ← lift (i1 &&& mask)
let i3 ← i1 >>> 52#i32
let i4 ← Array.index_usize words 1#usize
let i5 ← i4 <<< 12#i32
let i6 ← lift (i3 ||| i5)
let i7 ← lift (i6 &&& mask)
let i8 ← i4 >>> 40#i32
let i9 ← Array.index_usize words 2#usize
let i10 ← i9 <<< 24#i32
let i11 ← lift (i8 ||| i10)
let i12 ← lift (i11 &&& mask)
let i13 ← i9 >>> 28#i32
let i14 ← Array.index_usize words 3#usize
let i15 ← i14 <<< 36#i32
let i16 ← lift (i13 ||| i15)
let i17 ← lift (i16 &&& mask)
let i18 ← i14 >>> 16#i32
let i19 ← Array.index_usize words 4#usize
let i20 ← i19 <<< 48#i32
let i21 ← lift (i18 ||| i20)
let i22 ← lift (i21 &&& mask)
ok (Array.make 5#usize [ i2, i7, i12, i17, i22 ])
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::split_words_hi]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 108:4-117:5 -/
def backend.serial.u64.scalar.Scalar52.split_words_hi
(words : Array Std.U64 8#usize) :
Result backend.serial.u64.scalar.Scalar52
:= do
let i ← 1#u64 <<< 52#i32
let mask ← i - 1#u64
let i1 ← Array.index_usize words 4#usize
let i2 ← i1 >>> 4#i32
let i3 ← lift (i2 &&& mask)
let i4 ← i1 >>> 56#i32
let i5 ← Array.index_usize words 5#usize
let i6 ← i5 <<< 8#i32
let i7 ← lift (i4 ||| i6)
let i8 ← lift (i7 &&& mask)
let i9 ← i5 >>> 44#i32
let i10 ← Array.index_usize words 6#usize
let i11 ← i10 <<< 20#i32
let i12 ← lift (i9 ||| i11)
let i13 ← lift (i12 &&& mask)
let i14 ← i10 >>> 32#i32
let i15 ← Array.index_usize words 7#usize
let i16 ← i15 <<< 32#i32
let i17 ← lift (i14 ||| i16)
let i18 ← lift (i17 &&& mask)
let i19 ← i15 >>> 20#i32
let i20 ← lift (i19 &&& mask)
ok (Array.make 5#usize [ i3, i8, i13, i18, i20 ])
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_bytes_wide_parts]: loop body 1:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 130:12-132:13 -/
@[rust_loop_body]
def backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts_loop0_loop0.body
(bytes : Array Std.U8 64#usize) (i : Std.Usize)
(iter : core.ops.range.Range Std.Usize) (words : Array Std.U64 8#usize) :
Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Array Std.U64
8#usize)) (Array Std.U64 8#usize))
:= do
let (o, iter1) ←
core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
match o with
| none => ok (done words)
| some j =>
let i1 ← i * 8#usize
let i2 ← i1 + j
let i3 ← Array.index_usize bytes i2
let i4 ← lift (UScalar.cast .U64 i3)
let i5 ← j * 8#usize
let i6 ← i4 <<< i5
let i7 ← Array.index_usize words i
let i8 ← lift (i7 ||| i6)
let a ← Array.update words i i8
ok (cont (iter1, a))
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_bytes_wide_parts]: loop 1:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 130:12-132:13 -/
@[rust_loop]
def backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts_loop0_loop0
(iter : core.ops.range.Range Std.Usize) (bytes : Array Std.U8 64#usize)
(words : Array Std.U64 8#usize) (i : Std.Usize) :
Result (Array Std.U64 8#usize)
:= do
loop
(fun (iter1, words1) =>
backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts_loop0_loop0.body
bytes i iter1 words1)
(iter, words)
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_bytes_wide_parts]: loop body 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 129:8-133:9 -/
@[rust_loop_body]
def backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts_loop0.body
(bytes : Array Std.U8 64#usize) (iter : core.ops.range.Range Std.Usize)
(words : Array Std.U64 8#usize) :
Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Array Std.U64
8#usize)) (Array Std.U64 8#usize))
:= do
let (o, iter1) ←
core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
match o with
| none => ok (done words)
| some i =>
let words1 ←
backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts_loop0_loop0
{ start := 0#usize, «end» := 8#usize } bytes words i
ok (cont (iter1, words1))
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_bytes_wide_parts]: loop 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 129:8-133:9 -/
@[rust_loop]
def backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts_loop0
(iter : core.ops.range.Range Std.Usize) (bytes : Array Std.U8 64#usize)
(words : Array Std.U64 8#usize) :
Result (Array Std.U64 8#usize)
:= do
loop
(fun (iter1, words1) =>
backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts_loop0.body bytes
iter1 words1)
(iter, words)
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_bytes_wide_parts]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 127:4-135:5 -/
def backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts
(bytes : Array Std.U8 64#usize) :
Result (backend.serial.u64.scalar.Scalar52 ×
backend.serial.u64.scalar.Scalar52)
:= do
let words := Array.repeat 8#usize 0#u64
let words1 ←
backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts_loop0
{ start := 0#usize, «end» := 8#usize } bytes words
let s ← backend.serial.u64.scalar.Scalar52.split_words_lo words1
let s1 ← backend.serial.u64.scalar.Scalar52.split_words_hi words1
ok (s, s1)
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_reduce::part2]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 300:8-303: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_reduce::part1]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 294:8-297: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::conditional_add_l]: loop body 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 0:0-227: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::conditional_add_l]: loop 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 0:0-227: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::conditional_add_l]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 219:4-230: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub]: loop body 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 209:8-212: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub]: loop 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 209:8-212: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::sub]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 203:4-217: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_reduce]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 291:4-324: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::mul_internal]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 248:4-262: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_mul]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 343:4-345: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 a1 ← backend.serial.u64.scalar.Scalar52.mul_internal a b
backend.serial.u64.scalar.Scalar52.montgomery_reduce a1
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::add]: loop body 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 193:8-196: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::add]: loop 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 193:8-196: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::add]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 187:4-200: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_bytes_wide]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 137:4-142:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.from_bytes_wide
(bytes : Array Std.U8 64#usize) :
Result backend.serial.u64.scalar.Scalar52
:= do
let (lo, hi) ←
backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts bytes
let lo1 ←
backend.serial.u64.scalar.Scalar52.montgomery_mul lo
backend.serial.u64.constants.R
let hi1 ←
backend.serial.u64.scalar.Scalar52.montgomery_mul hi
backend.serial.u64.constants.RR
backend.serial.u64.scalar.Scalar52.add hi1 lo1
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::square_internal]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 267:4-286: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::mul]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 328:4-331: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 a1 ← backend.serial.u64.scalar.Scalar52.mul_internal a b
let ab ← backend.serial.u64.scalar.Scalar52.montgomery_reduce a1
let a2 ←
backend.serial.u64.scalar.Scalar52.mul_internal ab
backend.serial.u64.constants.RR
backend.serial.u64.scalar.Scalar52.montgomery_reduce a2
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::square]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 336:4-339:5
Visibility: public -/
def backend.serial.u64.scalar.Scalar52.square
(self : backend.serial.u64.scalar.Scalar52) :
Result backend.serial.u64.scalar.Scalar52
:= do
let a ← backend.serial.u64.scalar.Scalar52.square_internal self
let aa ← backend.serial.u64.scalar.Scalar52.montgomery_reduce a
let a1 ←
backend.serial.u64.scalar.Scalar52.mul_internal aa
backend.serial.u64.constants.RR
backend.serial.u64.scalar.Scalar52.montgomery_reduce a1
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::montgomery_square]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 349:4-351: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 a ← backend.serial.u64.scalar.Scalar52.square_internal self
backend.serial.u64.scalar.Scalar52.montgomery_reduce a
/-- [curve25519_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::as_montgomery]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 355:4-357: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_montgomery]: loop body 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 364:8-366: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_montgomery]: loop 0:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 364:8-366: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_dalek::backend::serial::u64::scalar::{curve25519_dalek::backend::serial::u64::scalar::Scalar52}::from_montgomery]:
Source: 'curve25519-dalek/src/backend/serial/u64/scalar.rs', lines 362:4-368: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_dalek
Reference in a new issue View git blame Copy permalink