fix(ts): resolve missing-symbol errors in src/ir/invariants.ts#62
Conversation
Replace missing symbols Var, Num, StrConst with correct imports (num, lambda, etc.) Update property() calls to use correct API with scope and bindings Fix TypeScript errors that show up under tsc --noEmit
|
Warning Rate limit exceeded
To keep reviews running without waiting, you can enable usage-based add-on for your organization. This allows additional reviews beyond the hourly cap. Account admins can enable it under billing. ⌛ How to resolve this issue?After the wait time has elapsed, 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 have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ 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)
Tip 💬 Introducing [Slack Agent](https://www.coderabbit.ai/agent): Turn conversations into code.Slack Agent is built on CodeRabbit's deep understanding of your code, so your team can collaborate across the entire SDLC without losing context.
Built for teams:
One agent for your entire SDLC. Right inside Slack. 👉 Get your free trial and get 200 agent minutes per Slack user (a $50 value). 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. Review rate limit: 0/1 reviews remaining, refill in 22 minutes and 46 seconds.Comment |
There was a problem hiding this comment.
Pull request overview
This PR updates implementations/typescript/src/ir/invariants.ts to use the current TypeScript IR APIs so the file type-checks under tsc --noEmit. It fits into the TS IR library by keeping the invariant definitions aligned with the newer property(...) and symbolic-construction APIs introduced elsewhere in the kit.
Changes:
- Replaced missing imports/usages (
Var,Num,StrConst) with currently exported helpers and types. - Converted each invariant declaration from the old
property(name, formula)style to the newer object-basedproperty({ name, scope, bindings, formula })API. - Added explicit IR types/casts while rewriting invariant formulas.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| scope: { kind: "module", path: "ir/invariants" }, | ||
| bindings: { vn: StringSort }, | ||
| formula: ({ vn }) => { | ||
| const c = choice(vn as unknown as string, Int, liftToTerm(true) as any); |
| return and( | ||
| liftToTerm("proofType" in evidence) as any, | ||
| liftToTerm("certificate" in evidence) as any |
| scope: { kind: "module", path: "ir/invariants" }, | ||
| bindings: { vn: StringSort }, | ||
| formula: ({ vn }) => { | ||
| const c = choice(vn as unknown as string, Int, liftToTerm(true) as any); |
| bindings: { name: StringSort }, | ||
| formula: ({ name }) => { | ||
| const v: IrTerm = { kind: "var", name: name as unknown as string }; |
| formula: ({ name }) => { | ||
| const v: IrTerm = { kind: "var", name: name as unknown as string }; | ||
| // VarTerm has no sort field at runtime | ||
| return not(liftToTerm("sort" in v) as unknown as IrFormula); |
| const lam = lambda("x", Int, liftToTerm(body)); | ||
| return and( | ||
| liftToTerm("body" in lam) as any, | ||
| not(assert.equal((lam as { body: IrTerm }).body, undefined as any)) |
| liftToTerm("bindings" in l) as any, | ||
| liftToTerm(Array.isArray((l as any).bindings)) as any, | ||
| ((l as any).bindings.length >= 1) | ||
| ? liftToTerm(true) as any | ||
| : liftToTerm(false) as any |
| const l = letTerm([{ name: "x", boundTerm: num(1) }], liftToTerm(x)); | ||
| return and( | ||
| liftToTerm("body" in l) as any, | ||
| not(assert.equal((l as any).body, undefined as any)) |
| const c = choice(vn as unknown as string, Int, liftToTerm(true) as any); | ||
| return and( | ||
| liftToTerm("body" in c) as any, | ||
| not(assert.equal((c as any).body, undefined as any)) |
| bindings: { pn: StringSort }, | ||
| formula: ({ pn }) => { | ||
| const lam = lambda(pn as unknown as string, Int, num(42)); |
![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: 634d57a334
ℹ️ 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".
| formula: ({ name }) => { | ||
| const v: IrTerm = { kind: "var", name: name as unknown as string }; | ||
| // VarTerm has no sort field at runtime | ||
| return not(liftToTerm("sort" in v) as unknown as IrFormula); |
There was a problem hiding this comment.
The invariant formulas now pass liftToTerm(...) results into logical operators (for example not(liftToTerm("sort" in v) as ...)), but liftToTerm returns an IrTerm (kind: "const"), not an IrFormula. That creates malformed formula trees where connective operands are terms, and downstream canonicalization expects only formula kinds (forall/exists/and/or/not/implies/atomic/choice), so processing these properties can fail or produce invalid IR when these invariants are minted/evaluated.
Useful? React with 👍 / 👎.
Summary
implementations/typescript/src/ir/invariants.tsVar,Num,StrConstwith correct imports (num,lambda, etc.)property()calls to use correct API withscopeandbindingstsc --noEmitBackground
PR #17 (TS cross-impl port) flagged this file references missing symbols
Num,StrConst,Var— pre-existing TS errors that don't trip vitest (which is what CI runs) but show up undertsc --noEmit.Changes
Var→{ kind: "var", name }(VarTerm creation)Num→num(correct function name)StrConst→ not used in fileproperty()calls to use correct API signature