From 43ca999645f59f3e80ad997335054244e94f8b93 Mon Sep 17 00:00:00 2001 From: Jordan Mecom Date: Wed, 14 Oct 2026 18:58:22 -0700 Subject: [PATCH] docs(djinn): label the archived optimization objective Identify the original 1.36x result beside its first mention and link the archived structural workload with its later-corrected fixture limitation. Co-authored-by: Codex Signed-off-by: Jordan Mecom --- crates/buzz-core/djinn-relay-filter/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/buzz-core/djinn-relay-filter/README.md b/crates/buzz-core/djinn-relay-filter/README.md index 2c412fd87b..d829418515 100644 --- a/crates/buzz-core/djinn-relay-filter/README.md +++ b/crates/buzz-core/djinn-relay-filter/README.md @@ -17,7 +17,7 @@ Keys and values are exact case-sensitive UTF-8 bytes. Later tag strings are irre ## Generation and proof boundary -The installed upstream is pinned to `8a9ae17c9a6cdbc5220f1881f5ad69f7e2d7e047`. `cargo djinn implement --agent codex` generated both [the complete Rust solution](djinn/solution/mod.rs) and [its Lean proofs](djinn/proofs/RelayFilter/Proofs.lean). The outer implementation owner authored the declarative specification, data-only projection, workload, tests and registry plumbing, **not** the Rust matching algorithm or Lean proofs. The initial fully verified implementation has 144 Rust lines and passed all 16 obligations with the standard axiom audit. Actual `cargo djinn optimize --cycles 3 --jobs 1` accepted two candidates and rejected/reverted the third after proof and timing. The frozen full caller objective improved from 10.297 ms to 7.560 ms per iteration (1.36× versus the first generated implementation), measured by the isolated research compiler. Detailed case measurements, regressions and hashes are recorded in the evidence. +The installed upstream is pinned to `8a9ae17c9a6cdbc5220f1881f5ad69f7e2d7e047`. `cargo djinn implement --agent codex` generated both [the complete Rust solution](djinn/solution/mod.rs) and [its Lean proofs](djinn/proofs/RelayFilter/Proofs.lean). The outer implementation owner authored the declarative specification, data-only projection, workload, tests and registry plumbing, **not** the Rust matching algorithm or Lean proofs. The initial fully verified implementation has 144 Rust lines and passed all 16 obligations with the standard axiom audit. Actual `cargo djinn optimize --cycles 3 --jobs 1` accepted two candidates and rejected/reverted the third after proof and timing. The [archived original structural objective](evidence/STRUCTURAL-V1.md), which included the later-corrected routing-inconsistent fixtures, improved from 10.297 ms to 7.560 ms per iteration (1.36× versus the first generated implementation), measured by the isolated research compiler. Detailed case measurements, regressions and hashes are recorded in the evidence. The proof covers the complete generated predicate: OR, all scalar fields, all generic tags, fallback, termination and absence of Rust panics in the translated operation. The supporting specifications are total and the top-level Boolean result is unambiguous; existence is discharged from the proved implementation. Only `propext`, `Classical.choice`, and `Quot.sound` may occur in audited theorem dependencies. There are no added axioms, admissions, weak output contracts or modifications to trusted translation/models.