saymrwulf/betrusted-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/betrusted-ed25519-verified.git synced 2026-09-03 20:13:47 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: saymrwulf:7b9ef53e488b739ba09a8caf5c2efc3f575db8cc
Branches Tags
saymrwulf:main
...
compare: saymrwulf:81f614a3cbd26412c6af7f0a31c0f128121fbfa4
Branches Tags
saymrwulf:main

No commits in common. "7b9ef53e488b739ba09a8caf5c2efc3f575db8cc" and "81f614a3cbd26412c6af7f0a31c0f128121fbfa4" have entirely different histories.
7b9ef53e48 ... 81f614a3cb

1 changed files with 8 additions and 0 deletions
Show stats Expand all files Collapse all files

8
README.md
View file

@ -122,3 +122,11 @@ scalar + the verify path's reachable code), regenerated in full by
See [TRUSTED-BASE.md](TRUSTED-BASE.md) for the complete list of assumptions See [TRUSTED-BASE.md](TRUSTED-BASE.md) for the complete list of assumptions
(Lean kernel, mathlib, Charon/Aeneas semantics, external-function models, (Lean kernel, mathlib, Charon/Aeneas semantics, external-function models,
and — in the signature layer only — an opaque SHA-512 model). and — in the signature layer only — an opaque SHA-512 model).
## Provenance
Proof engineering in this repository builds on the verification methodology
and proof architecture of
[PlanetMacro/ed25519-verificationtest](https://github.com/PlanetMacro/ed25519-verificationtest)
(the reference solution). All proofs here are checked against **this fork's
own extracted code**; nothing is claimed that the check script does not compile.