v1.3.1 — Bug fixes + proof strengthening
Bug fixes
-
Fix Set/Delete input-buffer aliasing (#209, #141) —
SetandDeleteno longer corrupt the caller's input[]bytewhen the slice has spare capacity. Theappend()call path was writing into the backing array beyond the returned slice. Now all mutation paths allocate a fresh buffer. -
Fix EachKey array-index inconsistency (#232) —
EachKeynow descends into terminal array-index paths (e.g."key", "[0]") consistently withGet. PreviouslyEachKeyreturned empty whereGetsucceeded on the same path. -
Fix benchmark measuring ffjson, not encoding/json (#126) — the benchmark payload types had ffjson-generated
MarshalJSON/UnmarshalJSONmethods, so the "10x faster than encoding/json" comparison was silently measuring ffjson. Now uses plain types with no generated methods.
Proof strengthening (how these bugs escaped, and the gates that prevent recurrence)
| Bug | Proof gap | New gate |
|---|---|---|
| #209/#141 Set aliasing | No obligation said "Set must not mutate the input buffer" | New obligation no_input_mutation + assertInputUnchanged gate (snapshots input + backing-array capacity before every Set/Delete, verifies unchanged after) |
| #232 EachKey ≠ Get | No obligation said "EachKey must resolve paths identically to Get" | New obligation api_consistency + TestApiConsistencyEachKeyMatchesGet gate (random JSON + paths, asserts EachKey result == Get result) |
| #126 benchmark ffjson | Proof didn't cover the benchmark suite | Benchmark honesty lint: verifies no benchmark type implements json.Marshaler/json.Unmarshaler |
Contributed by codex (gpt-5-codex) via codex exec.