mirror of
https://github.com/saymrwulf/anza-ed25519-verified.git
synced 2026-09-06 20:41:08 +00:00
THE SIGNATURE APEX on the anza fork: verify_accepts_iff, button-enforced
FOURTH AND FINAL PYRAMID CAPPED - the signature layer is complete on all four ed25519 forks. anza's verify code lives in the same crate as the curve (solana-ed25519), so the whole verify path joins the merged CurveField extraction directly: one universe, no glue layer, no FQ-name welding, and the Error enum plus the parse/filter helpers are all real extracted code. - extract.sh: verify_sha512 start-from joins the merged stanza; sha512_hash3 and the foreign ed25519 crate opaque; RUSTFLAGS --cfg curve25519_serial_only pins the serial backend so get_selected_backend extracts as the real constant Serial (the stale dispatch axiom is deleted from FunsExternal). - gen/CurveField externals: real defs for the ?-operator plumbing (Try::branch, FromResidual) and faithful identity models for Choice::unwrap_u8 (transparent-u8 body: self.0) and the RangeFull get_unchecked[_mut] raw-pointer pair (Rust body returns the pointer unchanged) - the three would-be cone intruders, eliminated. - Proofs/SigApexSpec.lean: verify_loop_full (standard three-axiom cone) and verify_accepts_iff - the verifier accepts IFF the recomputed compress([k](-A) + [s]B) equals the signature's R byte-for-byte, with the ZIP-215 legacy filters and the s < l parse conditioned by hypotheses, mirroring the siblings' hparse. - check.sh Phase 3b enforces the apex cone to be EXACTLY [propext, Classical.choice, Quot.sound, ed25519.Signature, ed_sigs.sha512_hash3, ed25519.Signature.r_bytes, ed25519.Signature.s_bytes] - the tightest boundary of the four pyramids: the SHA-512 oracle plus the foreign wire-format type and its two byte accessors, nothing else. check.sh (incl. Phase 3b) + check-scalar.sh both green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
parent
984d82a7d7
commit
771dc11cab
10 changed files with 916 additions and 236 deletions
File diff suppressed because one or more lines are too long
207
verification/Proofs/SigApexSpec.lean
Normal file
207
verification/Proofs/SigApexSpec.lean
Normal file
|
|
@ -0,0 +1,207 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────────
|
||||
Proofs/SigApexSpec.lean — the signature-layer apex, phase 1:
|
||||
the EdDSA verification equation, SHA-512 opaque.
|
||||
|
||||
`VerificationKey.verify_sha512 self sig msg` is the extracted
|
||||
solana-ed25519 verifier (dalek-style canonical-R path, gen/CurveField —
|
||||
anza's verify code lives in the SAME crate as the curve, so the whole
|
||||
path shares one extraction universe): run the legacy filters, parse the
|
||||
scalar `s`, recompute
|
||||
R' = compress( [k]·(−A) + [s]·B ) (k from the SHA-512 hash)
|
||||
and accept iff R' equals the signature's R, byte-for-byte.
|
||||
|
||||
This file proves the verifier's control flow reduces EXACTLY to that
|
||||
recompute-and-compare — the literal EdDSA check — over the PROVEN curve
|
||||
model. SHA-512 stays an opaque oracle: the statement holds for whatever
|
||||
bytes the hash produces, so the theorem is the honest
|
||||
"accept ↔ the recomputed compressed point equals R".
|
||||
|
||||
The legacy filters (all-zero key, excluded R list) and the s < ℓ parse
|
||||
are fixed by hypotheses, mirroring the sibling pyramids' `hparse`; the
|
||||
apex boundary is the tightest of the four: the SHA-512 oracle plus the
|
||||
foreign `ed25519::Signature` type with its two byte accessors — the
|
||||
`Error` enum and the backend dispatch are real extracted code here.
|
||||
|
||||
Phase 2 (the point-level equation, needing `to_bytes` canonicity and
|
||||
`decompress`) is deliberately deferred and documented — mirroring the
|
||||
dsm layer's phase split.
|
||||
────────────────────────────────────────────────────────────────────────────── -/
|
||||
import Proofs.ScalarDenote
|
||||
import Proofs.AddSpec
|
||||
open Aeneas Aeneas.Std Result ControlFlow
|
||||
open curve25519
|
||||
|
||||
set_option maxHeartbeats 4000000
|
||||
set_option linter.unusedSimpArgs false
|
||||
set_option maxRecDepth 8000
|
||||
|
||||
namespace CurveFieldProofs
|
||||
|
||||
open Aeneas.Std.WP
|
||||
|
||||
/-- Byte-equality of two 32-byte arrays over the tail `[n, 32)`. -/
|
||||
def rangeEq (e r : Array Std.U8 32#usize) (n : ℕ) : Prop :=
|
||||
∀ j, n ≤ j → j < 32 → e.val[j]! = r.val[j]!
|
||||
|
||||
instance (e r : Array Std.U8 32#usize) (n : ℕ) : Decidable (rangeEq e r n) := by
|
||||
have : rangeEq e r n ↔ ∀ j, j < 32 → n ≤ j → e.val[j]! = r.val[j]! := by
|
||||
unfold rangeEq; exact ⟨fun h j hj hn => h j hn hj, fun h j hn hj => h j hj hn⟩
|
||||
exact decidable_of_iff _ this.symm
|
||||
|
||||
/-- **The comparison loop returns byte-equality.** From accumulator `b` at
|
||||
index `i ≤ 32`, `verify_sha512_loop` returns `b ∧ (all bytes in [i,32)
|
||||
agree)`. NOTE the extracted loop's parameter order is `(r, e, b, i)`
|
||||
while the body compares `e[k] != r[k]`. -/
|
||||
theorem verify_loop_spec (e r : Array Std.U8 32#usize) :
|
||||
∀ (n : ℕ) (b : Bool) (i : Usize), i.val = 32 - n → n ≤ 32 →
|
||||
ed_sigs.verification_key.VerificationKey.verify_sha512_loop r e b i
|
||||
⦃ res => res = (b && decide (rangeEq e r (32 - n))) ⦄ := by
|
||||
intro n
|
||||
induction n with
|
||||
| zero =>
|
||||
intro b i hi _
|
||||
unfold ed_sigs.verification_key.VerificationKey.verify_sha512_loop
|
||||
apply loop_step
|
||||
simp only [ed_sigs.verification_key.VerificationKey.verify_sha512_loop.body]
|
||||
have hge : ¬ (i < 32#usize) := by clear * - hi; scalar_tac
|
||||
rw [if_neg hge]
|
||||
try simp only [spec_ok]
|
||||
have hemp : decide (rangeEq e r (32 - 0)) = true := by
|
||||
simp only [decide_eq_true_eq]; intro j hj1 hj2; omega
|
||||
rw [hemp, Bool.and_true]
|
||||
| succ n ih =>
|
||||
intro b i hi hle
|
||||
unfold ed_sigs.verification_key.VerificationKey.verify_sha512_loop
|
||||
apply loop_step
|
||||
simp only [ed_sigs.verification_key.VerificationKey.verify_sha512_loop.body]
|
||||
have hlt : i < 32#usize := by clear * - hi hle; scalar_tac
|
||||
rw [if_pos hlt]
|
||||
have hiv : i.val = 32 - (n + 1) := hi
|
||||
have hb1 : i.val < (e.val).length := by clear * - hle hiv; scalar_tac
|
||||
have hb2 : i.val < (r.val).length := by clear * - hle hiv; scalar_tac
|
||||
-- e[i], r[i]
|
||||
step as ⟨x, hx⟩
|
||||
step as ⟨y, hy⟩
|
||||
-- the accumulator update: reduce the `if` to a plain `ok`
|
||||
have hite : (if (x != y) = true then (ok false : Result Bool) else ok b)
|
||||
= ok (if (x != y) = true then false else b) := by
|
||||
by_cases hc : (x != y) = true
|
||||
· rw [if_pos hc, if_pos hc]
|
||||
· rw [if_neg hc, if_neg hc]
|
||||
rw [hite]
|
||||
-- name the reduced accumulator, then reduce the trivial `ok` bind
|
||||
generalize heq1 : (if (x != y) = true then false else b) = eq1
|
||||
simp only [bind_tc_ok]
|
||||
-- i + 1
|
||||
step as ⟨i3, hi3⟩
|
||||
have hnext : i3.val = 32 - n := by clear * - hi3 hiv hle; scalar_tac
|
||||
try simp only [spec_ok]
|
||||
-- close with the IH at (eq1, i3); rewrite the range split
|
||||
apply spec_mono (ih eq1 i3 hnext (by omega))
|
||||
intro res hres
|
||||
rw [hres]
|
||||
-- eq1 = (b && e[i]=r[i]); the [i,32) range = byte i ∧ [i+1,32)
|
||||
have hxv : x = e.val[i.val]'hb1 := by rw [hx]
|
||||
have hyv : y = r.val[i.val]'hb2 := by rw [hy]
|
||||
have heq1v : eq1 = (b && decide (e.val[i.val]! = r.val[i.val]!)) := by
|
||||
rw [← heq1, hxv, hyv]
|
||||
rw [getElem!_pos e.val i.val hb1, getElem!_pos r.val i.val hb2]
|
||||
by_cases h : e.val[i.val]'hb1 = r.val[i.val]'hb2
|
||||
· have hb : ¬ ((e.val[i.val]'hb1 != r.val[i.val]'hb2) = true) := by
|
||||
simp [bne_iff_ne, h]
|
||||
rw [if_neg hb]; simp [h]
|
||||
· have hb : (e.val[i.val]'hb1 != r.val[i.val]'hb2) = true := by
|
||||
simp [bne_iff_ne, h]
|
||||
rw [if_pos hb]; simp [h]
|
||||
rw [heq1v, Bool.and_assoc]
|
||||
congr 1
|
||||
-- decide(byte i) && decide(tail [i+1,32)) = decide(rangeEq [i,32))
|
||||
have hiff : rangeEq e r (32 - (n + 1)) ↔
|
||||
(e.val[i.val]! = r.val[i.val]!) ∧ rangeEq e r (32 - n) := by
|
||||
have h32 : i.val < 32 := by clear * - hlt; scalar_tac
|
||||
constructor
|
||||
· intro h
|
||||
refine ⟨h i.val (by clear * - hiv; omega) h32, ?_⟩
|
||||
intro j hj1 hj2; exact h j (by omega) hj2
|
||||
· rintro ⟨hbyte, htail⟩ j hj1 hj2
|
||||
rcases Nat.lt_or_ge j (32 - n) with hj | hj
|
||||
· have hji : j = i.val := by clear * - hj1 hj hiv; omega
|
||||
rw [hji]; exact hbyte
|
||||
· exact htail j hj hj2
|
||||
have hda : (decide (e.val[i.val]! = r.val[i.val]!) && decide (rangeEq e r (32 - n)))
|
||||
= decide ((e.val[i.val]! = r.val[i.val]!) ∧ rangeEq e r (32 - n)) := by
|
||||
by_cases hp : (e.val[i.val]! = r.val[i.val]!) <;>
|
||||
by_cases hq : rangeEq e r (32 - n) <;> simp [hp, hq]
|
||||
rw [hda, decide_eq_decide]
|
||||
exact hiff.symm
|
||||
|
||||
/-- The comparison loop from the verifier's entry state (`b = true`,
|
||||
`i = 0`): the result equals the full 32-byte equality. -/
|
||||
theorem verify_loop_full (e r : Array Std.U8 32#usize) :
|
||||
ed_sigs.verification_key.VerificationKey.verify_sha512_loop r e true 0#usize
|
||||
⦃ res => res = decide (rangeEq e r 0) ⦄ := by
|
||||
have h := verify_loop_spec e r 32 true 0#usize (by scalar_tac) (le_refl _)
|
||||
apply spec_mono h
|
||||
intro res hres; rw [hres]; simp
|
||||
|
||||
/-! ### The apex: the EdDSA verification equation -/
|
||||
|
||||
open ed_sigs ed_sigs.verification_key in
|
||||
/-- **The EdDSA verification equation, SHA-512 opaque.** For a signature
|
||||
whose byte accessors are total (`hrb`, `hsb`), a key that passes the
|
||||
all-zero filter (`hA`), an `R` outside the legacy-excluded list
|
||||
(`hleg`), a canonical scalar `s < ℓ` (`hs`), and a total recomputation
|
||||
(`hrec`, `he`), the extracted solana-ed25519 dalek-style verifier
|
||||
accepts **iff** the recomputed compressed point equals the signature's
|
||||
`R`, byte-for-byte:
|
||||
verify_sha512 self sig msg = ok (Ok ()) ↔ e = R (all 32 bytes).
|
||||
|
||||
`er` (via `recompute_r_sha512`) is the PROVEN composition
|
||||
`compress( [k]·(−A) + [s]·B )` over the certified curve model; `k` is
|
||||
the scalar the SHA-512 oracle produces — the hash stays opaque, so this
|
||||
is exactly the honest EdDSA acceptance criterion (ZIP-215 legacy
|
||||
filters conditioned out by hypothesis). -/
|
||||
theorem verify_accepts_iff
|
||||
(self : verification_key.VerificationKey)
|
||||
(sig : ed25519.Signature) (msg : Slice Std.U8)
|
||||
(rb sb : Array Std.U8 32#usize) (s : scalar.Scalar)
|
||||
(er : edwards.CompressedEdwardsY) (e : Array Std.U8 32#usize)
|
||||
(hrb : ed25519.Signature.r_bytes sig = ok rb)
|
||||
(hsb : ed25519.Signature.s_bytes sig = ok sb)
|
||||
(hA : VerificationKey.a_bytes_nonzero self = ok true)
|
||||
(hleg : is_legacy_excluded_r rb = ok false)
|
||||
(hs : check_scalar_canonical sb = ok (core.result.Result.Ok s))
|
||||
(hrec : VerificationKey.recompute_r_sha512 self rb s msg = ok er)
|
||||
(he : edwards.CompressedEdwardsY.as_bytes er = ok e) :
|
||||
VerificationKey.verify_sha512 self sig msg = ok (core.result.Result.Ok ())
|
||||
↔ rangeEq e rb 0 := by
|
||||
unfold VerificationKey.verify_sha512
|
||||
rw [hrb]
|
||||
simp only [bind_tc_ok]
|
||||
rw [hsb]
|
||||
simp only [bind_tc_ok]
|
||||
rw [hA]
|
||||
simp only [bind_tc_ok, if_true]
|
||||
rw [hleg]
|
||||
simp only [bind_tc_ok, Bool.false_eq_true, if_false]
|
||||
rw [hs]
|
||||
simp only [bind_tc_ok]
|
||||
simp only [core.result.Result.Insts.CoreOpsTry_traitTry.branch, bind_tc_ok]
|
||||
rw [hrec]
|
||||
simp only [bind_tc_ok]
|
||||
rw [he]
|
||||
simp only [bind_tc_ok]
|
||||
have hloop := verify_loop_full e rb
|
||||
obtain ⟨v, hv, hpost⟩ := spec_imp_exists hloop
|
||||
rw [hv]
|
||||
simp only [bind_tc_ok]
|
||||
rw [hpost]
|
||||
by_cases hb : rangeEq e rb 0
|
||||
· rw [decide_eq_true hb, if_pos rfl]
|
||||
simp only [hb, iff_true]
|
||||
· rw [decide_eq_false hb, if_neg (by simp)]
|
||||
constructor
|
||||
· intro hcontra; simp_all
|
||||
· intro hc; exact absurd hc hb
|
||||
|
||||
end CurveFieldProofs
|
||||
|
|
@ -60,6 +60,7 @@ PROOFS=(
|
|||
DsmNafLoopSpec
|
||||
DsmNafSpec
|
||||
DsmMulSpec
|
||||
SigApexSpec
|
||||
)
|
||||
# Fully-qualified certificate names; each must be axiom-clean.
|
||||
CERTS=(
|
||||
|
|
@ -78,6 +79,7 @@ CERTS=(
|
|||
CurveFieldProofs.non_adjacent_form_spec
|
||||
CurveFieldProofs.run_basepoint
|
||||
CurveFieldProofs.vartime_double_base_mul_spec
|
||||
CurveFieldProofs.verify_loop_full
|
||||
)
|
||||
# Imports needed so every certificate in CERTS is in scope for the audit.
|
||||
AUDIT_IMPORTS=(
|
||||
|
|
@ -88,6 +90,7 @@ AUDIT_IMPORTS=(
|
|||
Proofs.DsmLoopSpec
|
||||
Proofs.DsmNafSpec
|
||||
Proofs.DsmMulSpec
|
||||
Proofs.SigApexSpec
|
||||
)
|
||||
|
||||
# ── Phase 0: resource + integrity guards ────────────────────────────────────
|
||||
|
|
@ -167,5 +170,29 @@ lake env bash -c "
|
|||
exit 1
|
||||
fi
|
||||
"
|
||||
echo "=== Phase 3b: signature-apex audit (SHA-512 + wire-format boundary) ==="
|
||||
# The verification-equation apex is grounded in the PROVEN curve model; its
|
||||
# only axioms beyond the standard three are the deliberate, documented
|
||||
# boundary: the SHA-512 hash oracle and the opaque wire-format types.
|
||||
# NO curve axioms, NO scalar axioms, NO backend-dispatch axioms.
|
||||
cd "$AENEAS_LEAN"
|
||||
lake env bash -c "
|
||||
set -euo pipefail
|
||||
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||
cd '$HERE'
|
||||
ALLOWED='[propext, Classical.choice, Quot.sound, ed25519.Signature, ed_sigs.sha512_hash3, ed25519.Signature.r_bytes, ed25519.Signature.s_bytes]'
|
||||
AUD=\$(mktemp '$HERE/.apex-XXXX.lean')
|
||||
{ echo 'import Proofs.SigApexSpec'; echo '#print axioms CurveFieldProofs.verify_accepts_iff'; } > \"\$AUD\"
|
||||
OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
|
||||
echo \"\$OUT\"
|
||||
rm -f \"\$AUD\"
|
||||
FLAT=\$(echo \"\$OUT\" | tr '\\n' ' ' | tr -s ' ')
|
||||
if echo \"\$FLAT\" | grep -qF \"depends on axioms: \$ALLOWED\"; then
|
||||
echo ' apex axiom cone = exactly the SHA-512 + wire-format boundary (no curve/scalar/backend axioms)'
|
||||
else
|
||||
echo 'APEX AUDIT FAILED: verify_accepts_iff cone is not the documented boundary'; exit 1
|
||||
fi
|
||||
"
|
||||
|
||||
echo ""
|
||||
echo "ALL PROOFS PASS. ALL CERTIFICATES AXIOM-CLEAN. NO DEAD FILES."
|
||||
|
|
|
|||
|
|
@ -23,8 +23,12 @@ source ~/aeneas-toolchain/env.sh
|
|||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
CRATE=~/GitClone/FormalVerification/sources/anza-cryptography-source/curve25519/solana-ed25519
|
||||
|
||||
echo "[1/2] charon: Rust -> LLBC (field + curve_models + edwards + scalar [MERGED GEN])"
|
||||
echo "[1/2] charon: Rust -> LLBC (field + curve_models + edwards + scalar + verify [MERGED GEN])"
|
||||
cd "$CRATE"
|
||||
# Pin the serial backend: the AVX2 dispatch arm compiles out, so backend
|
||||
# selection extracts as the real constant Serial (no dispatch axiom).
|
||||
export RUSTFLAGS='--cfg curve25519_serial_only'
|
||||
cargo clean -p solana-ed25519 2>/dev/null || true
|
||||
charon cargo --preset=aeneas \
|
||||
--start-from crate::field \
|
||||
--start-from crate::backend::serial::u64::field \
|
||||
|
|
@ -43,6 +47,9 @@ charon cargo --preset=aeneas \
|
|||
--start-from 'crate::backend::serial::u64::scalar::_::from_bytes_wide' \
|
||||
--start-from 'crate::scalar::_::from_bytes_mod_order' \
|
||||
--start-from 'crate::scalar::_::from_bytes_mod_order_wide' \
|
||||
--start-from 'crate::ed_sigs::verification_key::_::verify_sha512' \
|
||||
--opaque 'crate::ed_sigs::sha512_hash3' \
|
||||
--opaque 'ed25519' \
|
||||
--opaque 'crate::field::_::internal_invert_batch' \
|
||||
--opaque 'crate::backend::serial::scalar_mul::variable_base' \
|
||||
--opaque 'crate::backend::serial::scalar_mul::vartime_triple_base' \
|
||||
|
|
@ -51,7 +58,6 @@ charon cargo --preset=aeneas \
|
|||
--opaque 'crate::backend::serial::scalar_mul::precomputed_straus' \
|
||||
--opaque 'crate::backend::serial::scalar_mul::pippenger' \
|
||||
--opaque 'crate::backend::vector' \
|
||||
--opaque 'crate::backend::get_selected_backend' \
|
||||
--opaque 'crate::backend::scalar_fits_in_128_bits' \
|
||||
--opaque 'crate::edwards::decompress' \
|
||||
--opaque 'crate::edwards::_::sum' \
|
||||
|
|
|
|||
|
|
@ -3738,6 +3738,11 @@ def backend.serial.u64.scalar.Scalar52.from_montgomery
|
|||
{ start := 0#usize, «end» := 5#usize } self limbs
|
||||
backend.serial.u64.scalar.Scalar52.montgomery_reduce limbs1
|
||||
|
||||
/-- [curve25519::backend::get_selected_backend]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend.rs', lines 53:0-64:1 -/
|
||||
def backend.get_selected_backend : Result backend.BackendKind := do
|
||||
ok backend.BackendKind.Serial
|
||||
|
||||
/-- [curve25519::backend::variable_base_mul]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend.rs', lines 221:0-227:1
|
||||
Visibility: public -/
|
||||
|
|
@ -3745,12 +3750,8 @@ def backend.variable_base_mul
|
|||
(point : edwards.EdwardsPoint) (scalar : scalar.Scalar) :
|
||||
Result edwards.EdwardsPoint
|
||||
:= do
|
||||
let bk ← backend.get_selected_backend
|
||||
match bk with
|
||||
| backend.BackendKind.Avx2 =>
|
||||
backend.vector.scalar_mul.variable_base.spec_avx2.mul point scalar
|
||||
| backend.BackendKind.Serial =>
|
||||
backend.serial.scalar_mul.variable_base.mul point scalar
|
||||
let _ ← backend.get_selected_backend
|
||||
backend.serial.scalar_mul.variable_base.mul point scalar
|
||||
|
||||
/-- [curve25519::backend::vartime_double_base_mul]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend.rs', lines 231:0-237:1
|
||||
|
|
@ -3759,12 +3760,8 @@ def backend.vartime_double_base_mul
|
|||
(a : scalar.Scalar) (A : edwards.EdwardsPoint) (b : scalar.Scalar) :
|
||||
Result edwards.EdwardsPoint
|
||||
:= do
|
||||
let bk ← backend.get_selected_backend
|
||||
match bk with
|
||||
| backend.BackendKind.Avx2 =>
|
||||
backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul a A b
|
||||
| backend.BackendKind.Serial =>
|
||||
backend.serial.scalar_mul.vartime_double_base.mul a A b
|
||||
let _ ← backend.get_selected_backend
|
||||
backend.serial.scalar_mul.vartime_double_base.mul a A b
|
||||
|
||||
/-- [curve25519::edwards::{impl core::ops::arith::Add<&'a curve25519::edwards::EdwardsPoint, curve25519::edwards::EdwardsPoint> for &'_1 curve25519::edwards::EdwardsPoint}::add]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 785:4-787:5
|
||||
|
|
@ -3834,14 +3831,9 @@ def backend.vartime_triple_base_mul_128_128_256_prechecked
|
|||
(A2 : edwards.EdwardsPoint) (b : scalar.Scalar) :
|
||||
Result edwards.EdwardsPoint
|
||||
:= do
|
||||
let bk ← backend.get_selected_backend
|
||||
match bk with
|
||||
| backend.BackendKind.Avx2 =>
|
||||
backend.vector.scalar_mul.vartime_triple_base.spec_avx2.mul_128_128_256_prechecked
|
||||
a1 A1 a2 A2 b
|
||||
| backend.BackendKind.Serial =>
|
||||
backend.serial.scalar_mul.vartime_triple_base.mul_128_128_256_prechecked a1
|
||||
A1 a2 A2 b
|
||||
let _ ← backend.get_selected_backend
|
||||
backend.serial.scalar_mul.vartime_triple_base.mul_128_128_256_prechecked a1
|
||||
A1 a2 A2 b
|
||||
|
||||
/-- [curve25519::backend::vartime_triple_base_mul_128_128_256]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend.rs', lines 244:0-256:1
|
||||
|
|
@ -3898,6 +3890,519 @@ def constants.BASEPOINT_ORDER : scalar.Scalar :=
|
|||
])
|
||||
}
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::LEGACY_EXCLUDED_R_ENCODINGS]
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 50:0-106:2 -/
|
||||
@[global_simps, irreducible]
|
||||
def ed_sigs.verification_key.LEGACY_EXCLUDED_R_ENCODINGS
|
||||
: Array (Array Std.U8 32#usize) 11#usize :=
|
||||
let a := Array.repeat 32#usize 0#u8
|
||||
Array.make 11#usize [
|
||||
a,
|
||||
Array.make 32#usize [
|
||||
1#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, 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, 0#u8
|
||||
],
|
||||
Array.make 32#usize [
|
||||
38#u8, 232#u8, 149#u8, 143#u8, 194#u8, 178#u8, 39#u8, 176#u8, 69#u8,
|
||||
195#u8, 244#u8, 137#u8, 242#u8, 239#u8, 152#u8, 240#u8, 213#u8, 223#u8,
|
||||
172#u8, 5#u8, 211#u8, 198#u8, 51#u8, 57#u8, 177#u8, 56#u8, 2#u8, 136#u8,
|
||||
109#u8, 83#u8, 252#u8, 5#u8
|
||||
],
|
||||
Array.make 32#usize [
|
||||
199#u8, 23#u8, 106#u8, 112#u8, 61#u8, 77#u8, 216#u8, 79#u8, 186#u8,
|
||||
60#u8, 11#u8, 118#u8, 13#u8, 16#u8, 103#u8, 15#u8, 42#u8, 32#u8, 83#u8,
|
||||
250#u8, 44#u8, 57#u8, 204#u8, 198#u8, 78#u8, 199#u8, 253#u8, 119#u8,
|
||||
146#u8, 172#u8, 3#u8, 122#u8
|
||||
],
|
||||
Array.make 32#usize [
|
||||
19#u8, 232#u8, 149#u8, 143#u8, 194#u8, 178#u8, 39#u8, 176#u8, 69#u8,
|
||||
195#u8, 244#u8, 137#u8, 242#u8, 239#u8, 152#u8, 240#u8, 213#u8, 223#u8,
|
||||
172#u8, 5#u8, 211#u8, 198#u8, 51#u8, 57#u8, 177#u8, 56#u8, 2#u8, 136#u8,
|
||||
109#u8, 83#u8, 252#u8, 133#u8
|
||||
],
|
||||
Array.make 32#usize [
|
||||
180#u8, 23#u8, 106#u8, 112#u8, 61#u8, 77#u8, 216#u8, 79#u8, 186#u8,
|
||||
60#u8, 11#u8, 118#u8, 13#u8, 16#u8, 103#u8, 15#u8, 42#u8, 32#u8, 83#u8,
|
||||
250#u8, 44#u8, 57#u8, 204#u8, 198#u8, 78#u8, 199#u8, 253#u8, 119#u8,
|
||||
146#u8, 172#u8, 3#u8, 250#u8
|
||||
],
|
||||
Array.make 32#usize [
|
||||
236#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 127#u8
|
||||
],
|
||||
Array.make 32#usize [
|
||||
237#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 127#u8
|
||||
],
|
||||
Array.make 32#usize [
|
||||
238#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 127#u8
|
||||
],
|
||||
Array.make 32#usize [
|
||||
217#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8
|
||||
],
|
||||
Array.make 32#usize [
|
||||
218#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8, 255#u8,
|
||||
255#u8, 255#u8, 255#u8, 255#u8, 255#u8
|
||||
]
|
||||
]
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::pack]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 1331:4-1335:5 -/
|
||||
def scalar.Scalar52.pack
|
||||
(self : backend.serial.u64.scalar.Scalar52) : Result scalar.Scalar := do
|
||||
let a ← backend.serial.u64.scalar.Scalar52.to_bytes self
|
||||
ok { bytes := a }
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::scalar::Scalar}::unpack]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 1288:4-1290:5 -/
|
||||
def scalar.Scalar.unpack
|
||||
(self : scalar.Scalar) : Result backend.serial.u64.scalar.Scalar52 := do
|
||||
backend.serial.u64.scalar.Scalar52.from_bytes self.bytes
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::scalar::Scalar}::reduce]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 1303:4-1320:5 -/
|
||||
def scalar.Scalar.reduce (self : scalar.Scalar) : Result scalar.Scalar := do
|
||||
let x ← scalar.Scalar.unpack self
|
||||
let xR ←
|
||||
backend.serial.u64.scalar.Scalar52.mul_internal x
|
||||
backend.serial.u64.constants.R
|
||||
let x_mod_l ← backend.serial.u64.scalar.Scalar52.montgomery_reduce xR
|
||||
scalar.Scalar52.pack x_mod_l
|
||||
|
||||
/-- [curve25519::scalar::{impl core::ops::index::Index<usize, u8> for curve25519::scalar::Scalar}::index]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 290:4-292:5
|
||||
Visibility: public -/
|
||||
def scalar.Scalar.Insts.CoreOpsIndexIndexUsizeU8.index
|
||||
(self : scalar.Scalar) (_index : Std.Usize) : Result Std.U8 := do
|
||||
Array.index_usize self.bytes _index
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::scalar::Scalar}::from_bytes_mod_order]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 207:4-216:5
|
||||
Visibility: public -/
|
||||
def scalar.Scalar.from_bytes_mod_order
|
||||
(bytes : Array Std.U8 32#usize) : Result scalar.Scalar := do
|
||||
let s ← scalar.Scalar.reduce { bytes }
|
||||
let i ← scalar.Scalar.Insts.CoreOpsIndexIndexUsizeU8.index s 31#usize
|
||||
let right_val ← i >>> 7#i32
|
||||
massert (0#u8 = right_val)
|
||||
ok s
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::check_scalar_canonical::L_BYTES]
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 482:4-485:6 -/
|
||||
@[global_simps, irreducible]
|
||||
def ed_sigs.verification_key.check_scalar_canonical.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
|
||||
]
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::check_scalar_canonical]: loop body 0:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 490:4-501:5 -/
|
||||
@[rust_loop_body]
|
||||
def ed_sigs.verification_key.check_scalar_canonical_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
|
||||
ed_sigs.verification_key.check_scalar_canonical.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)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::check_scalar_canonical]: loop 0:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 490:4-501:5 -/
|
||||
@[rust_loop]
|
||||
def ed_sigs.verification_key.check_scalar_canonical_loop
|
||||
(bytes : Array Std.U8 32#usize) (lt : Bool) (decided : Bool) (i : Std.Usize)
|
||||
:
|
||||
Result Bool
|
||||
:= do
|
||||
loop
|
||||
(fun (lt1, decided1, i1) =>
|
||||
ed_sigs.verification_key.check_scalar_canonical_loop.body bytes lt1
|
||||
decided1 i1)
|
||||
(lt, decided, i)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::check_scalar_canonical]:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 480:0-507:1 -/
|
||||
def ed_sigs.verification_key.check_scalar_canonical
|
||||
(bytes : Array Std.U8 32#usize) :
|
||||
Result (core.result.Result scalar.Scalar ed_sigs.error.Error)
|
||||
:= do
|
||||
let lt ←
|
||||
ed_sigs.verification_key.check_scalar_canonical_loop bytes false false
|
||||
32#usize
|
||||
if lt
|
||||
then
|
||||
let s ← scalar.Scalar.from_bytes_mod_order bytes
|
||||
ok (core.result.Result.Ok s)
|
||||
else ok (core.result.Result.Err ed_sigs.error.Error.InvalidSignature)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::is_legacy_excluded_r]: loop body 1:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 516:8-521:9 -/
|
||||
@[rust_loop_body]
|
||||
def ed_sigs.verification_key.is_legacy_excluded_r_loop0_loop0.body
|
||||
(r : Array Std.U8 32#usize) (i : Std.Usize) (eq : Bool) (j : Std.Usize) :
|
||||
Result (ControlFlow (Bool × Std.Usize) Bool)
|
||||
:= do
|
||||
if j < 32#usize
|
||||
then
|
||||
let a ←
|
||||
Array.index_usize ed_sigs.verification_key.LEGACY_EXCLUDED_R_ENCODINGS i
|
||||
let i1 ← Array.index_usize a j
|
||||
let i2 ← Array.index_usize r j
|
||||
let eq1 ← if i1 != i2
|
||||
then ok false
|
||||
else ok eq
|
||||
let j1 ← j + 1#usize
|
||||
ok (cont (eq1, j1))
|
||||
else ok (done eq)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::is_legacy_excluded_r]: loop 1:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 516:8-521:9 -/
|
||||
@[rust_loop]
|
||||
def ed_sigs.verification_key.is_legacy_excluded_r_loop0_loop0
|
||||
(r : Array Std.U8 32#usize) (i : Std.Usize) (eq : Bool) (j : Std.Usize) :
|
||||
Result Bool
|
||||
:= do
|
||||
loop
|
||||
(fun (eq1, j1) =>
|
||||
ed_sigs.verification_key.is_legacy_excluded_r_loop0_loop0.body r i eq1
|
||||
j1)
|
||||
(eq, j)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::is_legacy_excluded_r]: loop body 0:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 513:4-526:5 -/
|
||||
@[rust_loop_body]
|
||||
def ed_sigs.verification_key.is_legacy_excluded_r_loop0.body
|
||||
(r : Array Std.U8 32#usize) (found : Bool) (i : Std.Usize) :
|
||||
Result (ControlFlow (Bool × Std.Usize) Bool)
|
||||
:= do
|
||||
if i < 11#usize
|
||||
then
|
||||
let eq ←
|
||||
ed_sigs.verification_key.is_legacy_excluded_r_loop0_loop0 r i true
|
||||
0#usize
|
||||
let found1 ← if eq
|
||||
then ok true
|
||||
else ok found
|
||||
let i1 ← i + 1#usize
|
||||
ok (cont (found1, i1))
|
||||
else ok (done found)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::is_legacy_excluded_r]: loop 0:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 513:4-526:5 -/
|
||||
@[rust_loop]
|
||||
def ed_sigs.verification_key.is_legacy_excluded_r_loop0
|
||||
(r : Array Std.U8 32#usize) (found : Bool) (i : Std.Usize) :
|
||||
Result Bool
|
||||
:= do
|
||||
loop
|
||||
(fun (found1, i1) =>
|
||||
ed_sigs.verification_key.is_legacy_excluded_r_loop0.body r found1 i1)
|
||||
(found, i)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::is_legacy_excluded_r]:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 510:0-528:1 -/
|
||||
@[reducible]
|
||||
def ed_sigs.verification_key.is_legacy_excluded_r
|
||||
(r : Array Std.U8 32#usize) : Result Bool := do
|
||||
ed_sigs.verification_key.is_legacy_excluded_r_loop0 r false 0#usize
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::{curve25519::ed_sigs::verification_key::VerificationKey}::a_bytes_nonzero]: loop body 0:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 535:8-540:9 -/
|
||||
@[rust_loop_body]
|
||||
def ed_sigs.verification_key.VerificationKey.a_bytes_nonzero_loop.body
|
||||
(self : ed_sigs.verification_key.VerificationKey) (nonzero : Bool)
|
||||
(i : Std.Usize) :
|
||||
Result (ControlFlow (Bool × Std.Usize) Bool)
|
||||
:= do
|
||||
if i < 32#usize
|
||||
then
|
||||
let a := self.A_bytes
|
||||
let i1 ← Array.index_usize a i
|
||||
let nonzero1 ← if i1 != 0#u8
|
||||
then ok true
|
||||
else ok nonzero
|
||||
let i2 ← i + 1#usize
|
||||
ok (cont (nonzero1, i2))
|
||||
else ok (done nonzero)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::{curve25519::ed_sigs::verification_key::VerificationKey}::a_bytes_nonzero]: loop 0:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 535:8-540:9 -/
|
||||
@[rust_loop]
|
||||
def ed_sigs.verification_key.VerificationKey.a_bytes_nonzero_loop
|
||||
(self : ed_sigs.verification_key.VerificationKey) (nonzero : Bool)
|
||||
(i : Std.Usize) :
|
||||
Result Bool
|
||||
:= do
|
||||
loop
|
||||
(fun (nonzero1, i1) =>
|
||||
ed_sigs.verification_key.VerificationKey.a_bytes_nonzero_loop.body self
|
||||
nonzero1 i1)
|
||||
(nonzero, i)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::{curve25519::ed_sigs::verification_key::VerificationKey}::a_bytes_nonzero]:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 532:4-542:5 -/
|
||||
@[reducible]
|
||||
def ed_sigs.verification_key.VerificationKey.a_bytes_nonzero
|
||||
(self : ed_sigs.verification_key.VerificationKey) : Result Bool := do
|
||||
ed_sigs.verification_key.VerificationKey.a_bytes_nonzero_loop self false
|
||||
0#usize
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::scalar::Scalar}::from_bytes_mod_order_wide]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 220:4-229:5
|
||||
Visibility: public -/
|
||||
def scalar.Scalar.from_bytes_mod_order_wide
|
||||
(input : Array Std.U8 64#usize) : Result scalar.Scalar := do
|
||||
let unpacked ← backend.serial.u64.scalar.Scalar52.from_bytes_wide input
|
||||
scalar.Scalar52.pack unpacked
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 1068:4-1074:5
|
||||
Visibility: public -/
|
||||
def edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint
|
||||
(a : scalar.Scalar) (A : edwards.EdwardsPoint) (b : scalar.Scalar) :
|
||||
Result edwards.EdwardsPoint
|
||||
:= do
|
||||
backend.vartime_double_base_mul a A b
|
||||
|
||||
/-- [curve25519::field::{curve25519::backend::serial::u64::field::FieldElement51}::pow22501]:
|
||||
Source: 'curve25519/solana-ed25519/src/field.rs', lines 159:4-193:5 -/
|
||||
def field.FieldElement51.pow22501
|
||||
(self : backend.serial.u64.field.FieldElement51) :
|
||||
Result (backend.serial.u64.field.FieldElement51 ×
|
||||
backend.serial.u64.field.FieldElement51)
|
||||
:= do
|
||||
let t0 ← backend.serial.u64.field.FieldElement51.square self
|
||||
let fe ← backend.serial.u64.field.FieldElement51.square t0
|
||||
let t1 ← backend.serial.u64.field.FieldElement51.square fe
|
||||
let t2 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
self t1
|
||||
let t3 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t0 t2
|
||||
let t4 ← backend.serial.u64.field.FieldElement51.square t3
|
||||
let t5 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t2 t4
|
||||
let t6 ← backend.serial.u64.field.FieldElement51.pow2k t5 5#u32
|
||||
let t7 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t6 t5
|
||||
let t8 ← backend.serial.u64.field.FieldElement51.pow2k t7 10#u32
|
||||
let t9 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t8 t7
|
||||
let t10 ← backend.serial.u64.field.FieldElement51.pow2k t9 20#u32
|
||||
let t11 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t10 t9
|
||||
let t12 ← backend.serial.u64.field.FieldElement51.pow2k t11 10#u32
|
||||
let t13 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t12 t7
|
||||
let t14 ← backend.serial.u64.field.FieldElement51.pow2k t13 50#u32
|
||||
let t15 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t14 t13
|
||||
let t16 ← backend.serial.u64.field.FieldElement51.pow2k t15 100#u32
|
||||
let t17 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t16 t15
|
||||
let t18 ← backend.serial.u64.field.FieldElement51.pow2k t17 50#u32
|
||||
let t19 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t18 t13
|
||||
ok (t19, t3)
|
||||
|
||||
/-- [curve25519::field::{curve25519::backend::serial::u64::field::FieldElement51}::invert]:
|
||||
Source: 'curve25519/solana-ed25519/src/field.rs', lines 280:4-289:5 -/
|
||||
def field.FieldElement51.invert
|
||||
(self : backend.serial.u64.field.FieldElement51) :
|
||||
Result backend.serial.u64.field.FieldElement51
|
||||
:= do
|
||||
let (t19, t3) ← field.FieldElement51.pow22501 self
|
||||
let t20 ← backend.serial.u64.field.FieldElement51.pow2k t19 5#u32
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t20 t3
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::EdwardsPoint}::to_affine]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 564:4-569:5 -/
|
||||
def edwards.EdwardsPoint.to_affine
|
||||
(self : edwards.EdwardsPoint) : Result edwards.affine.AffinePoint := do
|
||||
let recip ← field.FieldElement51.invert self.Z
|
||||
let x ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
self.X recip
|
||||
let y ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
self.Y recip
|
||||
ok { x, y }
|
||||
|
||||
/-- [curve25519::field::{curve25519::backend::serial::u64::field::FieldElement51}::is_negative]:
|
||||
Source: 'curve25519/solana-ed25519/src/field.rs', lines 139:4-142:5 -/
|
||||
def field.FieldElement51.is_negative
|
||||
(self : backend.serial.u64.field.FieldElement51) : Result subtle.Choice := do
|
||||
let bytes ← backend.serial.u64.field.FieldElement51.to_bytes self
|
||||
let i ← Array.index_usize bytes 0#usize
|
||||
let i1 ← lift (i &&& 1#u8)
|
||||
core.convert.IntoFrom.into subtle.Choice.Insts.CoreConvertFromU8 i1
|
||||
|
||||
/-- [curve25519::edwards::affine::{curve25519::edwards::affine::AffinePoint}::compress]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards/affine.rs', lines 71:4-75:5
|
||||
Visibility: public -/
|
||||
def edwards.affine.AffinePoint.compress
|
||||
(self : edwards.affine.AffinePoint) : Result edwards.CompressedEdwardsY := do
|
||||
let s ← backend.serial.u64.field.FieldElement51.to_bytes self.y
|
||||
let c ← field.FieldElement51.is_negative self.x
|
||||
let i ← subtle.Choice.unwrap_u8 c
|
||||
let i1 ← i <<< 7#i32
|
||||
let i2 ← Array.index_usize s 31#usize
|
||||
let i3 ← lift (i2 ^^^ i1)
|
||||
let s1 ← Array.update s 31#usize i3
|
||||
ok s1
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::EdwardsPoint}::compress]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 615:4-617:5
|
||||
Visibility: public -/
|
||||
def edwards.EdwardsPoint.compress
|
||||
(self : edwards.EdwardsPoint) : Result edwards.CompressedEdwardsY := do
|
||||
let ap ← edwards.EdwardsPoint.to_affine self
|
||||
edwards.affine.AffinePoint.compress ap
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::{curve25519::ed_sigs::verification_key::VerificationKey}::recompute_r_sha512]:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 546:4-558:5 -/
|
||||
def ed_sigs.verification_key.VerificationKey.recompute_r_sha512
|
||||
(self : ed_sigs.verification_key.VerificationKey)
|
||||
(r_bytes : Array Std.U8 32#usize) (s : scalar.Scalar) (msg : Slice Std.U8) :
|
||||
Result edwards.CompressedEdwardsY
|
||||
:= do
|
||||
let s1 ←
|
||||
core.array.Array.index (core.ops.index.IndexSlice
|
||||
(core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice
|
||||
Std.U8)) r_bytes ()
|
||||
let a := self.A_bytes
|
||||
let s2 ←
|
||||
core.array.Array.index (core.ops.index.IndexSlice
|
||||
(core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice
|
||||
Std.U8)) a ()
|
||||
let a1 ← ed_sigs.sha512_hash3 s1 s2 msg
|
||||
let k ← scalar.Scalar.from_bytes_mod_order_wide a1
|
||||
let ep ←
|
||||
edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint k self.minus_A s
|
||||
edwards.EdwardsPoint.compress ep
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::CompressedEdwardsY}::as_bytes]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 198:4-200:5
|
||||
Visibility: public -/
|
||||
def edwards.CompressedEdwardsY.as_bytes
|
||||
(self : edwards.CompressedEdwardsY) : Result (Array Std.U8 32#usize) := do
|
||||
ok self
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::{curve25519::ed_sigs::verification_key::VerificationKey}::verify_sha512]: loop body 0:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 581:8-586:9
|
||||
Visibility: public -/
|
||||
@[rust_loop_body]
|
||||
def ed_sigs.verification_key.VerificationKey.verify_sha512_loop.body
|
||||
(r_bytes : Array Std.U8 32#usize) (e : Array Std.U8 32#usize) (equal : Bool)
|
||||
(k : Std.Usize) :
|
||||
Result (ControlFlow (Bool × Std.Usize) Bool)
|
||||
:= do
|
||||
if k < 32#usize
|
||||
then
|
||||
let i ← Array.index_usize e k
|
||||
let i1 ← Array.index_usize r_bytes k
|
||||
let equal1 ← if i != i1
|
||||
then ok false
|
||||
else ok equal
|
||||
let k1 ← k + 1#usize
|
||||
ok (cont (equal1, k1))
|
||||
else ok (done equal)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::{curve25519::ed_sigs::verification_key::VerificationKey}::verify_sha512]: loop 0:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 581:8-586:9
|
||||
Visibility: public -/
|
||||
@[rust_loop]
|
||||
def ed_sigs.verification_key.VerificationKey.verify_sha512_loop
|
||||
(r_bytes : Array Std.U8 32#usize) (e : Array Std.U8 32#usize) (equal : Bool)
|
||||
(k : Std.Usize) :
|
||||
Result Bool
|
||||
:= do
|
||||
loop
|
||||
(fun (equal1, k1) =>
|
||||
ed_sigs.verification_key.VerificationKey.verify_sha512_loop.body r_bytes
|
||||
e equal1 k1)
|
||||
(equal, k)
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::{curve25519::ed_sigs::verification_key::VerificationKey}::verify_sha512]:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 563:4-592:5
|
||||
Visibility: public -/
|
||||
def ed_sigs.verification_key.VerificationKey.verify_sha512
|
||||
(self : ed_sigs.verification_key.VerificationKey) (sig : ed25519.Signature)
|
||||
(msg : Slice Std.U8) :
|
||||
Result (core.result.Result Unit ed_sigs.error.Error)
|
||||
:= do
|
||||
let r_bytes ← ed25519.Signature.r_bytes sig
|
||||
let s_bytes ← ed25519.Signature.s_bytes sig
|
||||
let b ← ed_sigs.verification_key.VerificationKey.a_bytes_nonzero self
|
||||
if b
|
||||
then
|
||||
let b1 ← ed_sigs.verification_key.is_legacy_excluded_r r_bytes
|
||||
if b1
|
||||
then ok (core.result.Result.Err ed_sigs.error.Error.InvalidSignature)
|
||||
else
|
||||
let r ← ed_sigs.verification_key.check_scalar_canonical s_bytes
|
||||
let cf ← core.result.Result.Insts.CoreOpsTry_traitTry.branch r
|
||||
match cf with
|
||||
| core.ops.control_flow.ControlFlow.Continue val =>
|
||||
let expected_r ←
|
||||
ed_sigs.verification_key.VerificationKey.recompute_r_sha512 self
|
||||
r_bytes val msg
|
||||
let e ← edwards.CompressedEdwardsY.as_bytes expected_r
|
||||
let equal ←
|
||||
ed_sigs.verification_key.VerificationKey.verify_sha512_loop r_bytes e
|
||||
true 0#usize
|
||||
if equal
|
||||
then ok (core.result.Result.Ok ())
|
||||
else ok (core.result.Result.Err ed_sigs.error.Error.InvalidSignature)
|
||||
| core.ops.control_flow.ControlFlow.Break residual =>
|
||||
core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
|
||||
Unit (core.convert.FromSame ed_sigs.error.Error) residual
|
||||
else ok (core.result.Result.Err ed_sigs.error.Error.InvalidSignature)
|
||||
|
||||
/-- [curve25519::edwards::affine::{impl core::clone::Clone for curve25519::edwards::affine::AffinePoint}::clone]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards/affine.rs', lines 11:15-11:20
|
||||
Visibility: public -/
|
||||
|
|
@ -4071,29 +4576,6 @@ def edwards.affine.AffinePoint.to_edwards
|
|||
let fe1 ← backend.serial.u64.field.FieldElement51.ONE
|
||||
ok { X := self.x, Y := self.y, Z := fe1, T := fe }
|
||||
|
||||
/-- [curve25519::field::{curve25519::backend::serial::u64::field::FieldElement51}::is_negative]:
|
||||
Source: 'curve25519/solana-ed25519/src/field.rs', lines 139:4-142:5 -/
|
||||
def field.FieldElement51.is_negative
|
||||
(self : backend.serial.u64.field.FieldElement51) : Result subtle.Choice := do
|
||||
let bytes ← backend.serial.u64.field.FieldElement51.to_bytes self
|
||||
let i ← Array.index_usize bytes 0#usize
|
||||
let i1 ← lift (i &&& 1#u8)
|
||||
core.convert.IntoFrom.into subtle.Choice.Insts.CoreConvertFromU8 i1
|
||||
|
||||
/-- [curve25519::edwards::affine::{curve25519::edwards::affine::AffinePoint}::compress]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards/affine.rs', lines 71:4-75:5
|
||||
Visibility: public -/
|
||||
def edwards.affine.AffinePoint.compress
|
||||
(self : edwards.affine.AffinePoint) : Result edwards.CompressedEdwardsY := do
|
||||
let s ← backend.serial.u64.field.FieldElement51.to_bytes self.y
|
||||
let c ← field.FieldElement51.is_negative self.x
|
||||
let i ← subtle.Choice.unwrap_u8 c
|
||||
let i1 ← i <<< 7#i32
|
||||
let i2 ← Array.index_usize s 31#usize
|
||||
let i3 ← lift (i2 ^^^ i1)
|
||||
let s1 ← Array.update s 31#usize i3
|
||||
ok s1
|
||||
|
||||
/-- [curve25519::edwards::{impl core::ops::arith::Mul<curve25519::scalar::Scalar, curve25519::edwards::EdwardsPoint> for curve25519::edwards::EdwardsPoint}::mul]:
|
||||
Source: 'curve25519/solana-ed25519/src/macros.rs', lines 107:12-109:13
|
||||
Visibility: public -/
|
||||
|
|
@ -4185,13 +4667,6 @@ def edwards.CompressedEdwardsY.Insts.CoreHashHash : core.hash.Hash
|
|||
edwards.CompressedEdwardsY.Insts.CoreHashHash.hash corehashHasherInst
|
||||
}
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::CompressedEdwardsY}::as_bytes]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 198:4-200:5
|
||||
Visibility: public -/
|
||||
def edwards.CompressedEdwardsY.as_bytes
|
||||
(self : edwards.CompressedEdwardsY) : Result (Array Std.U8 32#usize) := do
|
||||
ok self
|
||||
|
||||
/-- [curve25519::edwards::{impl subtle::ConstantTimeEq for curve25519::edwards::CompressedEdwardsY}::ct_eq]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 178:4-180:5
|
||||
Visibility: public -/
|
||||
|
|
@ -4535,67 +5010,6 @@ def edwards.EdwardsPoint.Insts.CoreCmpEq : core.cmp.Eq edwards.EdwardsPoint
|
|||
edwards.EdwardsPoint.Insts.CoreCmpEq.assert_fields_are_eq
|
||||
}
|
||||
|
||||
/-- [curve25519::field::{curve25519::backend::serial::u64::field::FieldElement51}::pow22501]:
|
||||
Source: 'curve25519/solana-ed25519/src/field.rs', lines 159:4-193:5 -/
|
||||
def field.FieldElement51.pow22501
|
||||
(self : backend.serial.u64.field.FieldElement51) :
|
||||
Result (backend.serial.u64.field.FieldElement51 ×
|
||||
backend.serial.u64.field.FieldElement51)
|
||||
:= do
|
||||
let t0 ← backend.serial.u64.field.FieldElement51.square self
|
||||
let fe ← backend.serial.u64.field.FieldElement51.square t0
|
||||
let t1 ← backend.serial.u64.field.FieldElement51.square fe
|
||||
let t2 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
self t1
|
||||
let t3 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t0 t2
|
||||
let t4 ← backend.serial.u64.field.FieldElement51.square t3
|
||||
let t5 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t2 t4
|
||||
let t6 ← backend.serial.u64.field.FieldElement51.pow2k t5 5#u32
|
||||
let t7 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t6 t5
|
||||
let t8 ← backend.serial.u64.field.FieldElement51.pow2k t7 10#u32
|
||||
let t9 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t8 t7
|
||||
let t10 ← backend.serial.u64.field.FieldElement51.pow2k t9 20#u32
|
||||
let t11 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t10 t9
|
||||
let t12 ← backend.serial.u64.field.FieldElement51.pow2k t11 10#u32
|
||||
let t13 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t12 t7
|
||||
let t14 ← backend.serial.u64.field.FieldElement51.pow2k t13 50#u32
|
||||
let t15 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t14 t13
|
||||
let t16 ← backend.serial.u64.field.FieldElement51.pow2k t15 100#u32
|
||||
let t17 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t16 t15
|
||||
let t18 ← backend.serial.u64.field.FieldElement51.pow2k t17 50#u32
|
||||
let t19 ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t18 t13
|
||||
ok (t19, t3)
|
||||
|
||||
/-- [curve25519::field::{curve25519::backend::serial::u64::field::FieldElement51}::invert]:
|
||||
Source: 'curve25519/solana-ed25519/src/field.rs', lines 280:4-289:5 -/
|
||||
def field.FieldElement51.invert
|
||||
(self : backend.serial.u64.field.FieldElement51) :
|
||||
Result backend.serial.u64.field.FieldElement51
|
||||
:= do
|
||||
let (t19, t3) ← field.FieldElement51.pow22501 self
|
||||
let t20 ← backend.serial.u64.field.FieldElement51.pow2k t19 5#u32
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
t20 t3
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::EdwardsPoint}::as_affine_niels]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 551:4-561:5 -/
|
||||
def edwards.EdwardsPoint.as_affine_niels
|
||||
|
|
@ -4624,19 +5038,6 @@ def edwards.EdwardsPoint.as_affine_niels
|
|||
y x
|
||||
ok { y_plus_x := fe2, y_minus_x := fe3, xy2d }
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::EdwardsPoint}::to_affine]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 564:4-569:5 -/
|
||||
def edwards.EdwardsPoint.to_affine
|
||||
(self : edwards.EdwardsPoint) : Result edwards.affine.AffinePoint := do
|
||||
let recip ← field.FieldElement51.invert self.Z
|
||||
let x ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
self.X recip
|
||||
let y ←
|
||||
Shared0FieldElement51.Insts.CoreOpsArithMulSharedAFieldElement51FieldElement51.mul
|
||||
self.Y recip
|
||||
ok { x, y }
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::EdwardsPoint}::to_montgomery]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 580:4-590:5
|
||||
Visibility: public -/
|
||||
|
|
@ -4655,14 +5056,6 @@ def edwards.EdwardsPoint.to_montgomery
|
|||
let a ← backend.serial.u64.field.FieldElement51.to_bytes u
|
||||
ok a
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::EdwardsPoint}::compress]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 615:4-617:5
|
||||
Visibility: public -/
|
||||
def edwards.EdwardsPoint.compress
|
||||
(self : edwards.EdwardsPoint) : Result edwards.CompressedEdwardsY := do
|
||||
let ap ← edwards.EdwardsPoint.to_affine self
|
||||
edwards.affine.AffinePoint.compress ap
|
||||
|
||||
/-- Trait implementation: [curve25519::edwards::{impl core::ops::arith::Add<&'a curve25519::edwards::EdwardsPoint, curve25519::edwards::EdwardsPoint> for &'_1 curve25519::edwards::EdwardsPoint}]
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 783:0-788:1 -/
|
||||
@[reducible]
|
||||
|
|
@ -4865,15 +5258,6 @@ def edwards.EdwardsPoint.mul_base_clamped
|
|||
let a ← scalar.clamp_integer bytes
|
||||
edwards.EdwardsPoint.mul_base { bytes := a }
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::EdwardsPoint}::vartime_double_scalar_mul_basepoint]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 1068:4-1074:5
|
||||
Visibility: public -/
|
||||
def edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint
|
||||
(a : scalar.Scalar) (A : edwards.EdwardsPoint) (b : scalar.Scalar) :
|
||||
Result edwards.EdwardsPoint
|
||||
:= do
|
||||
backend.vartime_double_base_mul a A b
|
||||
|
||||
/-- [curve25519::edwards::{curve25519::edwards::EdwardsPoint}::vartime_triple_scalar_mul_basepoint]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards.rs', lines 1099:4-1107:5
|
||||
Visibility: public -/
|
||||
|
|
@ -5398,53 +5782,4 @@ def edwards.EdwardsPoint.Insts.CoreOpsArithMulAssignScalar :
|
|||
edwards.EdwardsPoint.Insts.CoreOpsArithMulAssignScalar.mul_assign
|
||||
}
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::backend::serial::u64::scalar::Scalar52}::pack]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 1331:4-1335:5 -/
|
||||
def scalar.Scalar52.pack
|
||||
(self : backend.serial.u64.scalar.Scalar52) : Result scalar.Scalar := do
|
||||
let a ← backend.serial.u64.scalar.Scalar52.to_bytes self
|
||||
ok { bytes := a }
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::scalar::Scalar}::unpack]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 1288:4-1290:5 -/
|
||||
def scalar.Scalar.unpack
|
||||
(self : scalar.Scalar) : Result backend.serial.u64.scalar.Scalar52 := do
|
||||
backend.serial.u64.scalar.Scalar52.from_bytes self.bytes
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::scalar::Scalar}::reduce]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 1303:4-1320:5 -/
|
||||
def scalar.Scalar.reduce (self : scalar.Scalar) : Result scalar.Scalar := do
|
||||
let x ← scalar.Scalar.unpack self
|
||||
let xR ←
|
||||
backend.serial.u64.scalar.Scalar52.mul_internal x
|
||||
backend.serial.u64.constants.R
|
||||
let x_mod_l ← backend.serial.u64.scalar.Scalar52.montgomery_reduce xR
|
||||
scalar.Scalar52.pack x_mod_l
|
||||
|
||||
/-- [curve25519::scalar::{impl core::ops::index::Index<usize, u8> for curve25519::scalar::Scalar}::index]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 290:4-292:5
|
||||
Visibility: public -/
|
||||
def scalar.Scalar.Insts.CoreOpsIndexIndexUsizeU8.index
|
||||
(self : scalar.Scalar) (_index : Std.Usize) : Result Std.U8 := do
|
||||
Array.index_usize self.bytes _index
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::scalar::Scalar}::from_bytes_mod_order]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 207:4-216:5
|
||||
Visibility: public -/
|
||||
def scalar.Scalar.from_bytes_mod_order
|
||||
(bytes : Array Std.U8 32#usize) : Result scalar.Scalar := do
|
||||
let s ← scalar.Scalar.reduce { bytes }
|
||||
let i ← scalar.Scalar.Insts.CoreOpsIndexIndexUsizeU8.index s 31#usize
|
||||
let right_val ← i >>> 7#i32
|
||||
massert (0#u8 = right_val)
|
||||
ok s
|
||||
|
||||
/-- [curve25519::scalar::{curve25519::scalar::Scalar}::from_bytes_mod_order_wide]:
|
||||
Source: 'curve25519/solana-ed25519/src/scalar.rs', lines 220:4-229:5
|
||||
Visibility: public -/
|
||||
def scalar.Scalar.from_bytes_mod_order_wide
|
||||
(input : Array Std.U8 64#usize) : Result scalar.Scalar := do
|
||||
let unpacked ← backend.serial.u64.scalar.Scalar52.from_bytes_wide input
|
||||
scalar.Scalar52.pack unpacked
|
||||
|
||||
end curve25519
|
||||
|
|
|
|||
|
|
@ -121,27 +121,29 @@ def core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index
|
|||
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]
|
||||
|
||||
AXIOM: raw-pointer API, never called by the extracted field code. -/
|
||||
MODEL (faithful): Rust body for `RangeFull` is `slice` — the pointer
|
||||
unchanged (identity). -/
|
||||
@[rust_fun
|
||||
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get_unchecked_mut"]
|
||||
axiom
|
||||
def
|
||||
core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked_mut
|
||||
{T : Type} :
|
||||
core.ops.range.RangeFull → MutRawPtr (Slice T) → Result (MutRawPtr (Slice
|
||||
T))
|
||||
{T : Type} (_ : core.ops.range.RangeFull) (p : MutRawPtr (Slice T)) :
|
||||
Result (MutRawPtr (Slice T)) :=
|
||||
ok p
|
||||
|
||||
/-- [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]
|
||||
|
||||
AXIOM: raw-pointer API, never called by the extracted field code. -/
|
||||
MODEL (faithful): Rust body for `RangeFull` is `slice` — the pointer
|
||||
unchanged (identity). -/
|
||||
@[rust_fun
|
||||
"core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>}::get_unchecked"]
|
||||
axiom
|
||||
def
|
||||
core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked
|
||||
{T : Type} :
|
||||
core.ops.range.RangeFull → ConstRawPtr (Slice T) → Result (ConstRawPtr
|
||||
(Slice T))
|
||||
{T : Type} (_ : core.ops.range.RangeFull) (p : ConstRawPtr (Slice T)) :
|
||||
Result (ConstRawPtr (Slice T)) :=
|
||||
ok p
|
||||
|
||||
/-- [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
|
||||
|
|
@ -171,9 +173,12 @@ def core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
|
|||
/-- [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 -/
|
||||
Visibility: public
|
||||
|
||||
MODEL (faithful): Rust body is `self.0`; `Choice` is the transparent
|
||||
`u8` newtype model (TypesExternal), so this is the identity. -/
|
||||
@[rust_fun "subtle::{subtle::Choice}::unwrap_u8"]
|
||||
axiom subtle.Choice.unwrap_u8 : subtle.Choice → Result Std.U8
|
||||
def subtle.Choice.unwrap_u8 (c : subtle.Choice) : Result Std.U8 := ok c
|
||||
|
||||
/-- [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
|
||||
|
|
@ -359,10 +364,6 @@ axiom
|
|||
scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar →
|
||||
edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
|
||||
|
||||
/-- [curve25519::backend::get_selected_backend]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend.rs', lines 53:0-64:1 -/
|
||||
axiom backend.get_selected_backend : Result backend.BackendKind
|
||||
|
||||
/-- [curve25519::backend::scalar_fits_in_128_bits]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend.rs', lines 283:0-285:1 -/
|
||||
axiom backend.scalar_fits_in_128_bits : scalar.Scalar → Result Bool
|
||||
|
|
@ -474,3 +475,52 @@ axiom field.FieldElement51.internal_invert_batch
|
|||
backend.serial.u64.field.FieldElement51 → Result ((Slice
|
||||
backend.serial.u64.field.FieldElement51) × (Slice
|
||||
backend.serial.u64.field.FieldElement51))
|
||||
|
||||
/-! ### Signature-layer externals.
|
||||
|
||||
Real definitions for the `?`-operator plumbing, and the documented
|
||||
signature-apex boundary: the SHA-512 oracle plus the foreign
|
||||
`ed25519::Signature` wire-format accessors. Everything else on the
|
||||
verify path — including the `Error` enum and backend selection — is
|
||||
real extracted code. -/
|
||||
|
||||
/-- `Try::branch` for `core::result::Result` — the `?` operator's dispatch. -/
|
||||
def core.result.Result.Insts.CoreOpsTry_traitTry.branch
|
||||
{T : Type} {E : Type} (r : core.result.Result T E) :
|
||||
Result (core.ops.control_flow.ControlFlow
|
||||
(core.result.Result core.convert.Infallible E) T) :=
|
||||
match r with
|
||||
| .Ok v => ok (.Continue v)
|
||||
| .Err e => ok (.Break (.Err e))
|
||||
|
||||
/-- `FromResidual` for `core::result::Result` — the `?` operator's error
|
||||
conversion. The `Ok Infallible` branch is uninhabited. -/
|
||||
def core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
|
||||
(T : Type) {E : Type} {F : Type} (convertFromInst : core.convert.From F E)
|
||||
(r : core.result.Result core.convert.Infallible E) :
|
||||
Result (core.result.Result T F) :=
|
||||
match r with
|
||||
| .Ok v => nomatch v
|
||||
| .Err e => do
|
||||
let f ← convertFromInst.from_ e
|
||||
ok (.Err f)
|
||||
|
||||
/-- [ed25519::{ed25519::Signature}::r_bytes]: opaque wire-format accessor
|
||||
on the foreign `ed25519::Signature` type (apex boundary). -/
|
||||
@[rust_fun "ed25519::{ed25519::Signature}::r_bytes"]
|
||||
axiom ed25519.Signature.r_bytes
|
||||
: ed25519.Signature → Result (Array Std.U8 32#usize)
|
||||
|
||||
/-- [ed25519::{ed25519::Signature}::s_bytes]: opaque wire-format accessor
|
||||
on the foreign `ed25519::Signature` type (apex boundary). -/
|
||||
@[rust_fun "ed25519::{ed25519::Signature}::s_bytes"]
|
||||
axiom ed25519.Signature.s_bytes
|
||||
: ed25519.Signature → Result (Array Std.U8 32#usize)
|
||||
|
||||
/-- [curve25519::ed_sigs::sha512_hash3]: THE SHA-512 ORACLE — the single
|
||||
opaque hash call of the verified verification path; semantically
|
||||
`Sha512(r || a || m)` (apex boundary). -/
|
||||
axiom ed_sigs.sha512_hash3
|
||||
:
|
||||
Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result (Array Std.U8
|
||||
64#usize)
|
||||
|
|
|
|||
|
|
@ -80,6 +80,29 @@ axiom U32.Insts.CoreIterRangeStep.forward_checked
|
|||
axiom U32.Insts.CoreIterRangeStep.steps_between
|
||||
: Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize))
|
||||
|
||||
/-- [core::result::{impl core::ops::try_trait::Try for core::result::Result<T, E>}::branch]:
|
||||
Source: '/rustc/library/core/src/result.rs', lines 2177:4-2177:64
|
||||
Name pattern: [core::result::{core::ops::try_trait::Try<core::result::Result<@T, @E>>}::branch]
|
||||
Visibility: public -/
|
||||
@[rust_fun
|
||||
"core::result::{core::ops::try_trait::Try<core::result::Result<@T, @E>>}::branch"]
|
||||
axiom core.result.Result.Insts.CoreOpsTry_traitTry.branch
|
||||
{T : Type} {E : Type} :
|
||||
core.result.Result T E → Result (core.ops.control_flow.ControlFlow
|
||||
(core.result.Result core.convert.Infallible E) T)
|
||||
|
||||
/-- [core::result::{impl core::ops::try_trait::FromResidual<core::result::Result<core::convert::Infallible, E>> for core::result::Result<T, F>}::from_residual]:
|
||||
Source: '/rustc/library/core/src/result.rs', lines 2192:4-2192:70
|
||||
Name pattern: [core::result::{core::ops::try_trait::FromResidual<core::result::Result<@T, @F>, core::result::Result<core::convert::Infallible, @E>>}::from_residual]
|
||||
Visibility: public -/
|
||||
@[rust_fun
|
||||
"core::result::{core::ops::try_trait::FromResidual<core::result::Result<@T, @F>, core::result::Result<core::convert::Infallible, @E>>}::from_residual"]
|
||||
axiom
|
||||
core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual
|
||||
(T : Type) {E : Type} {F : Type} (convertFromInst : core.convert.From F E) :
|
||||
core.result.Result core.convert.Infallible E → Result (core.result.Result T
|
||||
F)
|
||||
|
||||
/-- [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]
|
||||
|
|
@ -146,6 +169,22 @@ axiom core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
|
|||
{T : Type} :
|
||||
core.ops.range.RangeFull → Slice T → Result (Option (Slice T))
|
||||
|
||||
/-- [ed25519::{ed25519::Signature}::r_bytes]:
|
||||
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ed25519-2.2.3/src/lib.rs', lines 341:4-341:44
|
||||
Name pattern: [ed25519::{ed25519::Signature}::r_bytes]
|
||||
Visibility: public -/
|
||||
@[rust_fun "ed25519::{ed25519::Signature}::r_bytes"]
|
||||
axiom ed25519.Signature.r_bytes
|
||||
: ed25519.Signature → Result (Array Std.U8 32#usize)
|
||||
|
||||
/-- [ed25519::{ed25519::Signature}::s_bytes]:
|
||||
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ed25519-2.2.3/src/lib.rs', lines 346:4-346:44
|
||||
Name pattern: [ed25519::{ed25519::Signature}::s_bytes]
|
||||
Visibility: public -/
|
||||
@[rust_fun "ed25519::{ed25519::Signature}::s_bytes"]
|
||||
axiom ed25519.Signature.s_bytes
|
||||
: ed25519.Signature → Result (Array Std.U8 32#usize)
|
||||
|
||||
/-- [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]
|
||||
|
|
@ -283,36 +322,17 @@ axiom backend.serial.scalar_mul.vartime_triple_base.mul_128_128_256_prechecked
|
|||
scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar →
|
||||
edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
|
||||
|
||||
/-- [curve25519::backend::vector::scalar_mul::variable_base::spec_avx2::mul]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-3:68
|
||||
Visibility: public -/
|
||||
axiom backend.vector.scalar_mul.variable_base.spec_avx2.mul
|
||||
: edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
|
||||
|
||||
/-- [curve25519::backend::vector::scalar_mul::vartime_double_base::spec_avx2::mul]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend/vector/scalar_mul/vartime_double_base.rs', lines 14:0-14:68
|
||||
Visibility: public -/
|
||||
axiom backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul
|
||||
:
|
||||
scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result
|
||||
edwards.EdwardsPoint
|
||||
|
||||
/-- [curve25519::backend::vector::scalar_mul::vartime_triple_base::spec_avx2::mul_128_128_256_prechecked]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend/vector/scalar_mul/vartime_triple_base.rs', lines 10:0-10:68 -/
|
||||
axiom
|
||||
backend.vector.scalar_mul.vartime_triple_base.spec_avx2.mul_128_128_256_prechecked
|
||||
:
|
||||
scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar →
|
||||
edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
|
||||
|
||||
/-- [curve25519::backend::get_selected_backend]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend.rs', lines 53:0-64:1 -/
|
||||
axiom backend.get_selected_backend : Result backend.BackendKind
|
||||
|
||||
/-- [curve25519::backend::scalar_fits_in_128_bits]:
|
||||
Source: 'curve25519/solana-ed25519/src/backend.rs', lines 283:0-285:1 -/
|
||||
axiom backend.scalar_fits_in_128_bits : scalar.Scalar → Result Bool
|
||||
|
||||
/-- [curve25519::ed_sigs::sha512_hash3]:
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs.rs', lines 45:0-54:1 -/
|
||||
axiom ed_sigs.sha512_hash3
|
||||
:
|
||||
Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result (Array Std.U8
|
||||
64#usize)
|
||||
|
||||
/-- [curve25519::edwards::affine::{impl subtle::ConditionallySelectable for curve25519::edwards::affine::AffinePoint}::conditional_swap]:
|
||||
Source: 'curve25519/solana-ed25519/src/edwards/affine.rs', lines 23:0-30:1
|
||||
Visibility: public -/
|
||||
|
|
|
|||
|
|
@ -190,9 +190,31 @@ def backend.serial.u64.scalar.Scalar52 := Array Std.U64 5#usize
|
|||
Source: 'curve25519/solana-ed25519/src/backend.rs', lines 46:0-50:1 -/
|
||||
@[discriminant isize]
|
||||
inductive backend.BackendKind where
|
||||
| Avx2 : backend.BackendKind
|
||||
| Serial : backend.BackendKind
|
||||
|
||||
/-- [curve25519::ed_sigs::error::Error]
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/error.rs', lines 5:0-14:1
|
||||
Visibility: public -/
|
||||
@[discriminant isize]
|
||||
inductive ed_sigs.error.Error where
|
||||
| MalformedSecretKey : ed_sigs.error.Error
|
||||
| MalformedPublicKey : ed_sigs.error.Error
|
||||
| InvalidSignature : ed_sigs.error.Error
|
||||
| InvalidSliceLength : ed_sigs.error.Error
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::VerificationKeyBytes]
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 129:0-129:74
|
||||
Visibility: public -/
|
||||
@[reducible]
|
||||
def ed_sigs.verification_key.VerificationKeyBytes := Array Std.U8 32#usize
|
||||
|
||||
/-- [curve25519::ed_sigs::verification_key::VerificationKey]
|
||||
Source: 'curve25519/solana-ed25519/src/ed_sigs/verification_key.rs', lines 223:0-226:1
|
||||
Visibility: public -/
|
||||
structure ed_sigs.verification_key.VerificationKey where
|
||||
A_bytes : ed_sigs.verification_key.VerificationKeyBytes
|
||||
minus_A : edwards.EdwardsPoint
|
||||
|
||||
/-- [curve25519::edwards::affine::AffinePoint]
|
||||
Source: 'curve25519/solana-ed25519/src/edwards/affine.rs', lines 12:0-15:1
|
||||
Visibility: public -/
|
||||
|
|
|
|||
|
|
@ -22,3 +22,9 @@ set_option maxRecDepth 2048
|
|||
identity, so we model the type as `U8` directly. -/
|
||||
@[reducible, rust_type "subtle::Choice"]
|
||||
def subtle.Choice : Type := Std.U8
|
||||
|
||||
/-- [ed25519::Signature]: the foreign wire-format signature type — opaque
|
||||
(apex boundary); its two byte accessors are axiomatized in
|
||||
FunsExternal.lean. -/
|
||||
@[rust_type "ed25519::Signature"]
|
||||
axiom ed25519.Signature : Type
|
||||
|
|
|
|||
|
|
@ -13,6 +13,13 @@ set_option maxHeartbeats 1000000
|
|||
/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
|
||||
set_option maxRecDepth 2048
|
||||
|
||||
/-- [ed25519::Signature]
|
||||
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ed25519-2.2.3/src/lib.rs', lines 303:0-303:20
|
||||
Name pattern: [ed25519::Signature]
|
||||
Visibility: public -/
|
||||
@[rust_type "ed25519::Signature"]
|
||||
axiom ed25519.Signature : Type
|
||||
|
||||
/-- [subtle::Choice]
|
||||
Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 120:0-120:17
|
||||
Name pattern: [subtle::Choice]
|
||||
|
|
|
|||
Loading…
Reference in a new issue