saymrwulf/risc0-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/risc0-ed25519-verified.git synced 2026-09-07 20:30:43 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

coherence pass 1: TRUSTED-BASE scalar notes + both check-button docs

Browse source 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-02 23:58:31 +02:00
parent 6fe31be80d
commit 661e8c4c8f
2 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
README.md
View file

@ -58,6 +58,14 @@ cd verification
./check.sh # compiles EVERY shipped file + axiom-audits EVERY certificate ./check.sh # compiles EVERY shipped file + axiom-audits EVERY certificate
``` ```
The scalar layer has its own pair of buttons:
```bash
./extract-scalar.sh # regenerates gen/CurveScalar (Scalar52 limb arithmetic)
./check-scalar.sh # compiles the scalar gen + the proven scalar foundation
```
## Trusted base ## Trusted base
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

9
TRUSTED-BASE.md
View file

@ -20,6 +20,13 @@ running Rust code. Everything else is machine-checked.
certificate has the shape "IF the hash model computes SHA-512, THEN an certificate has the shape "IF the hash model computes SHA-512, THEN an
accepted signature satisfies the EdDSA verification equation". The hash accepted signature satisfies the EdDSA verification equation". The hash
implementation itself is NOT verified. implementation itself is NOT verified.
6. **Compilation of Rust to machine code** (rustc backend) is out of scope, 6. **`Scalar52::sub::black_box` (scalar layer)**: this fork's v4.1.3 code
implements the constant-time conditional via a local `black_box` =
`unsafe { core::ptr::read_volatile(&value) }`. The volatile read is an
optimization fence whose VALUE semantics is the identity; it is modeled as
`id` in `gen/CurveScalar/FunsExternal.lean`. (Upstream v5 uses `subtle`
here; betrusted v4.1.2 uses a pure arithmetic mask — each fork is verified
against its own strategy.)
7. **Compilation of Rust to machine code** (rustc backend) is out of scope,
as is side-channel behaviour (timing, speculation). The proofs are about as is side-channel behaviour (timing, speculation). The proofs are about
functional correctness at the MIR/LLBC level. functional correctness at the MIR/LLBC level.