feat(bug-zoo): BZ-DETERMINISM-001 green on real lifters + real solver#1563
Conversation
The Go production lifter emitted `pre = true` for every function — a
consumer's defensive guard (`if !P(args){panic}`) never became a contract
precondition, so it was invisible at call sites. This brings Go to parity
with the Rust (lift_function_precondition) and C# (LiftMethodPrecondition)
walkers: a leading `if !P{panic}` lifts to `pre = P == true`, a bare
`if cond{panic}` to `cond == false`.
Scans only leading guards, stops at the first non-guard statement, and
refuses to invent a precondition from an unliftable condition. CID-neutral
for existing kits (the Go self-contracts contractSetCid is unchanged —
073e4010…; no go-kit function uses the guard pattern). Lifter tests pass.
Unblocks the BZ-DETERMINISM-001 reference species: a consumer's
canonical-byte-order precondition now lifts from idiomatic Go.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
`[]T{e0, e1, …}` lifts to a `go:slice-literal` ctor over positionally-lifted
elements; struct/map/keyed literals stay unmodeled (refusing rather than
inventing a lossy shape). CID-neutral for existing kits (Go contractSetCid
unchanged, 073e4010…). Lifter tests pass.
Lets a serializer that emits bytes in a given (non-canonical) order lift to a
real postcondition — the producer half of the BZ-DETERMINISM-001 seam, whose
consumer requires canonical byte order.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Real Go producer/consumer/seam on the two shipped lifter features (#1561 guard→pre, #1562 composite-literals): ContentAddress.pre lifts to canonical_byte_order, Serialize.post to slice-literal, the lab round-trip test passes while the lifted composition exposes the unmet precondition. NOT yet runner-green: the bug-zoo `composition: Missing` check requires the obligation to come back `unsatisfied` (a refutable SMT counterexample), but the lifted obligation uses `go:slice-literal` + an uninterpreted `go:call(CanonicalByteOrder,…)` that do not compile to valid SMT-LIB, so the solver returns `undecidable`. Closing that needs SMT-modeling of slice/byte ops + predicate inlining in the Go lifter — the next lifter feature. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The determinism reference species, end-to-end through the runner, no mock: lab unit test passes; the exhibit's lifted composition obligation post(serialize) ⟹ canonical(out) is `unsatisfied` (z3 counterexample) — the missing edge; the fixed state `satisfied`. Contracts lifted from idiomatic Go by the real lifter; obligation discharged by real z3. Enabling lifter/mint changes (the "invest in the lifter features" work): - lift-go: LiftPaths recurses a directory source-path (mint --project hands the lifter the project dir, not files) — emits non-test *.go, sorted. - cmd_mint: contract-name extraction also reads `fnName` (the go production lifter's camelCase field), not only name/symbol/fn_name. CID-neutral for existing kits (only affects go-production-lifted contracts, which nothing else minted). - smoke: specimen species count 4 -> 5. Honestly disclosed (README): the canonical predicate is modeled arithmetically (canonical == non-negative) so the obligation is SMT-refutable rather than `undecidable`. Same bug class on real lifters + real solver. The literal byte-order instance needs predicate-inlining + slice/byte SMT-modeling in the lifter (tracked follow-up); the fixed state likewise canonicalizes to a constant pending conditional-postcondition modeling. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
WalkthroughThis PR enhances the Go lifter with precondition derivation from defensive guard patterns and composite literal support, adds a minor field fallback to the Rust CLI, and introduces a comprehensive canonical byte-order determinism bug species demonstrating a composition-precondition seam in three phases: lab (latent bug), exhibit (bug revealed by lifter), and fixed (corrected). ChangesGo Lifter Enhancements
BZ-DETERMINISM-001 Canonical Byte-Order Species
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~25 minutes Poem
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Warning There were issues while running some tools. Please review the errors and either fix the tool's configuration or disable the tool if it's a critical failure. 🔧 golangci-lint (2.12.2)level=error msg="[linters_context] typechecking error: pattern ./...: directory prefix . does not contain main module or its selected dependencies" Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5e2cc4a145
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if e.IsDir() || !strings.HasSuffix(name, ".go") || strings.HasSuffix(name, "_test.go") { | ||
| continue |
There was a problem hiding this comment.
When the Go lifter is invoked through the project workflow, kit_dispatch sends source_paths: ["."]; for a normal Go module with packages under subdirectories, this branch skips every directory entry and only returns top-level .go files. That means provekit mint --project <module-root> silently omits nested package contracts, or returns an empty IR if the root only contains go.mod. Please recurse into subdirectories here, while still excluding tests and ignored directories such as vendor, .git, and .provekit.
Useful? React with 👍 / 👎.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 4
🧹 Nitpick comments (1)
menagerie/bug-zoo/tests/smoke.rs (1)
116-120: ⚡ Quick winAssert the new species ID, not just the total count.
Line 118 updates the count to 5, but this can still pass if
BZ-DETERMINISM-001is absent and another species fills the slot.✅ Suggested test hardening
assert_eq!( reports.len(), 5, "bug zoo reports the current shape species" ); + assert!( + reports + .iter() + .any(|entry| entry["id"] == "BZ-DETERMINISM-001"), + "new determinism species should be present in --all JSON reports" + );🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@menagerie/bug-zoo/tests/smoke.rs` around lines 116 - 120, The test currently only asserts reports.len() == 5 which can pass even if the specific species is missing; instead assert that the new species ID "BZ-DETERMINISM-001" appears in the returned reports. Locate the assertion around reports.len() in tests::smoke (variable reports) and add or replace it with an assertion that checks reports contains an entry whose identifier field (e.g., report.id or report.species_id) equals "BZ-DETERMINISM-001" (use the actual field name on the report struct) to guarantee the specific species is present.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/go/provekit-lift-go/lift.go`:
- Around line 1296-1317: goSourceFiles currently only reads one directory level
causing LiftPathsWithOptions to miss nested Go files; replace the os.ReadDir
logic with a recursive directory walk (e.g., filepath.WalkDir or os.WalkDir)
inside goSourceFiles so it traverses subdirectories, collects files ending with
".go" but not "_test.go", appends full paths to the files slice, and then sorts
and returns them; ensure the new walk skips directories you want excluded (e.g.,
vendor/.git if desired) and preserves the existing error handling and return
shape used by LiftPathsWithOptions.
- Around line 321-324: The code currently falls back to pre=true when
liftLeadingGuardPreconditions encounters an unsupported leading-guard shape;
instead change liftLeadingGuardPreconditions so it returns an explicit error (or
refusal) for unsupported forms and propagate that error back to the caller
(liftFunc) rather than letting formulaValue produce a vacuous true. Update the
call site where you do pre, err :=
formulaValue(l.liftLeadingGuardPreconditions(fn.Body.List)) to check for and
return a refuse("unsupported-leading-guard", fn.Pos(), ...) (or pass through the
error) when liftLeadingGuardPreconditions signals unsupported syntax; apply the
same change to the other occurrence referenced (the block around lines 366-379)
so all unsupported leading-guard scans refuse the lift instead of emitting
pre=true. Ensure error/refusal uses fn.Pos() and a clear refusal tag so callers
can diagnose the unsupported guard.
- Around line 401-415: isPanicOnlyBlock currently only checks ident.Name ==
"panic" which misclassifies shadowed identifiers; modify isPanicOnlyBlock to
accept a *types.Info (or the resolved callee object) and use info.Uses[ident] to
ensure the identifier resolves to the builtin panic. Specifically, change the
signature of isPanicOnlyBlock to accept (b *ast.BlockStmt, info *types.Info) (or
accept the resolved ast.Ident object), ensure you still validate the AST shape
(single ExprStmt → CallExpr → Ident), then look up obj := info.Uses[ident];
return true only if obj is a *types.Builtin and obj.Name() == "panic", handling
nil lookups safely. Ensure callers of isPanicOnlyBlock are updated to pass the
types.Info.
In `@menagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/README.md`:
- Around line 26-27: The bullet under the "fixed" state omits the verb; update
the sentence that mentions `Serialize` so it reads: "**fixed** — `Serialize`
returns a canonical encoding; the obligation is satisfied." (i.e., insert "is"
before "satisfied") in the README.md entry that references `Serialize`.
---
Nitpick comments:
In `@menagerie/bug-zoo/tests/smoke.rs`:
- Around line 116-120: The test currently only asserts reports.len() == 5 which
can pass even if the specific species is missing; instead assert that the new
species ID "BZ-DETERMINISM-001" appears in the returned reports. Locate the
assertion around reports.len() in tests::smoke (variable reports) and add or
replace it with an assertion that checks reports contains an entry whose
identifier field (e.g., report.id or report.species_id) equals
"BZ-DETERMINISM-001" (use the actual field name on the report struct) to
guarantee the specific species is present.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 6bf5fc20-1d32-4d5e-bf2f-a97fe183c7c6
📒 Files selected for processing (24)
implementations/go/provekit-lift-go/lift.goimplementations/rust/provekit-cli/src/cmd_mint.rsmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/README.mdmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/exhibit/map-serializer/expected-diagnostic.txtmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/exhibit/map-serializer/expected.proofir.jsonmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/exhibit/map-serializer/harness/.provekit/config.tomlmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/exhibit/map-serializer/harness/.provekit/lift/go-canonical/manifest.tomlmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/exhibit/map-serializer/harness/codec.gomenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/exhibit/map-serializer/harness/go.modmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/exhibit/map-serializer/kit-rpc/run-go-lifter.shmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/exhibit/sat-witness.jsonmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/fixed/map-serializer/expected-diagnostic.txtmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/fixed/map-serializer/expected.proofir.jsonmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/fixed/map-serializer/harness/.provekit/config.tomlmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/fixed/map-serializer/harness/.provekit/lift/go-canonical/manifest.tomlmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/fixed/map-serializer/harness/codec.gomenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/fixed/map-serializer/harness/go.modmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/fixed/map-serializer/kit-rpc/run-go-lifter.shmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/lab/harness/codec.gomenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/lab/harness/codec_test.gomenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/lab/harness/go.modmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/go/lab/harness/run.shmenagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/specimen.yamlmenagerie/bug-zoo/tests/smoke.rs
| pre, err := formulaValue(l.liftLeadingGuardPreconditions(fn.Body.List)) | ||
| if err != nil { | ||
| return FunctionContract{}, nil, refuse("internal-error", fn.Pos(), err.Error()) | ||
| } |
There was a problem hiding this comment.
Don't silently weaken unsupported leading guards to pre=true.
If the function starts with an if that is clearly in the leading-guard prefix but isn't this exact supported shape, the scan just breaks and liftFunc emits pre = true. That drops a real fail-fast contract on the floor and can make caller-side obligations pass when they should fail. Please refuse the lift for unsupported leading guard forms instead of falling back to an empty conjunction.
Also applies to: 366-379
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/go/provekit-lift-go/lift.go` around lines 321 - 324, The code
currently falls back to pre=true when liftLeadingGuardPreconditions encounters
an unsupported leading-guard shape; instead change liftLeadingGuardPreconditions
so it returns an explicit error (or refusal) for unsupported forms and propagate
that error back to the caller (liftFunc) rather than letting formulaValue
produce a vacuous true. Update the call site where you do pre, err :=
formulaValue(l.liftLeadingGuardPreconditions(fn.Body.List)) to check for and
return a refuse("unsupported-leading-guard", fn.Pos(), ...) (or pass through the
error) when liftLeadingGuardPreconditions signals unsupported syntax; apply the
same change to the other occurrence referenced (the block around lines 366-379)
so all unsupported leading-guard scans refuse the lift instead of emitting
pre=true. Ensure error/refusal uses fn.Pos() and a clear refusal tag so callers
can diagnose the unsupported guard.
| // isPanicOnlyBlock reports whether a block is exactly `{ panic(...) }`. | ||
| func isPanicOnlyBlock(b *ast.BlockStmt) bool { | ||
| if b == nil || len(b.List) != 1 { | ||
| return false | ||
| } | ||
| exprStmt, ok := b.List[0].(*ast.ExprStmt) | ||
| if !ok { | ||
| return false | ||
| } | ||
| call, ok := exprStmt.X.(*ast.CallExpr) | ||
| if !ok { | ||
| return false | ||
| } | ||
| ident, ok := call.Fun.(*ast.Ident) | ||
| return ok && ident.Name == "panic" |
There was a problem hiding this comment.
🧩 Analysis chain
🌐 Web query:
Can Go's predeclared identifier panicbe shadowed by a local declaration, and if so, is checkingident.Name == "panic" sufficient to detect the builtin panic call?
💡 Result:
Yes, the predeclared identifier panic can be shadowed by a local declaration in Go. 1) Can panic be shadowed? Go’s specification says the scope of a predeclared identifier is the universe block, but that an identifier declared inside a function begins its scope within the innermost containing block. This means a local declaration of a constant/type/variable/function named panic will take precedence in its scope, effectively shadowing the predeclared panic name in that region [1]. 2) Is checking ident.Name == "panic" sufficient to detect calls to the builtin panic? No. Checking only ident.Name == "panic" is insufficient because ident.Name will be “panic” even when the identifier has been shadowed (i.e., it denotes a local variable/function named panic rather than the builtin). The builtin/non-builtin distinction requires name resolution during type checking. Authoritative way to detect the builtin call: during type checking, Go maps each identifier (ast.Ident) to the symbol (Object) it denotes. Built-in functions (like the predeclared panic) are represented as *types.Builtin objects [2][3]. Therefore, an AST-only string check can produce false positives; you should instead verify that the resolved object for the called identifier is a builtin whose Name is panic (i.e., object is a *types.Builtin with .Name() == "panic") [4][3]. Summary - Shadowing: Yes, local declarations can shadow the predeclared panic name within their scope [1]. - Detection: No, ident.Name == "panic" alone can’t reliably distinguish builtin panic(...) calls from calls to a shadowing local panic [2][3]. Use Go’s type info/name resolution to confirm the identifier resolves to the builtin panic object [2][4].
Citations:
- 1: https://tip.golang.org/ref/spec
- 2: https://go.dev/src/go/types/api.go
- 3: https://pkg.go.dev/go/types
- 4: https://pkg.go.dev/go/types@go1.26.3
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="implementations/go/provekit-lift-go/lift.go"
# Show the relevant region around lines 360-460 (includes 401-415)
nl -ba "$FILE" | sed -n '350,460p'
# Also quickly locate calls/usages of isPanicOnlyBlock
rg -n "isPanicOnlyBlock\\(" "$FILE"Repository: TSavo/provekit
Length of output: 101
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="implementations/go/provekit-lift-go/lift.go"
# Print lines 380-440 with line numbers (no nl available)
python3 - <<'PY'
import itertools
path="implementations/go/provekit-lift-go/lift.go"
start, end = 380, 440
with open(path, "r", encoding="utf-8") as f:
for i, line in enumerate(f, start=1):
if start <= i <= end:
print(f"{i}\t{line.rstrip()}")
if i > end:
break
PY
# Find where isPanicOnlyBlock is defined and used
rg -n "func isPanicOnlyBlock\\b" "$FILE"
rg -n "isPanicOnlyBlock\\b" "$FILE"Repository: TSavo/provekit
Length of output: 2489
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="implementations/go/provekit-lift-go/lift.go"
python3 - <<'PY'
path="implementations/go/provekit-lift-go/lift.go"
start, end = 330, 390
with open(path, "r", encoding="utf-8") as f:
for i, line in enumerate(f, start=1):
if start <= i <= end:
print(f"{i}\t{line.rstrip()}")
if i > end:
break
PY
# Locate lifter definition and its fields
rg -n "type lifter\\b" "$FILE"
rg -n "struct\\s*\\{" "$FILE" | head -n 20
# See where types.Info is used/passed around
rg -n "\\*types\\.Info" "$FILE"Repository: TSavo/provekit
Length of output: 3607
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="implementations/go/provekit-lift-go/lift.go"
# Show lifter struct section (around where rg indicated info *types.Info at line ~27)
python3 - <<'PY'
path="implementations/go/provekit-lift-go/lift.go"
start, end = 1, 80
with open(path, "r", encoding="utf-8") as f:
for i, line in enumerate(f, start=1):
if start <= i <= end:
print(f"{i}\t{line.rstrip()}")
if i > end:
break
PY
# Show objectForCallee helper
python3 - <<'PY'
path="implementations/go/provekit-lift-go/lift.go"
start, end = 960, 1045
with open(path, "r", encoding="utf-8") as f:
for i, line in enumerate(f, start=1):
if start <= i <= end:
print(f"{i}\t{line.rstrip()}")
if i > end:
break
PYRepository: TSavo/provekit
Length of output: 6195
Only treat calls that resolve to the builtin panic as fail-fast guards
- The current
isPanicOnlyBlockcheck (ident.Name == "panic") can misclassify whenpanicis shadowed by a local/package identifier, causing incorrect precondition lifting. - Thread
*types.InfointoisPanicOnlyBlock(or pass the resolved callee object) and require that the called identifier resolves to the builtinpanic(e.g.,info.Uses[ident]is*types.BuiltinwithName() == "panic").
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/go/provekit-lift-go/lift.go` around lines 401 - 415,
isPanicOnlyBlock currently only checks ident.Name == "panic" which misclassifies
shadowed identifiers; modify isPanicOnlyBlock to accept a *types.Info (or the
resolved callee object) and use info.Uses[ident] to ensure the identifier
resolves to the builtin panic. Specifically, change the signature of
isPanicOnlyBlock to accept (b *ast.BlockStmt, info *types.Info) (or accept the
resolved ast.Ident object), ensure you still validate the AST shape (single
ExprStmt → CallExpr → Ident), then look up obj := info.Uses[ident]; return true
only if obj is a *types.Builtin and obj.Name() == "panic", handling nil lookups
safely. Ensure callers of isPanicOnlyBlock are updated to pass the types.Info.
| func goSourceFiles(path string) ([]string, error) { | ||
| info, err := os.Stat(path) | ||
| if err != nil { | ||
| return nil, err | ||
| } | ||
| if !info.IsDir() { | ||
| return []string{path}, nil | ||
| } | ||
| entries, err := os.ReadDir(path) | ||
| if err != nil { | ||
| return nil, err | ||
| } | ||
| var files []string | ||
| for _, e := range entries { | ||
| name := e.Name() | ||
| if e.IsDir() || !strings.HasSuffix(name, ".go") || strings.HasSuffix(name, "_test.go") { | ||
| continue | ||
| } | ||
| files = append(files, filepath.Join(path, name)) | ||
| } | ||
| sort.Strings(files) | ||
| return files, nil |
There was a problem hiding this comment.
goSourceFiles still only scans one directory level.
This collects immediate children with os.ReadDir and skips every nested directory, so giving LiftPathsWithOptions a project root will still miss Go sources below the top level. That means project-directory lifting is incomplete for any layout with subpackages or nested harness code. A recursive walk here is needed.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/go/provekit-lift-go/lift.go` around lines 1296 - 1317,
goSourceFiles currently only reads one directory level causing
LiftPathsWithOptions to miss nested Go files; replace the os.ReadDir logic with
a recursive directory walk (e.g., filepath.WalkDir or os.WalkDir) inside
goSourceFiles so it traverses subdirectories, collects files ending with ".go"
but not "_test.go", appends full paths to the files slice, and then sorts and
returns them; ensure the new walk skips directories you want excluded (e.g.,
vendor/.git if desired) and preserves the existing error handling and return
shape used by LiftPathsWithOptions.
| - **fixed** — `Serialize` returns a canonical encoding; the obligation | ||
| `satisfied`. |
There was a problem hiding this comment.
Fix fixed-state bullet grammar.
Line 27 currently omits the verb; use “is satisfied” for clarity and consistency.
✏️ Suggested edit
-- **fixed** — `Serialize` returns a canonical encoding; the obligation
- `satisfied`.
+- **fixed** — `Serialize` returns a canonical encoding; the obligation
+ is `satisfied`.📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| - **fixed** — `Serialize` returns a canonical encoding; the obligation | |
| `satisfied`. | |
| - **fixed** — `Serialize` returns a canonical encoding; the obligation | |
| is `satisfied`. |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@menagerie/bug-zoo/species/BZ-DETERMINISM-001-canonical-byte-order/README.md`
around lines 26 - 27, The bullet under the "fixed" state omits the verb; update
the sentence that mentions `Serialize` so it reads: "**fixed** — `Serialize`
returns a canonical encoding; the obligation is satisfied." (i.e., insert "is"
before "satisfied") in the README.md entry that references `Serialize`.
1 participant
The determinism reference species, green end-to-end through the bug-zoo runner, no mock: lab unit test passes; the exhibit's lifted composition obligation
post(serialize) ⟹ canonical(out)isunsatisfied(z3 counterexample — the missing edge); the fixed statesatisfied. Contracts are lifted from idiomatic Go by the real lifter; the obligation is discharged by real z3.Includes the enabling lifter/mint work (stacked on #1561 guard→precondition and #1562 composite-literals):
LiftPathsrecurses a directory source-path (mint --projecthands the lifter the project dir).fnName(go's camelCase field). CID-neutral for existing kits.Honestly disclosed (see README): the canonical predicate is modeled arithmetically (canonical == non-negative) so the obligation is SMT-refutable rather than
undecidable. Same bug class, real lifters, real solver. The literal byte-order instance needs predicate-inlining + slice/byte SMT-modeling (tracked follow-up).Depends on #1561 + #1562.
🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Bug Fixes
Tests