feat(lift): extend v0 whitelist to method calls + multi-arg ctors

[TSavo]

Summary

Closes the substrate gap surfaced by ProvekIt's first self-lift run (PR #38). v0 of the rust-tests adapter accepted only single-arg or zero-arg constructor calls and rejected method calls outright. Of the 82 candidate atoms in provekit-canonicalizer, 13 lifted; 53 of the 69 skips traced to that one whitelist limitation.

The canonicalizer's load-bearing claim shape is assert_eq!(encode_jcs(&Value::object([("k", v), ...])), "<canonical>"). v0 could not reach it. Every spec-mandated byte-faithful JCS rule (sorted keys, no whitespace, escape sequences, integer formatting) was operationally enforced by tests but unreachable by the auto-lifter.

This PR widens the operand whitelist to v0.5. New shapes accepted:

• free-function call f(a, b, ...) -> Ctor("f", [args])
• method call recv.f(a, b) -> Ctor("f", [recv, a, b]) (UFCS, one level)
• reference &expr -> lift(expr) (transparent)
• cast expr as T -> lift(expr) (transparent)
• array literal [a, b] -> Ctor("array", [args])
• tuple literal (a, b) -> Ctor("tuple", [args])
• vec![a, b] macro -> Ctor("vec", [args])
• byte-string literal b"..." -> Ctor("byte_str", [str])
• binary op a OP b in operand position -> Ctor("<op>", [a, b])

Out of scope: every Rust expression, the assert!-body predicate grammar (still requires a binary comparison), format!() and other operand-position macros besides vec![], indexing/field-access/closures/blocks/ranges. assert!(h.starts_with(PREFIX)) still skips with a clean reason.

Skip-count delta

                       v0                       v0.5
rust-tests       seen=82  lifted=13  skipped=69   seen=57  lifted=41  skipped=16
rust-tests-l2    seen=11  lifted=0   skipped=11   seen=11  lifted=8   skipped=3

Total catalog members: 13 -> 49 (+36)

seen for rust-tests dropped from 82 to 57 because Layer 2 now claims 8 tests as characterization conjunctions (3-atom integer_renders_without_decimal_point, 8-atom control_characters_are_unicode_escaped, etc.); claimed tests don't re-appear in Layer 0. Combined coverage shows up in decls=49.

Catalog CID:

• v0: blake3-512:79ef1067...8632de
• v0.5: blake3-512:5725809e...71ce01

Sample IR-JSON for newly-lifted contracts

encode_simple_object_sorts_keys::0

Source:

