Skip to content

[ir1-ssa-contract] Patch 1: Add skipped IR1 SSA contract tests#259

Closed
subsetpark wants to merge 1 commit into
mainfrom
ir1-ssa-contract/patch-1
Closed

[ir1-ssa-contract] Patch 1: Add skipped IR1 SSA contract tests#259
subsetpark wants to merge 1 commit into
mainfrom
ir1-ssa-contract/patch-1

Conversation

@subsetpark
Copy link
Copy Markdown
Collaborator

@subsetpark subsetpark commented May 9, 2026

Patch 1: Add skipped IR1 SSA contract tests

  • Create describe("ir1-ssa-contract", ...) in tools/ts2pant/tests/ir1-ssa-contract.test.mts.
  • Add skipped tests for opaque version allocation with location metadata.
  • Add skipped tests for degenerate join simplification and location-compatible join construction.
  • Add skipped tests proving Map value and membership are represented as distinct coordinated locations.
  • Add skipped tests proving Set clear is represented inside the Set membership SSA value.
  • Add skipped tests proving foreach loop summaries produce distinct summary versions.
  • Each skipped test should include a short PENDING comment naming Patch 2 as the implementation patch.

Changes

  • Create describe("ir1-ssa-contract", ...) in tools/ts2pant/tests/ir1-ssa-contract.test.mts.
  • Add skipped tests for opaque version allocation with location metadata.
  • Add skipped tests for degenerate join simplification and location-compatible join construction.
  • Add skipped tests proving Map value and membership are represented as distinct coordinated locations.
  • Add skipped tests proving Set clear is represented inside the Set membership SSA value.
  • Add skipped tests proving foreach loop summaries produce distinct summary versions.
  • Each skipped test should include a short PENDING comment naming Patch 2 as the implementation patch.

Files to Modify

  • tools/ts2pant/tests/ir1-ssa-contract.test.mts (create): Create node:test stubs with skip markers for the IR1 SSA type and constructor contract.

Gameplan Specification

module IR1_SSA_CONTRACT.

IR1Program.
Construct.
Location.
Version.
Read.
Write.
Join.
LoopSummary.
Rule.
PropResult.
Diagnostic.

supported-constructs p: IR1Program => [Construct].
lowered-constructs p: IR1Program => [Construct].
diagnostics p: IR1Program => [Diagnostic].
diagnostic-construct d: Diagnostic => Construct.
writes p: IR1Program => [Write].
reads p: IR1Program => [Read].
joins p: IR1Program => [Join].
loop-summaries p: IR1Program => [LoopSummary].
write-location w: Write => Location.
write-version w: Write => Version.
read-location r: Read => Location.
read-version r: Read => Version.
read-dominated? p: IR1Program, r: Read => Bool.
join-location j: Join => Location.
then-version j: Join => Version.
else-version j: Join => Version.
join-version j: Join => Version.
summary-location s: LoopSummary => Location.
summary-version s: LoopSummary => Version.
initial-version l: Location => Version.
version-location v: Version => Location.
rule-of-location l: Location => Rule.
declared-rules p: IR1Program => [Rule].
modified-rules p: IR1Program => [Rule].
framed-rules p: IR1Program => [Rule].
emitted-props p: IR1Program => [PropResult].

---

all p: IR1Program, c in supported-constructs p |
  c in lowered-constructs p.

all p: IR1Program, d in diagnostics p |
  ~(diagnostic-construct d in supported-constructs p).

all p: IR1Program, w in writes p |
  version-location (write-version w) = write-location w.

all p: IR1Program, s in loop-summaries p |
  version-location (summary-version s) = summary-location s.

all l: Location |
  version-location (initial-version l) = l.

all p: IR1Program, w1 in writes p, w2 in writes p |
  write-version w1 = write-version w2 -> w1 = w2.

all p: IR1Program, r in reads p |
  read-dominated? p r and
  version-location (read-version r) = read-location r and
  (
    read-version r = initial-version (read-location r) or
    (some w in writes p |
      write-version w = read-version r and
      write-location w = read-location r) or
    (some s in loop-summaries p |
      summary-version s = read-version r and
      summary-location s = read-location r)
  ).

