jerry/buzz
1
0
Fork 0
mirror of https://github.com/block/buzz.git synced 2026-11-13 12:51:34 +00:00
Code Issues Packages Projects Releases Wiki Activity

docs(djinn): label the archived optimization objective

Browse Source 
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 <codex@openai.com>
Signed-off-by: Jordan Mecom <jm@squareup.com>
This commit is contained in:
Jordan Mecom
2026-10-14 18:58:22 -07:00
parent 97e9b4e2d2
commit 43ca999645
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
crates/buzz-core/djinn-relay-filter/README.md
View File

@@ -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.