let v = Value::object([("b", Value::integer(1)), ("a", Value::string("x"))]);
assert_eq!(encode_jcs(&v), r#"{"a":"x","b":1}"#);

IR:

{
  "Atomic": {
    "name": "=",
    "args": [
      {"Ctor": {"name": "encode_jcs", "args": [{"Var": {"name": "v"}}]}},
      {"Const": {"value": {"String": "{\"a\":\"x\",\"b\":1}"}, "sort": "String"}}
    ]
  }
}

(v lifts as a free Var because the let-binding flow is a Layer 3 future-work feature; the structural lift is faithful to the source line.)

integer_renders_without_decimal_point (Layer 2 characterization, 3-atom)

Source:

assert_eq!(encode_jcs(&Value::integer(42)), "42");
assert_eq!(encode_jcs(&Value::integer(0)),  "0");
assert_eq!(encode_jcs(&Value::integer(1)),  "1");

IR (and-conjunction of 3 atoms; one shown):

{
  "Atomic": {
    "name": "=",
    "args": [
      {"Ctor": {"name": "encode_jcs", "args": [
        {"Ctor": {"name": "Value::integer", "args": [
          {"Const": {"value": {"Int": 42}, "sort": "Int"}}
        ]}}
      ]}},
      {"Const": {"value": {"String": "42"}, "sort": "String"}}
    ]
  }
}

distinct_inputs_distinct_hashes::0

Source:

assert_ne!(blake3_512_of(b"hello"), blake3_512_of(b"world"));

IR:

{
  "Atomic": {
    "name": "≠",
    "args": [
      {"Ctor": {"name": "blake3_512_of", "args": [
        {"Ctor": {"name": "byte_str", "args": [
          {"Const": {"value": {"String": "hello"}, "sort": "String"}}
        ]}}
      ]}},
      {"Ctor": {"name": "blake3_512_of", "args": [
        {"Ctor": {"name": "byte_str", "args": [
          {"Const": {"value": {"String": "world"}, "sort": "String"}}
        ]}}
      ]}}
    ]
  }
}

This is the contract that v0 could not reach (b"" not whitelisted) and the spec rule "distinct inputs distinct hashes" is now lifted.

Lift-report.txt diff summary

• Adapter totals updated (above)
• "v0.5 whitelist extension" section added documenting newly-accepted shapes
• "Lifted contracts" enumerates 49 mementos split by Layer 0 (41) and Layer 2 (8)
• Skip taxonomy reduced from 3 categories (53 + 14 + 2) to 3 (14 assert!-body + 1 residual + 1 receiver). The 14 assert!-body skips are out of scope for this PR (separate code path); they belong in a v0.6 predicate-grammar extension.
• Spec coverage section now shows YES for sorted object keys, escape minimal set, integer plain decimal, booleans/null, distinct inputs distinct hashes (all NONE in v0)

Existing lifter tests pass

• 23 unit tests in provekit-lift-rust-tests::lib: pass
• 23 unit tests in provekit-lift-rust-tests::layer2: pass (pattern3_releases_claim_when_only_one_atom_lifts updated to use format!() as the negative shape since "hello".len() now lifts)
• 1 integration test fixture_lifts_5_skips_1_and_round_trips_through_verifier: pass (deliberately-skipped fixture moved from method-call shape to format!() shape)
• 7 unit tests + 4 integration tests in provekit-lift: pass

New positive tests added: lifts_method_call_as_ufcs_ctor (with IR-shape inspection), lifts_multi_arg_call_with_array_and_tuple (recursive ctor verification), lifts_vec_macro_as_ctor, lifts_cast_transparently, lifts_byte_string_literal, lifts_binary_op_in_operand_position.

New negative tests added: skips_format_macro_in_operand_position, skips_block_expression_in_operand_position.

Expression shapes still skipped (with reason)

• assert!(h.starts_with(PREFIX)) and assert!(matches!(c, ...)) (14 hits) — the assert! body grammar requires a top-level binary comparison; method-call results in boolean position need a v0.6 predicate-grammar extension or an IR atomic-predicate addition. Out of scope here.
• format!(...) and other macro calls in operand position (1 hit in fixture; many in real code) — explicit skip with reason "macro format!(...) in operand position not lifted in v0.5". Only vec![...] is recognized.
• Indexing, field access, closures, blocks, ranges, .await — never reached this PR; skip with the catch-all v0.5 reason.
• Layer 2 multi-statement loop bodies (3 skips) — unchanged from v0; orthogonal to operand whitelist work, deferred to Layer 2.5.

Verification

$ make self-lift-canonicalizer
>> self-lifting provekit-canonicalizer
  cid: blake3-512:5725809e7388b7a2d77c4f808a6804f053e523f1ce45a4a55e2fdfb60ef0047020d1ec5e2c46bc06ba94d31d570e82f2c6eb604619535558acd47daeba71ce01
  proof: .provekit/self-lifts/canonicalizer/blake3-512:5725809e...proof
  report: .provekit/self-lifts/canonicalizer/lift-report.txt

Two runs produce the same CID. provekit verify reports zero load errors.

A small diagnostic cargo run --example dump_self_lift -- <workspace> is included under provekit-lift/examples/ for inspecting per-adapter warnings and lifted-contract IR. Used during this PR to verify the structural fidelity of the lift; reusable for future workspace investigations.

Test plan

• cargo test --release -p provekit-lift-rust-tests (24 tests pass)
• cargo test --release -p provekit-lift (11 tests pass)
• make self-lift-canonicalizer produces v0.5 CID 5725809e... deterministically across runs
• provekit verify .provekit/self-lifts/canonicalizer returns zero load errors
• IR for 3 sample contracts inspected by hand and structurally faithful to source
• CI on this branch

🤖 Generated with Claude Code

[coderabbitai]

Warning

Rate limit exceeded

@TSavo has exceeded the limit for the number of commits that can be reviewed per hour. Please wait 4 minutes and 15 seconds before requesting another review.

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 @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

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 configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: aa993efd-4f09-49fa-877e-1ce63b00c2ef

📥 Commits

Reviewing files that changed from the base of the PR and between 01f1cb6 and b45291c.

📒 Files selected for processing (7)

• .provekit/self-lifts/canonicalizer/blake3-512:5725809e7388b7a2d77c4f808a6804f053e523f1ce45a4a55e2fdfb60ef0047020d1ec5e2c46bc06ba94d31d570e82f2c6eb604619535558acd47daeba71ce01.proof
• .provekit/self-lifts/canonicalizer/blake3-512:79ef1067621f7a3bb3ad31acd157be9ec9e087eb6aa585acd9ea6c9d0965adb02e7f1037a3146dcbc3f6a4c284796d6eadee7e0265d3eeab75791b79628632de.proof
• .provekit/self-lifts/canonicalizer/lift-report.txt
• implementations/rust/provekit-lift-rust-tests/src/layer2.rs
• implementations/rust/provekit-lift-rust-tests/src/lib.rs
• implementations/rust/provekit-lift-rust-tests/tests/round_trip.rs
• implementations/rust/provekit-lift/examples/dump_self_lift.rs

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch feat/lifter-method-call-ctor-whitelist

---

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.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Review rate limit: 0/1 reviews remaining, refill in 4 minutes and 15 seconds.}

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