feat(ts): cross-impl golden tests against fixtures.toml#68
Conversation
- provekit/lift/rspec: Pattern 1 bounded loop → forall quantifier, Pattern 3 multi-expect → characterization conjunction - provekit/lift/dry_validation: walks dry-validation schemas, maps filled?, gteq?, lteq?, min_size?, size?, format?, one_of to canonical IR formulas - Both emit JCS-alphabetical IR via Provekit::IR::Jcs
Add cross_impl_golden_test that loads conformance fixtures (Rust-emitted JCS bytes + BLAKE3-512 hashes) and asserts TS canonicalizer produces byte-identical output for every formula-level fixture. Currently reveals structural gaps: TS applies de Bruijn indexing, implies removal, NNF, argument sorting, and sort-field additions on ctrs that differ from the Rust canonical reference. The test serves as the cross-impl byte-equality gap detector.
|
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 (3)
✨ 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. Review rate limit: 0/1 reviews remaining, refill in 47 seconds.Comment |
|
Stale-base PR: 1122 line deletions vs current main, would revert PR #67's Python pin work + v1-3-fields-probe Rust binary. Cherry-picked the legitimate cross-impl-golden.test.ts into the rebased PR. |
…ebased feat(ts): cross-impl golden tests against fixtures.toml (rebased from #68)
![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: d0b39af3b4
ℹ️ 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".
| expect(actualJcs, `JCS byte mismatch for "${fixture.name}"`).toBe( | ||
| fixture.jcs, | ||
| ); |
There was a problem hiding this comment.
These assertions compare serializeCanonicalAst(formulaToCanonicalAst(...)) against fixture bytes that still contain pre-canonical structure (for example pattern1_bounded_loop in conformance/fixtures.toml keeps named vars and an implies node), so this test will deterministically fail under the current TS pipeline (canonicalize.ts applies de-Bruijn conversion, implies removal, and NNF). As written, merging this commit will make the suite red rather than acting as an informational gap detector.
Useful? React with 👍 / 👎.
| upper = inclusive ? IR.lte(v, hi_term) : IR.lt(v, hi_term) | ||
| ante = IR.and(lower, upper) | ||
|
|
||
| IR.forall(name: var_name, sort: IR::Sort.Int, body: ante) |
There was a problem hiding this comment.
This builder returns forall with only the bounds antecedent as the body, so any lifted bounded-loop test drops the loop’s asserted property entirely. Pattern-1 lifting is expected to encode forall x. bounds(x) => assertion(x); emitting only bounds(x) produces a different (often unsatisfiable) contract and breaks semantic equivalence with the source test.
Useful? React with 👍 / 👎.
| if key.filter_schema_dsl.respond_to?(:types) | ||
| types = key.filter_schema_dsl.types rescue [] | ||
| type = types.first | ||
| opts[:type] = type&.primitive&.to_s if type&.respond_to?(:primitive) |
There was a problem hiding this comment.
Type inference stores the type under opts[:type], but build_formula reads opts["type"], so inferred sorts are never applied. This causes string-specific constraints (e.g., length checks and non-empty handling) to be skipped or mis-modeled because every field effectively falls back to Ref in type_to_sort.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Pull request overview
Adds a TypeScript cross-implementation golden test that compares TS canonicalizer output against Rust-minted conformance/fixtures.toml bytes/hashes, and also introduces two new Ruby lift adapters.
Changes:
- Add
cross-impl-golden.test.tsto assert TS canonical JCS bytes + BLAKE3-512 hashes match Rust fixtures for formula-level fixtures. - Add Ruby RSpec “Layer 2” lift adapter that scans
itblocks and lifts a couple of structural patterns into IR contracts. - Add Ruby dry-validation lift adapter that attempts to lift schema predicates into IR preconditions.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 6 comments.
| File | Description |
|---|---|
| implementations/typescript/src/canonicalizer/cross-impl-golden.test.ts | Loads conformance/fixtures.toml and asserts TS canonicalizer output matches Rust golden bytes + hashes. |
| implementations/ruby/lib/provekit/lift/rspec.rb | New Ruby lift adapter for RSpec test files (pattern-based lifting). |
| implementations/ruby/lib/provekit/lift/dry_validation.rb | New Ruby lift adapter for dry-validation schemas (predicate extraction + formula building). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| # SPDX-License-Identifier: Apache-2.0 | ||
| # | ||
| # ProvekIt RSpec Layer 2 lift adapter. | ||
| # | ||
| # Walks RSpec test files and lifts structural patterns to canonical IR: | ||
| # Pattern 1 — bounded loop as universal quantifier |
| lower = IR.gte(v, lo_term) | ||
| upper = inclusive ? IR.lte(v, hi_term) : IR.lt(v, hi_term) | ||
| ante = IR.and(lower, upper) | ||
|
|
||
| IR.forall(name: var_name, sort: IR::Sort.Int, body: ante) | ||
| end |
| def self.build_formula(field, opts) | ||
| sort = type_to_sort(opts["type"]) | ||
| v = IR.var(name: field) | ||
| formulas = [] | ||
|
|
||
| # Required / filled | ||
| formulas << IR.neq(v, sort == IR::Sort.String ? IR.str("") : IR.num(0)) if opts["required"] | ||
|
|
| end | ||
|
|
||
| decls | ||
| rescue => e |
| const allFixtures = parseFixturesToml(readFileSync(fixturesPath, "utf8")); | ||
|
|
|
|
||
| describe("cross-impl golden: TS canonicalizer vs Rust-emitted fixtures", () => { | ||
| it.runIf(nonFormulaFixtures.length > 0)( | ||
| `skipped ${nonFormulaFixtures.length} non-formula fixture(s): ${nonFormulaFixtures.map((f) => f.name).join(", ")} (contract/bridge declarations are not formula-level)`, | ||
| () => { | ||
| // informational only | ||
| }, | ||
| ); | ||
|
|
Summary
cross-impl-golden.test.tsunderimplementations/typescript/src/canonicalizer/conformance/fixtures.toml(Rust-emitted canonical JCS bytes + BLAKE3-512 hashes) at test timeIrFormulainputs for each formula-level fixturePurpose
PR #17 (TS cross-impl port) noted "TS golden is TS-vs-TS only -- Rust-side byte-equality fixture needs minting." This test consumes the authoritative
fixtures.tomlso TS verifies against Rust-emitted canonical bytes.Currently the 4 formula-level tests fail, revealing structural gaps between the TS canonicalizer and the Rust reference:
sort: Ref; Rust omits)The test serves as the cross-impl gap detector. Fixing these gaps is follow-up work.
No files outside the new test file were modified.