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
10 commits 1 branch 0 tags 6 MiB
Commit graph

5 commits

Author SHA1 Message Date
saymrwulf
5f785a75a3 coherence pass 2: restore the one-button property, institutionalize audits 
- check.sh: proofs memory default 6144 -> 8192 (ReduceSpec's norm_num
  step peaks above 6144; guard aborted gracefully — R3 was broken, S1
  held). Matches pasta's calibration.
- check.sh: dead-file gate now exempts Scalar* (delegated to
  check-scalar.sh); the gate had been un-passable since the scalar layer
  landed, masked by the memory failure.
- check.sh: axiom-audit phase routed through lean-guard (cgroup + flock;
  was raw lean -M), audit temp file moved into the workspace (lake env
  rejects /tmp inputs — the /tmp phase had never run green).
- check-scalar.sh: NEW Phase 3 kernel axiom audit — ScalarProofs.L_val
  must report exactly [propext, Classical.choice, Quot.sound].
- README: signature layer '⏳ planned' (was 'in progress' with nothing
  started); planned certificate names marked as such.

Validated: full check.sh + check-scalar.sh green end-to-end in the pass-2
sweep (see formal-verification-control/COHERENCE-PASS-2.md).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
 2026-07-03 12:54:26 +02:00
mrwulf
c81b26d9c2 lean-guard: disable core dumps (no more apport popups on capped aborts) 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
 2026-07-02 16:23:30 +02:00
mrwulf
67f1b11730 controls: route all compiles through lean-guard (memory-capped, single-flight) 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
 2026-07-02 16:10:55 +02:00
mrwulf
8ce599c4aa group-law layer: complete twisted Edwards addition law proven 
Extraction widened to backend::serial::curve_models + edwards (own gen/,
209 defs). Adapted the reference Ed* proof suite: namespace rename +
Curve25519TraitsIdentity -> Curve25519_dalekTraitsIdentity. New opaque
externals (scalar_mul backends, get_selected_backend, decompress, sum,
from_slice) are axioms outside both certificate cones — verified by the
Phase-3 audit. All 21 proofs compile; field certificates unchanged.

Not claimed (matching the reference solution's honest scope): edAdd
associativity, scalar multiplication, decompress/compress, AVX2 backend.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
 2026-07-02 14:50:42 +02:00
mrwulf
b79375600f field layer: 14 proofs pass, fieldImplementation axiom-clean 
Ported from the locally verified Hermes working copy; FeQ and Square2Spec
(dead files in the published replica) now compile and are in the check
manifest. check.sh gates: source integrity, stub audit, zero axiom
declarations under Proofs/, per-certificate axiom audit.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
 2026-07-02 14:17:44 +02:00