Patched source for Aeneas/Charon formal verification transpilation
Find a file
mrwulf 0cf451c896 Aeneas-compat: mask the bare shift in Scalar52::from_bytes_wide
hi[4] = words[7] >> 20  is the only shift in the function whose result is
stored without a trailing mask/or; at the pinned Aeneas (bf13c42e) a bare
`x >> c` as a full RHS extracts ill-typed (wrapping_shr applied to an i32
with an emitted-but-unsubstituted U32 cast). Masking is a semantic no-op:
words[7] >> 20 < 2^44 < 2^52.  Semantics unchanged; needed to bring
from_bytes_wide (the hash-to-scalar reduction) into verification scope.
2026-07-03 22:40:00 +02:00
.github chore: remove upstream CI workflows (not our CI infrastructure) 2026-06-30 17:44:29 +02:00
curve25519 Aeneas-compat: mask the bare shift in Scalar52::from_bytes_wide 2026-07-03 22:40:00 +02:00
experimental/ed25519-pokos Add workspace.package information and do minor clean-up (#14) 2026-04-26 10:11:05 +09:00
scripts [chore] ci for crate release (#7) 2026-04-15 08:44:33 -04:00
secp256r1 impl secp256r1 (#45) 2026-06-17 09:45:41 -04:00
syscall [solana-bn254-syscall] Add solana-bn254-syscall crate (#13) 2026-05-19 08:56:06 +09:00
.gitattributes Skeleton for cryptography repo (#1) 2026-03-07 15:52:28 -05:00
.gitignore Skeleton for cryptography repo (#1) 2026-03-07 15:52:28 -05:00
Cargo.lock impl secp256r1 (#45) 2026-06-17 09:45:41 -04:00
Cargo.toml impl secp256r1 (#45) 2026-06-17 09:45:41 -04:00