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

Commit graph

  • 0c82f217a8 coherence sweep: no private paths in public docs; dead /paper/v0.2 links repointed to git history; leaf-index numbering (doc-only) main mrwulf 2026-08-22 18:43:00 +0200
  • 5c5da2f149 docs: estate-wide consistency pass (workflow audit, 36 findings, all verified before fixing) mrwulf 2026-08-07 16:00:53 +0200
  • fa22ececa7 docs: state the signing exclusion (round-7 review, ed-scope-exclusions-missing) mrwulf 2026-08-06 20:54:44 +0200
  • a6e5e89120 verification: lifted phases run under the buttons shell options, enforced in lift-guard mrwulf 2026-08-04 12:58:28 +0200
  • a2922e076e verification: separate the two accounting questions (round-9 review, Claude N2) mrwulf 2026-08-04 03:17:05 +0200
  • 06aaa1f41f lift-guard: eleven more classes, two of them regressions I introduced mrwulf 2026-08-03 21:03:35 +0200
  • e1208634e4 lift-guard: close all nine classes the reviewer demonstrated mrwulf 2026-08-03 13:14:20 +0200
  • b4e8a4e733 audit: bind the scalar statements, and make the accounting identity mean audit mrwulf 2026-08-03 12:15:26 +0200
  • 74d1497e96 correspondence: a named section is not a namespace; an extra axiom is a failure mrwulf 2026-08-02 21:29:54 +0200
  • a46b92b41b verification: derive lift dependencies instead of hand-keeping them mrwulf 2026-08-02 13:07:28 +0200
  • 63fac01889 Round-7 F1: make model/template correspondence SEMANTIC, and fail closed mrwulf 2026-08-02 02:24:15 +0200
  • 37bf01fc6f Account for every constant the kernel sees, by set containment mrwulf 2026-08-01 16:10:59 +0200
  • e2c5cf1d4b P2-c: classify and pin the extraction boundary mrwulf 2026-07-31 17:53:31 +0200
  • dd10ba26a0 P2-a': can a declaration hide from the inventory walker? mrwulf 2026-07-31 11:56:04 +0200
  • 28f13eb5f5 P2-a: attack the arithmetic/apex tier boundary itself mrwulf 2026-07-31 02:39:34 +0200
  • 922bd0e8e1 verification: build hygiene, and the hidden dependency it exposed (P0-a) mrwulf 2026-07-30 22:54:00 +0200
  • 54a6720f7c verification: --audit-only mode, and the guard that keeps it from becoming evidence (T1) mrwulf 2026-07-30 19:16:17 +0200
  • 2060d1d5a5 verification: close the two-button seam and level up the scalar button (P0-b) mrwulf 2026-07-30 12:30:26 +0200
  • 55a688858c verification: pin the whole declaration surface (P1-b) mrwulf 2026-07-30 01:20:15 +0200
  • 18e8753a62 verification: pin the harness, the audit drivers and the policy files (P1-c) mrwulf 2026-07-29 20:12:57 +0200
  • 18abd45edb verification: bind the statements, the specifications, and the model (P1-a) mrwulf 2026-07-29 00:38:17 +0200
  • 93d62703f3 TRUSTED-BASE: record the kernel-side axiom gate and its residue mrwulf 2026-07-28 21:18:44 +0200
  • 9eb3beabc4 verification: kernel-side axiom-declaration gate (Phase 2b) + self-test mrwulf 2026-07-28 18:24:18 +0200
  • 2f182afd64 check.sh: delete the compiled audit artifact, not just its source mrwulf 2026-07-28 17:31:54 +0200
  • 33fb8bb231 Coherence pass 4 (the closing pass): 4-tier apex documentation + hygiene mrwulf 2026-07-06 04:01:15 +0200
  • eb2c77be09 PHASE 2 COMPLETE ON DALEK: THE FULL POINT-LEVEL LIFT (verify_accepts_iff_decompress, button-enforced) mrwulf 2026-07-06 00:05:55 +0200
  • 3c3283f86b Phase 2, decompress step 2: THE BYTE PARSER PROVEN (from_bytes_spec, kernel-audited) mrwulf 2026-07-05 22:55:18 +0200
  • e17687b59f Phase 2, decompress part 2b: THE SQUARE-ROOT WALK PROVEN (sqrt_ratio_i_sq_spec, kernel-audited) mrwulf 2026-07-05 22:03:57 +0200
  • 32d3c05495 Phase 2, decompress part 2a: fe conditional-select + THE SQUARE-ROOT CORE (kernel-audited) mrwulf 2026-07-05 21:16:05 +0200
  • c908982c2c Phase 2, decompress part 1: pow_p58 + ct_eq semantics (kernel-audited) mrwulf 2026-07-05 20:08:21 +0200
  • 5fb5047150 THE POINT-LEVEL VERIFICATION EQUATION: verify_accepts_iff_point_eq, button-enforced (phase-2 goal reached on dalek) mrwulf 2026-07-05 18:27:25 +0200
  • a2803fe34e Phase 2, brick 3 opened: decompress extracted for real (gen green) mrwulf 2026-07-05 18:04:04 +0200
  • fe021b9486 PHASE 2 HALF-LIFT PROVEN: verify_accepts_iff_point, button-enforced mrwulf 2026-07-05 16:06:23 +0200
  • de9d29907b Phase 2, half-lift items 2+5: dsm dispatch transfer + byte-comparison bridge (Proofs/PointLiftSpec.lean, kernel-audited) mrwulf 2026-07-05 14:36:03 +0200
  • 7f166eee12 Phase 2, half-lift prerequisite: the hash-to-scalar entry is canonical (from_bytes_mod_order_wide_spec, kernel-audited) mrwulf 2026-07-05 14:10:09 +0200
  • 85cfb34a7d Phase 2, brick 1 complete: ed_compress_spec - compress emits the canonical encoding of the denoted affine point (kernel-audited) mrwulf 2026-07-05 13:33:58 +0200
  • e07f51c7f7 Phase 2, brick 1a: to_bytes canonicity proven (to_bytes_spec, kernel-audited) mrwulf 2026-07-05 13:10:43 +0200
  • e22e8a12ad Coherence pass 3: post-apex accuracy sweep, hygiene, guard ladder mrwulf 2026-07-05 11:48:17 +0200
  • b7f3934dbd Regenerated CurveField.llbc from the reproducibility run mrwulf 2026-07-04 19:51:05 +0200
  • d6a60b2135 extract.sh: reproducible end-to-end (CurveField merged gen + CurveSig glue) mrwulf 2026-07-04 19:50:37 +0200
  • c177d417ab Remove stray audit temp file mrwulf 2026-07-04 19:46:14 +0200
  • c85704c0c4 THE SIGNATURE APEX: the EdDSA verification equation, proven and audited mrwulf 2026-07-04 19:45:55 +0200
  • 5bf9ed5176 Merge scalar into CurveField; integrate the verify glue against the model mrwulf 2026-07-04 18:13:58 +0200
  • 133eab8467 NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex mrwulf 2026-07-04 16:52:06 +0200
  • 195eafcc16 NAF campaign stages 1-2: LE load walks + the digit loop's arithmetic core mrwulf 2026-07-04 15:30:18 +0200
  • 4071d68457 Double-scalar-mul proof campaign, bricks 1-3: table, digit step, loop mrwulf 2026-07-04 15:30:18 +0200
  • 8e52a449dc Double-scalar-mul enters the verified model: vartime_double_base extracted transparently mrwulf 2026-07-04 11:48:51 +0200
  • 3a10206600 Hash-to-scalar PROVEN: from_bytes_wide_spec - Scalar::from_hash's reduction is exact mod l mrwulf 2026-07-04 10:31:32 +0200
  • e5f8982e84 chore: remove stray telescope probe file (never wired into the button) mrwulf 2026-07-04 04:33:50 +0200
  • 6aa4f39328 Signature layer: the 64-byte unpack certificates (8x8 loops proven) mrwulf 2026-07-04 03:00:42 +0200
  • d08a6e1890 Signature layer, first bricks: canonicity closure + hash-to-scalar foundation mrwulf 2026-07-03 23:18:29 +0200
  • a6b6e86865 Scalar layer complete: Montgomery reduction + full mul proven, scalarImplementation aggregate mrwulf 2026-07-03 21:06:15 +0200
  • 0120fe971a scalar layer: mul_internal proven — Montgomery frontier phase A down saymrwulf 2026-07-03 18:56:04 +0200
  • 5fade418de scalar layer: Scalar52::add FULLY proven mod l (add_val_spec) saymrwulf 2026-07-03 18:02:38 +0200
  • 9479a2bcba re-budget scalar caps post-optimization; guard 3b (headroom clamp) saymrwulf 2026-07-03 17:51:14 +0200
  • 1766544daf scalar layer: Scalar52::sub FULLY proven mod l (sub_val_spec) saymrwulf 2026-07-03 17:26:50 +0200
  • 8a37ed7273 scalar layer: prove Scalar52::sub borrow + conditional-add-L carry chains saymrwulf 2026-07-03 16:26:24 +0200
  • 5f785a75a3 coherence pass 2: restore the one-button property, institutionalize audits saymrwulf 2026-07-03 12:54:26 +0200
  • 2f9e80ada3 coherence pass 1: TRUSTED-BASE scalar notes + both check-button docs mrwulf 2026-07-02 23:58:29 +0200
  • 5eeaaad74a scalar: add ScalarLoop to the check manifest mrwulf 2026-07-02 21:56:40 +0200
  • 24a9fb653a scalar: generic loop-combinator lemmas (loop_step, range_next_lt/ge_spec) mrwulf 2026-07-02 21:47:47 +0200
  • c4fbd063bd scalar layer: clean Scalar52 extraction + denotation foundation mrwulf 2026-07-02 21:13:43 +0200
  • c81b26d9c2 lean-guard: disable core dumps (no more apport popups on capped aborts) mrwulf 2026-07-02 16:23:30 +0200
  • 67f1b11730 controls: route all compiles through lean-guard (memory-capped, single-flight) mrwulf 2026-07-02 16:10:55 +0200
  • 8ce599c4aa group-law layer: complete twisted Edwards addition law proven mrwulf 2026-07-02 14:50:42 +0200
  • b79375600f field layer: 14 proofs pass, fieldImplementation axiom-clean mrwulf 2026-07-02 14:17:44 +0200
  • 1b06f2a0b9 skeleton: proof-pyramid layout, honest status table, trusted-base doc mrwulf 2026-07-02 13:10:26 +0200