all p: IR1Program, j in joins p |
  version-location (then-version j) = join-location j and
  version-location (else-version j) = join-location j and
  version-location (join-version j) = join-location j.

all p: IR1Program, j in joins p |
  then-version j != else-version j and
  join-version j != then-version j and
  join-version j != else-version j.

all p: IR1Program, rule in modified-rules p |
  rule in declared-rules p and
  ~(rule in framed-rules p).

all p: IR1Program, rule in framed-rules p |
  rule in declared-rules p and
  ~(rule in modified-rules p).

all p: IR1Program, rule in declared-rules p |
  rule in modified-rules p or rule in framed-rules p.

all p: IR1Program, w in writes p |
  rule-of-location (write-location w) in modified-rules p.

all p: IR1Program, s in loop-summaries p |
  rule-of-location (summary-location s) in modified-rules p.

all p: IR1Program |
  #(lowered-constructs p) > 0 -> #(emitted-props p) > 0.

Patch Specification

module IR1_SSA_CONTRACT_PATCH_1.

SsaContractTest.
Invariant.

covers-invariant t: SsaContractTest => Invariant.
implemented? t: SsaContractTest => Bool.

---

> Patch 1 introduces pending test declarations only. The tests may be skipped,
> but each test must name an invariant it is intended to cover.
all t: SsaContractTest | covers-invariant t = covers-invariant t.

Implementation Notes

No additional notes: this patch is a test-only scaffold with skipped stubs, and it intentionally avoids changing IR1 behavior or production translation paths.


Summary by cubic

Add tools/ts2pant/tests/ir1-ssa-contract.test.mts with a skipped test suite defining the IR1 SSA contract. It documents pending invariants for opaque version allocation with location metadata, degenerate join simplification, Map value vs membership locations, Set clear encoding, and distinct loop-summary versions to be implemented in Patch 2.

Written for commit 0aae2d3. Summary will update on new commits.

Summary by CodeRabbit

  • Tests
    • Added placeholder test cases for upcoming feature enhancements in future patches.

Review Change Stack

@vercel
Copy link
Copy Markdown

vercel Bot commented May 9, 2026

The latest updates on your projects. Learn more about Vercel for GitHub.

Project Deployment Actions Updated (UTC)
onton Ready Ready Preview, Comment May 9, 2026 8:09pm

Request Review

@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 9, 2026

Caution

Review failed

Pull request was closed or merged during review

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info
⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: CHILL

Plan: Pro

Run ID: a1e3fa2f-7a8a-46e2-b052-5b26827b5ee6

📥 Commits

Reviewing files that changed from the base of the PR and between 655eca8 and 0aae2d3.

📒 Files selected for processing (1)
  • tools/ts2pant/tests/ir1-ssa-contract.test.mts

📝 Walkthrough

Walkthrough

This PR introduces a new test file defining a skeleton test suite for SSA contract invariants. The file contains five skipped test cases with placeholder bodies marked for future implementation in a subsequent patch.

Changes

SSA Contract Test Skeleton

Layer / File(s) Summary
Test Imports
tools/ts2pant/tests/ir1-ssa-contract.test.mts
Node.js test framework imports are established.
Test Suite and Cases
tools/ts2pant/tests/ir1-ssa-contract.test.mts
Five skipped test cases are defined for opaque SSA version allocation with location metadata, degenerate join simplification before join node construction, Map state modeling as coordinated value plus membership, Set clear encoding within membership SSA values, and distinct loop-summary version exposure.

Estimated code review effort

🎯 1 (Trivial) | ⏱️ ~3 minutes

Poem

🐰 A new test file hops into view,
Five skipped cases, pending their due,
With "Patch 2" placeholders in sight,
SSA contracts await their light,
Future specs in a test written true!

🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title clearly and accurately summarizes the primary change: adding skipped test cases for the IR1 SSA contract suite as part of Patch 1.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.

✏️ Tip: You can configure your own custom pre-merge checks in the settings.

✨ Finishing Touches
📝 Generate docstrings
  • Create stacked PR
  • Commit on current branch
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch ir1-ssa-contract/patch-1

Comment @coderabbitai help to get the list of available commands and usage tips.

@subsetpark subsetpark marked this pull request as ready for review May 9, 2026 20:09
@subsetpark subsetpark closed this May 9, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant