feat(lift-go): model unkeyed slice/array composite literals#1562
Conversation
`[]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>
|
Warning Review limit reached
More reviews will be available in 46 minutes and 2 seconds. Learn how PR review limits work. Your organization has run out of usage credits. Purchase more in the billing tab. ⌛ How to resolve this issue?After more reviews become available, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans include higher PR review limits than trial, open-source, and free plans. In all cases, reviews become available again over time. During sustained high-volume PR review activity, CodeRabbit may temporarily slow when the next review becomes available. Please see our Fair Usage Limits Policy for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (1)
✨ Finishing Touches🧪 Generate unit tests (beta)
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: 5fb6fb1145
ℹ️ 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".
| term: ir.MakeCtor("go:slice-literal", elemTerms, sort), | ||
| alg: op("go:slice-literal", elemAlgs...), |
There was a problem hiding this comment.
When a lifted function body or standalone function-contract contains []T{...}, this new go:slice-literal ctor is now emitted into the post/body term, but goExprFromIRTerm in implementations/go/provekit-lift-go/compile.go has no case for it. That makes newly lifted IR fail CompileBody/bare-body round trips, and compiling a contract-only IR for a non-void function can drop the return expression instead of reconstructing the slice literal. Please add the matching compile case or keep refusing these literals until the source compiler can consume the new ctor.
Useful? React with 👍 / 👎.
1 participant
[]T{e0, e1, …}lifts to ago:slice-literalctor over positionally-lifted elements; struct/map/keyed literals stay unmodeled (refused rather than lifted lossily). CID-neutral for existing kits (GocontractSetCidunchanged,073e4010…); lifter tests pass.Second of the lifter features for BZ-DETERMINISM-001: lets a serializer emitting bytes in a given (non-canonical) order lift to a real postcondition. With #1561 (guard→precondition), the determinism seam now lifts end-to-end from idiomatic Go —
provekit prove --formulaonpost(serialize) ⟹ pre(content_address)returns not-valid (the consumer'scanonical_byte_orderprecondition can't be discharged from the producer's post). Real contracts, real solver, no mock.🤖 Generated with Claude Code