feat(rust): self-lift provekit-canonicalizer (substrate dogfoods itself)#38
Merged
Conversation
The framework writes lifters and uses them on test fixtures; this is
the first time it lifts itself. `provekit-lift` runs against the
`provekit-canonicalizer` crate and emits a durable `.proof` plus a
honest skip taxonomy at `.provekit/self-lifts/canonicalizer/`.
Outcome (rust-tests adapter on canonicalizer source):
files_scanned: 9
rust-tests seen=82 lifted=13 skipped=69
rust-tests-l2 seen=11 lifted=0 skipped=11
proptest/contracts/kani/prusti/creusot/flux/quickcheck/verus: zero
(the crate uses no external annotation library)
13 contract mementos lifted: prefix_constant, deterministic_across_calls,
empty-input vector pin, count=128, Unicode round-trip witnesses, etc.
All survive `provekit verify` clean.
Skip causes (honest gap-finding):
53 hits expression shape outside v0 whitelist (method calls,
constructors, multi-arg calls)
14 hits assert! body not a binary comparison
2 hits byte-string literals (b"") not in the v0 literal set
Spec coverage (canonicalization-grammar.md): partial. The lifter
reaches counter and identifier equalities, the prefix constant, and
a handful of literal pins. The byte-faithful claims (sorted keys, no
whitespace, escape sequences, integer formatting) all skip because
every test on the lhs is encode_jcs(&v), a method call. That is the
operationally enforced bulk of the canonicalizer's invariants and it
is currently unreachable by the auto-lifter; surfacing the gap is
the point.
Idempotent: default seed [0x42; 32] produces a byte-deterministic
catalog CID (verified across two runs into separate temp dirs).
make self-lift-canonicalizer
regenerates the .proof at the same CID. NOT wired into make
conformance because this is an experiment, not core conformance.
Cross-impl leverage: the same skip patterns will hit the TS, Go, C++
canonicalizers when their respective lifters point at their
canonicalizer crates. The shape gap is in the lifter's expression
whitelist, not in any one language's idioms.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
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 (4)
✨ 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 27 minutes and 9 seconds.Comment |
There was a problem hiding this comment.
Pull request overview
This PR adds a self-lift experiment for the Rust canonicalizer crate, checking in the resulting lifted .proof artifact and a human-readable report so the repository can track what provekit-lift currently reaches on first-party canonicalizer tests. It extends the top-level build orchestration with a dedicated make target and updates ignore rules so the experiment artifact can live in source control.
Changes:
- Adds
make self-lift-canonicalizerand help text for running the Rust lifter againstimplementations/rust/provekit-canonicalizer. - Checks in a generated self-lift
.proofbundle plus a companionlift-report.txtsummarizing lifted and skipped assertions. - Updates
.gitignoreto allow versioning self-lift.proofartifacts under.provekit/self-lifts/.
Reviewed changes
Copilot reviewed 3 out of 4 changed files in this pull request and generated 6 comments.
| File | Description |
|---|---|
| Makefile | Adds help text and a new self-lift experiment target for the Rust canonicalizer crate. |
| .provekit/self-lifts/canonicalizer/lift-report.txt | Adds a checked-in textual report describing lifted contracts, skip taxonomy, and spec coverage. |
| .provekit/self-lifts/canonicalizer/blake3-512:79ef1067621f7a3bb3ad31acd157be9ec9e087eb6aa585acd9ea6c9d0965adb02e7f1037a3146dcbc3f6a4c284796d6eadee7e0265d3eeab75791b79628632de.proof | Adds the generated proof envelope produced by the self-lift run. |
| .gitignore | Unignores self-lift .proof artifacts and documents that they are intended to be committed. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+264
to
+271
| @out=$$($(PROVEKIT_LIFT) \ | ||
| --workspace implementations/rust/provekit-canonicalizer \ | ||
| --target-dir $(SELF_LIFT_DIR) --quiet); \ | ||
| echo " cid: $$out"; \ | ||
| test -f $(SELF_LIFT_DIR)/$$out.proof || \ | ||
| (echo "FAIL: lifter did not write $(SELF_LIFT_DIR)/$$out.proof" && exit 1); \ | ||
| echo " proof: $(SELF_LIFT_DIR)/$$out.proof" | ||
| @echo " report: $(SELF_LIFT_DIR)/lift-report.txt" |
| (object-key Unicode preservation witness) | ||
|
|
||
| non_ascii_strings_round_trip_byte_faithful::0 | ||
| i = "≥" |
Comment on lines
+76
to
+80
| jcs = ? | ||
| realistic_envelope_shape_round_trips::2 | ||
| cid = ? | ||
| realistic_envelope_shape_round_trips::3 | ||
| cid_again = ? |
Comment on lines
+84
to
+85
| a = b | ||
| (avalanche regression test, lifted as identifier-equality) |
Comment on lines
+187
to
+189
| bodies. Three of the canonicalizer's parameterized loops use a | ||
| three-line shape (input -> let -> assert) and skip cleanly with | ||
| a structured warning. |
Comment on lines
+18
to
+27
| proptest seen=0 lifted=0 skipped=0 | ||
| contracts seen=0 lifted=0 skipped=0 | ||
| kani seen=0 lifted=0 skipped=0 | ||
| prusti seen=0 lifted=0 skipped=0 | ||
| creusot seen=0 lifted=0 skipped=0 | ||
| flux seen=0 lifted=0 skipped=0 | ||
| quickcheck seen=0 lifted=0 skipped=0 | ||
| verus seen=0 lifted=0 skipped=0 | ||
| rust-tests seen=82 lifted=13 skipped=69 | ||
| rust-tests-l2 seen=11 lifted=0 skipped=11 |
This was referenced May 2, 2026
TSavo
added a commit
that referenced
this pull request
May 23, 2026
…from lift IR Proves the substrate's lift IR carries enough data to emit a complete java compilation unit (interface, constants, @boundary stubs) WITHOUT hand-writing the wrapper at integration time. Reads provekit lift --library-bindings output, extracts bind-lift-entry signatures, maps rust types via a small source-aliases table (the substrate-honest version walks the kit's catalog), emits: - package + imports - class header + static fields/constants - AdapterLifter interface - @boundary primitive stubs with byte-identical signatures to source The substrate-honest version of this script is the java realize plugin emitting the same when invoked over the whole IR (via the provekit.plugin.assemble RPC method — pending task #38). This Python script is the proof of concept: the IR carries the data; only the emission needs threading through cmd_lower or a new assemble RPC. What this retires: the hand-written CrossPlatform.java wrapper in the demo's test harness — the LAST hand-written java code in the rust → java → rust cycle. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 23, 2026
…es hand-written boundary code
The python wrapper-emitter is now retired. cmd_lower --target java
auto-emits the full java compilation unit when boundary entries are
present in the lift IR:
package com.provekit.crossplatform;
imports (Jackson, runtime carriers, java.nio.file.Path)
public final class CrossPlatform {
static final ObjectMapper MAPPER;
static String PLUGIN_VERSION; ... (constants)
public interface AdapterLifter { name(); surface(); lift(...); }
// @boundary primitives auto-emitted from rust @boundary declarations:
public static <Type> json_parse(String s) { throw UnsupportedOp; }
... (9 primitives, signatures derived via map_rust_type_to_java)
// @sugar functions follow (each as a static method inside the class):
public static JsonNode ok_response(...) { ... }
...
}
CHANGES:
- NamedTermDocument gains boundary_entries: Vec<Json> field (defaults
empty, populated from bind-lift-entry records in the IR).
- named_term_document_from_ir_document collects bind-lift-entry items
that aren't also @sugar (i.e. true @boundary functions).
- lower_named_document detects target=="java" + non-empty boundary_entries
and emits emit_java_module_preamble() before, '}' after.
- map_rust_type_to_java handles &str, Value, [u8;N], Result<T,E>, etc.
- strip_transported_class_wrapper peels per-function 'final class XxxTransported'
wrappers so the @sugar methods sit directly inside CrossPlatform.
EMPIRICAL: provekit lower --target java now emits a single compilation
unit with package + imports + CrossPlatform class + 9 @boundary stubs +
all @sugar methods. The python wrapper-emitter script is retired (kept
as proof-of-concept demonstration).
Substrate-honest note: this lives in rust cmd_lower because the
provekit.plugin.assemble RPC method-shape is still pending (#38). The
ideal home is the java realize plugin (it owns the target's file
layout). Moving this code there is a future refactor; the current shape
is functional and demonstrates the substrate emits its own wrapper.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Sir's framing
The framework writes lifters and uses them on test fixtures; this is the first time it lifts itself. The canonicalizer is the right starting point because every CID in the system hashes over JCS-canonical bytes the canonicalizer produces. If the canonicalizer is wrong, everything is wrong; it is the substrate's first invariant.
What the Rust lifter actually does
provekit-lift(crateimplementations/rust/provekit-lift/) walks a Rust workspace, parses every.rsfile withsyn, dispatches each parsed file to nine adapter crates, collectsContractDeclvalues, mints each as a signed contract memento viaprovekit_claim_envelope::mint_contract, and bundles them into a single.proofenvelope addressed by its BLAKE3-512 CID.Annotation sources the lifter reads:
proptest! { #[test] fn ... }blocks (adapterproptest)#[contracts::requires]/#[contracts::ensures]attrs (contracts)kani::proof/prusti/creusot/flux/verusattrs (one adapter each)#[quickcheck](quickcheck)#[test]and#[tokio::test]functions whose bodies containassert!/assert_eq!/assert_ne!/assert_matches!(rust-testsLayer 0)for x in lo..hi { assert!(...) }bounded loops, helper-function inlining, multi-assertion characterization (rust-testsLayer 2)Outputs: a
<cid>.prooffile (deterministic CBOR) under the requested target dir. CLI flags:provekit-lift --workspace <dir> --target-dir <out>(direct invocation)cargo provekit-lift ...(Cargo subcommand form)provekit-lift --rpc(NDJSON-on-stdio plugin mode)The lifter has no
--configflag; it picks up every.rsfile under--workspace.How I ran it
Exact command:
Output (verbatim):
Determinism: confirmed across two runs into separate temp dirs (default seed
[0x42; 32]); both produced the same CID byte for byte.What got lifted (13 contract mementos)
Each name is
<test_fn>::<assert_index>. Atom shape is a single binary comparison whose operands are identifiers, integer/string literals, or single-arg ctor calls.prefix_constant_matches_spec::0BLAKE3_512_PREFIX = PREFIX(the spec literal "blake3-512:")cid_string_form_for_empty_is_well_known::0cid_regex_compliance::0count = 128(hex character count)deterministic_across_calls::0a = b(identity of two same-input calls)cid_distinguishes_byte_strings_from_text::0blake3_512_hex(s) = blake3_512_of(b)(str/bytes parity)mixed_ascii_and_unicode_preserved::0encoded = "x \u{2265} 0"(UTF-8 round-trip witness)unicode_in_object_key_and_value::0encoded = '{"name":"\u{2265}"}'non_ascii_strings_round_trip_byte_faithful::0,::2\u{2265}and\u{65E5}\u{672C}\u{8A9E}realistic_envelope_shape_round_trips::1,::2,::3single_bit_flip_changes_most_output_bits::0All 13 survive
provekit verifyclean (zero callsites, zero load errors; this is a pure-contract bundle, no bridges).What couldn't be lifted (69 + 11 = 80 skips, honest gap-finding)
rust-testsadapter (69 skips):assert_eq!(encode_jcs(&Value::object([...])), "<canonical>"). The lhs is a method call; the rhs's operand is a multi-arg constructor. Both fall outside the "identifier, literal, single-arg ctor" whitelist.assert!body must be a binary comparison. The CID-shape tests useassert!(matches!(...))andassert!(h.starts_with(PREFIX))heavily.b"") are not in the v0 literal set, soassert_eq!(blake3_512_hex(s), blake3_512_of(b""))skips.rust-tests-layer2adapter (11 skips):for input in [...] { let h = ...; let hex = ...; assert_eq!(...) }exceeds the v0 single-stmt cap.encode_jcs(&v) == "..."shape, none of which Layer 0 can lift; Layer 2 then releases all eight tests back to Layer 0, which skips them).Spec coverage against
protocol/specs/2026-04-30-canonicalization-grammar.md:\u00XXescapes for U+0000..U+001Fcount=128, empty-vector pin)blake3-512:b""not whitelisted)Full per-skip-reason taxonomy with file paths is in
.provekit/self-lifts/canonicalizer/lift-report.txt.Make target
builds
provekit-lift(release), wipes any prior.proofunder.provekit/self-lifts/canonicalizer/, re-runs the lift, and writes the same CID. Idempotent. NOT wired intomake conformanceormake ci; this is an experiment, not core conformance, and the task explicitly cautioned against pinning a self-lift CID into the gate while the lifter is still v0.Cross-impl leverage
The same skip patterns will surface on the TS, Go, and C++ canonicalizer test files when their respective lifters point at them, because the test idiom is the same across kits:
expect(encodeJcs(...)).toEqual("..."),assert.Equal(t, EncodeJcs(...), "..."),EXPECT_EQ(encode_jcs(...), "..."). The shape gap is in the lifter's expression whitelist, not in any one language's idioms. Concrete next moves once the v0 whitelist grows (single-arg method-call lhs, multi-arg ctor rhs):provekit-lift-vitestagainstimplementations/typescript/src/canonicalizer/provekit-lift-go-testsagainstimplementations/go/.../canonicalizer/implementations/cpp/provekit/canonicalizer/Each will recover roughly the same shape of mementos this run produced and skip roughly the same shape of tests with the same structured warnings.
Don't-touch list (followed)
provekit-canonicalizer/source. The point was to surface what the lifter reaches as-is.provekit-self-contracts(it ships a pinned CID undermake conformance; conflating the experiment with core conformance would have wrecked it).protocol/specs/text..github/workflows/.Test plan
make self-lift-canonicalizersucceeds and prints the same CID across two runsprovekit verify <proof>loads the lifted catalog clean (0 errors, 0 violations)git statusclean after the make target re-runs (idempotent).provekit/self-lifts/canonicalizer/lift-report.txtand skim the skip taxonomy