feat(walk): C.8 aliasing + C.9 Outlives — #384 Tier C gap closure#419
feat(walk): C.8 aliasing + C.9 Outlives — #384 Tier C gap closure#419TSavo wants to merge 7 commits into
Conversation
…int AliasingMemento for &mut formals (closes #409)
|
Warning Rate limit exceeded
To continue reviewing without waiting, purchase usage credits in the billing tab. ⌛ 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)
WalkthroughThis pull request introduces aliasing analysis and region extraction to the provekit-walk lifter. It adds a new ChangesAliasing Analysis & Region Extraction
Sequence DiagramsequenceDiagram
participant Lifter as Lifter (llbc_lift)
participant Aliasing as Aliasing Module
participant TypeDecls as Type Declarations
participant Contract as Contract
participant Canon as Canonical (JCS)
Lifter->>Aliasing: has_unsafecell_transitive(formal_ty, type_decls)
Aliasing->>TypeDecls: adt_decl_matches_id(decl, adt_id)
Aliasing-->>Lifter: bool (interior mutability detected?)
Lifter->>Aliasing: is_shared_ref_charon_ty(ty), is_mut_ref_charon_ty(ty)
Aliasing-->>Lifter: bool (reference kind)
Lifter->>Lifter: Pair formals by ref type<br/>Detect interior-mut aliasing<br/>Auto-mint Disjoint mementos
Lifter->>Contract: FunctionContractMemento {<br/> auto_minted_mementos,<br/> formal_regions,<br/> return_region,<br/> effects: [PossibleAliasing, ...]<br/>}
Contract->>Contract: check_aliasing_discharged()<br/>Verify mementos cover<br/>PossibleAliasing pairs
Contract->>Canon: build_memento_value(contract)<br/>→ build_value(...,<br/> auto_minted_mementos)
Canon->>Canon: aliasing_mementos_to_value(mementos)<br/>JCS serialize each memento
Canon-->>Contract: Arc<Value> (canonical JSON)
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related issues
Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ 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. Comment |
![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: 5a14c6cdf5
ℹ️ 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".
| } | ||
| } | ||
| } | ||
| return false; |
There was a problem hiding this comment.
has_unsafecell_transitive returns false for an ADT after checking only its own name and generic arguments, but it never walks the ADT's declared field types from type_decls. That means types like struct S { c: Cell<u32> } are misclassified as non-interior-mutable unless S itself is one of the hardcoded wrapper names, so Effect::PossibleAliasing will be missed for shared refs to such structs.
Useful? React with 👍 / 👎.
| // PossibleAliasing is discharged by auto_minted_mementos in the | ||
| // contract bundle; the substrate verifier checks these before | ||
| // composition. No pool check at this level. | ||
| Effect::PossibleAliasing { .. } => {} |
There was a problem hiding this comment.
check_opacity_effects treats Effect::PossibleAliasing as already discharged (empty branch), and compose_function_contracts_checked also whitelists it as non-blocking, so composition succeeds even when no aliasing mementos were provided. This contradicts the intended refusal semantics for unresolved aliasing and effectively disables enforcement for the new effect path.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Pull request overview
This PR extends provekit-walk’s Rust LLBC lifter to surface potential aliasing hazards as an explicit effect (Effect::PossibleAliasing) and to derive (auto-mint) disjointness evidence for &mut formal pairs via an AliasingMemento, with the intent that the substrate can refuse composition unless aliasing is discharged.
Changes:
- Added a new aliasing analysis module intended to detect interior mutability transitively from Charon type JSON.
- Introduced
Effect::PossibleAliasing,AliasingMemento/AliasingStatus, and anauto_minted_mementosfield onFunctionContractMemento. - Updated LLBC lifting to (a) emit
PossibleAliasingfor shared refs with interior mutability and (b) auto-mintDisjointmementos for&mut-formal pairs; updated marriage classification and demo formatting accordingly.
Reviewed changes
Copilot reviewed 7 out of 7 changed files in this pull request and generated 6 comments.
Show a summary per file
| File | Description |
|---|---|
| implementations/rust/provekit-walk/src/aliasing.rs | New helper intended to detect interior mutability through type graphs (with cycle detection). |
| implementations/rust/provekit-walk/src/contract.rs | Adds aliasing effect + memento types and threads auto_minted_mementos through the contract struct and composition gating logic. |
| implementations/rust/provekit-walk/src/llbc_lift.rs | Emits PossibleAliasing from formal scans and auto-mints Disjoint aliasing mementos for &mut pairs. |
| implementations/rust/provekit-walk/src/marriage.rs | Treats PossibleAliasing as an LLBC-only “BorrowState” layer difference when formulas match. |
| implementations/rust/provekit-walk/src/lib.rs | Exposes the new aliasing module. |
| implementations/rust/provekit-walk/src/bin/walk_demo.rs | Prints possible_aliasing(...) in effect summaries. |
| implementations/rust/provekit-walk/src/llbc_calls.rs | Updates test contract construction to include the new auto_minted_mementos field. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // Adt: recurse into fields | ||
| if let Some(adt) = inner.get("Adt") { | ||
| let id = adt.get("id"); | ||
| let adt_id = id.and_then(|i| i.as_u64()).or_else(|| { | ||
| id.and_then(|i| i.get("Adt")).and_then(|a| a.as_u64()) | ||
| }); | ||
|
|
||
| // Check the ADT's own name against interior-mut set | ||
| if let Some(type_name) = adt_name_for_id(type_decls, adt_id) { | ||
| if INTERIOR_MUT_TYPE_NAMES.contains(&type_name.as_str()) { | ||
| return true; | ||
| } | ||
| } | ||
|
|
||
| // Cycle detection | ||
| if let Some(aid) = adt_id { | ||
| if !visited.insert(aid) { | ||
| return false; // already visited, no interior mut found | ||
| } | ||
| } | ||
|
|
||
| // Recurse into generic type params | ||
| if let Some(types_arr) = adt | ||
| .get("generics") | ||
| .and_then(|g| g.get("types")) | ||
| .and_then(|t| t.as_array()) | ||
| { | ||
| for t in types_arr { | ||
| // Wrap in Untagged for the recursive call | ||
| let mut map = serde_json::Map::new(); | ||
| map.insert("Untagged".to_string(), t.clone()); | ||
| let wrapped = Value::Object(map); | ||
| if has_unsafecell_transitive(&wrapped, type_decls, visited) { | ||
| return true; | ||
| } | ||
| } | ||
| } | ||
| return false; | ||
| } |
| fn adt_name_for_id(type_decls: Option<&Value>, adt_id: Option<u64>) -> Option<String> { | ||
| let tds = type_decls?.as_array()?; | ||
| let target = adt_id?; | ||
| for td in tds { | ||
| let idx = td.get("def_id")?.get("index")?.as_u64()?; | ||
| if idx == target { | ||
| let name_arr = td.get("item_meta")?.get("name")?.as_array()?; | ||
| for seg in name_arr.iter().rev() { | ||
| if let Some(ident_arr) = seg.get("Ident").and_then(|v| v.as_array()) { | ||
| if let Some(s) = ident_arr.first().and_then(|v| v.as_str()) { | ||
| return Some(s.to_string()); | ||
| } | ||
| } | ||
| } | ||
| } | ||
| } | ||
| None |
| // Wrap in Untagged for the recursive call | ||
| let mut map = serde_json::Map::new(); | ||
| map.insert("Untagged".to_string(), t.clone()); | ||
| let wrapped = Value::Object(map); | ||
| if has_unsafecell_transitive(&wrapped, type_decls, visited) { | ||
| return true; |
| // PossibleAliasing is discharged by auto_minted_mementos in the | ||
| // contract bundle; the substrate verifier checks these before | ||
| // composition. No pool check at this level. | ||
| Effect::PossibleAliasing { .. } => {} |
| #[derive(Debug, Clone)] | ||
| pub struct FunctionContractMemento { | ||
| pub fn_name: String, | ||
| pub formals: Vec<String>, | ||
| pub formal_sorts: Vec<Sort>, | ||
| pub return_sort: Sort, | ||
| pub pre: IrFormula, | ||
| pub post: IrFormula, | ||
| pub body_cid: Option<String>, | ||
| pub effects: EffectSet, | ||
| pub locus: Locus, | ||
| pub canonical_bytes: Vec<u8>, | ||
| pub cid: String, | ||
| pub auto_minted_mementos: Vec<AliasingMemento>, | ||
| } |
| impl AliasingMemento { | ||
| pub fn to_jcs_value(&self) -> Arc<Value> { | ||
| Value::object([ | ||
| ("kind", Value::string("AliasingMemento")), | ||
| ("formal_a", Value::string(self.formal_a.clone())), | ||
| ("formal_b", Value::string(self.formal_b.clone())), | ||
| ("status", Value::string(self.status.as_str())), | ||
| ]) |
|
Review summary on this PR before merge: 4-5 P1 soundness / substrate-correctness issues from chatgpt-codex + Copilot. P1: Aliasing detection misses interior mutability inside ADT fields. P1: PossibleAliasing whitelisted as discharged in composition. P1: Memento CID doesn't commit to auto-minted aliasing evidence (substrate-correctness). P1: AliasingMemento kind violates codebase kebab-case convention. P1: adt_name_for_id def_id-shape mismatch for local decls. P1: Untagged double-wrapping in generic recursion. These are correctness issues, not editorial. Three of them (whitelisted discharge, missing CID commitment, ADT-field traversal gap) defeat the PR's stated purpose. Recommend addressing all six inline before merge. |
|
Holding this PR: not merging until the P1s land. One framing note for whoever picks it up. Order of priority within the six. The six P1s split into two architectural layers, not one. Five are mechanism-level (interior-mutability traversal, def_id shape, Untagged wrapping, kebab-case kind, opacity-discharge whitelist). One is substrate-level: the auto_minted_mementos field is not in the canonical Value, so the contract CID does not commit to it. This is the only one that defeats the substrate's federation property: two parties holding the same content-addressed contract can disagree on what aliasing was minted, because the bytes that hash do not include the auto-minted record. The five mechanism-level concerns are corrigible inside the existing module surface. The substrate-level one is the architecture call. Fix it first; the others fall into place around it. Concrete shape for the canonical-Value fix (P1c). Look at how other multi-field memento variants are canonicalized in If The kebab-case decision (P1d) is now-or-never. Once mementos with The discharge whitelist (P1b) is the test that proves the effect is doing work. If The other three (P1a, P1e, P1f) are tractable in an afternoon. ADT field traversal (P1a): walk Add tests for each fix; the module's doc comment makes promises that the current implementation doesn't keep, and the tests are how those promises stop being aspirational. I won't be the one merging this. Whoever owns the branch should push the revisions and re-request review. |
…tagged wrap, CID commitment, kebab-case, discharge gating
…s from Charon LLBC (closes #410) Core implementation: - Region extraction from Charon generics.regions table - Per-formal region tracking via formal_regions + return_region - Outlives emission from Charon regions_outlive where-clauses - Region terms use @region: prefix for name collision avoidance - Region facts injected as conjuncts into lifted pre formula - sort_translate: extract_region_name for Ref types Fixtures: region_id, region_longer (where 'b: 'a), region_two_unrelated, region_static (7 hand-crafted LLBC files mirroring Charon output) Tests: 7 passing (region extraction, Outlives emission, static regions, non-reference formals None, JCS determinism, marriage classification) Also fixed C.8 build_memento_value auto_minted_mementos argument.
TSavo
changed the title
TSavo
force-pushed
the
feat/384-c8-aliasing
branch
from
7d0fc14 to
cc6ff12
Compare
Re-review Summary: PR #419 (7d0fc14 post-rebase)Head commit verified: P1 Verification — All 6 Prior Issues AddressedP1a (has_unsafecell_transitive): PASS
P1b (PossibleAliasing defeater): PASS
P1c (Memento CID commits to auto_minted_mementos): PASS
P1d (kind kebab-case): PASS
P1e (adt_name_for_id def_id shapes): PASS
P1f (Untagged double-wrapping): PASS
C.9 Review — Outlives + Region FactsScope expansion confirmed: PR now closes both #409 (C.8 aliasing) and #410 (C.9 Outlives). Title accurately reflects this. C.9 Implementation:
Potential C.9 issue (minor):
Test Coverage1278 lines added across 8 test fixture files (4 LLBC + 4 Rust):
Coverage gap: Tests use hand-crafted Charon fixtures, not MementoPool integration. Per #427 feedback, verify that end-to-end tests with a real CI Status
No failures detected. Rebase conflict resolution appears clean. RecommendationMerge — all 6 prior P1s confirmed addressed post-rebase. C.9 implementation is thorough. Two minor follow-ups (HRTB fixture coverage, MementoPool integration test) can be deferred to post-merge tracking issues; they do not block correctness. Awaiting CI green light (prove + conformance gates). |
CI failure on
|
After merge of #400 (which added Effect::Drop to the enum), this branch needs the Drop variant fully wired: - Effect::Drop variant definition + docs - to_value() serialization - dyn_id() content-addressing - OpacityError::DropNotDischarged variant - Discharge check in EffectSet::validate() - walk_demo summary formatting Closes #419 merge conflict.
Fix appliedThe CI failure on the original run was due to incomplete merging of #400 (which added Fixed in commit fa79f02:
Verification:
Ready for merge. |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 9
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@implementations/rust/provekit-walk/src/aliasing.rs`:
- Around line 41-47: The cycle detection currently uses the global `visited` set
keyed only by `adt_id`, causing sibling branches with different type arguments
(e.g., `Wrapper<u32>` vs `Wrapper<Cell<u32>>`) to be skipped; make the check
path-local by either removing the `adt_id` from `visited` when unwinding this
visit or by changing the key to the fully instantiated type (include type
parameters) instead of just `def_id`; update the logic around the `if let
Some(aid) = adt_id { if !visited.insert(aid) { return false } }` block in
aliasing.rs and ensure `PossibleAliasing` detection now considers the per-path
instantiation so generic wrappers with interior-mut types are not
under-reported.
In `@implementations/rust/provekit-walk/src/contract.rs`:
- Around line 200-208: to_jcs_value() is emitting alias pairs in the original
order which leads to non-deterministic hashes/CIDs because (a,b) and (b,a) are
considered equivalent by check_aliasing_discharged(); update to_jcs_value() (and
the related aliasing_mementos_to_value() comparator) to canonicalize the pair
ordering (e.g., sort the two formals lexicographically) before constructing the
JCS Value and ensure the comparator/sort also includes the status field so
identical-name duplicates are deterministic, keeping the symbol names
to_jcs_value(), aliasing_mementos_to_value(), and check_aliasing_discharged() as
points of change.
- Around line 353-355: FunctionContractMemento now contains new lifetime
metadata fields formal_regions and return_region but build_value() and
build_memento_value() do not serialize them, so the canonical contract bytes
(and resulting CID) omit lifetime data; update build_value() and
build_memento_value() to include serializing
FunctionContractMemento.formal_regions and .return_region into the canonical
contract/memento representation (follow the existing ordering/encoding used for
other fields) so that the LLBC-enriched regions become part of the contract
identity.
- Around line 394-423: The check_aliasing_discharged implementation currently
only inspects self.auto_minted_mementos and therefore never considers
verifier-supplied aliasing proofs; change it to query the canonical memento
pool/lookup abstraction (OpacityMementoLookup) used elsewhere in opacity rather
than directly iterating auto_minted_mementos: replace the coverage check in
check_aliasing_discharged with a call into the lookup (or pool) API (e.g., a
method like lookup.has_aliasing_memento(formal_a, formal_b) or equivalent) so
verifier-provided mementos are considered, and apply the same refactor to the
analogous checks mentioned in the other spots (the other aliasing-discharge
loops at the two similar sites) so all aliasing discharge paths go through the
shared lookup abstraction.
In `@implementations/rust/provekit-walk/src/llbc_lift.rs`:
- Around line 398-406: pre_with_regions currently merges region_facts into the
pre contract but post_formula is finalized earlier so Outlives facts are not
propagated to the return-side; mirror the same merging logic for the post
contract: build a post_with_regions by checking if region_facts.is_empty() then
clone post_formula, else if post_formula matches IrFormula::Atomic { name ==
"true", args.is_empty() } then use simplify_conjunction(region_facts), else
create operands = vec![post_formula.clone()] ; operands.extend(region_facts) and
set IrFormula::And { operands }; then use post_with_regions where post_formula
was previously used so Outlives facts are preserved at return.
In `@implementations/rust/provekit-walk/src/marriage.rs`:
- Around line 215-223: The Identical-agreement branch detects LLBC-only
PossibleAliasing but marry() still begins from ast.clone(), dropping LLBC borrow
metadata; change marry() so when you return
LayerAgreement::LlbcExtra(LlbcExtraCategory::BorrowState) you build the merged
contract by starting from a merge of ast and llbc (not ast.clone()),
deterministically combining EffectSet (merge llbc.effects into the
merged.effects with a stable ordering), and also copying LLBC-only fields
(auto_minted_mementos, the new region fields, and any PossibleAliasing effects)
into the merged contract; update or add tests around
marry()/LayerAgreement::LlbcExtra and Effect::PossibleAliasing to cover married
contracts that must preserve LLBC borrow evidence.
In `@implementations/rust/provekit-walk/tests/fixtures/region_longer.llbc`:
- Around line 57-66: The fixture encodes the outlives pair in the wrong
direction: in the Rust source longer<'a, 'b: 'a> region index 1 ('b) outlives
index 0 ('a), so the "regions_outlive" pair should be [ { "Body": 1 }, { "Body":
0 } ] not [ { "Body": 0 }, { "Body": 1 } ]; update the regions_outlive entry in
the fixture so the first element is Body(1) and the second is Body(0) so that
the lifter (llbc_lift.rs) will emit Outlives(region_a, region_b) with the
longer-lived region as the first argument and make the test
region_longer_emits_outlives_b_a reflect the intended direction.
In `@implementations/rust/provekit-walk/tests/fixtures/region_static.llbc`:
- Around line 228-271: Statement id=4 in the fixture for function give_static
incorrectly assigns a plain Copy of local 1 (type u32) into local 0 (type
&'static u32); change the second Assign element for statement id=4 so that it
produces a reference-to-promoted-constant (i.e., a Ref/Promoted or otherwise a
Literal reference with Static=true) rather than a Copy of an integer: update the
part that currently emits "Use: Copy: Local 1" to emit a reference/Literal that
matches local 0's type (&'static u32), ensuring the Assign for local 0 is
structurally a Ref to a static/promoted u32 consistent with the function
give_static signature.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 21439c5d-4919-4863-867f-72c60772abb1
📒 Files selected for processing (17)
implementations/rust/provekit-walk/src/aliasing.rsimplementations/rust/provekit-walk/src/bin/walk_demo.rsimplementations/rust/provekit-walk/src/contract.rsimplementations/rust/provekit-walk/src/lib.rsimplementations/rust/provekit-walk/src/llbc.rsimplementations/rust/provekit-walk/src/llbc_calls.rsimplementations/rust/provekit-walk/src/llbc_lift.rsimplementations/rust/provekit-walk/src/marriage.rsimplementations/rust/provekit-walk/src/sort_translate.rsimplementations/rust/provekit-walk/tests/fixtures/region_id.llbcimplementations/rust/provekit-walk/tests/fixtures/region_id.rsimplementations/rust/provekit-walk/tests/fixtures/region_longer.llbcimplementations/rust/provekit-walk/tests/fixtures/region_longer.rsimplementations/rust/provekit-walk/tests/fixtures/region_static.llbcimplementations/rust/provekit-walk/tests/fixtures/region_static.rsimplementations/rust/provekit-walk/tests/fixtures/region_two_unrelated.llbcimplementations/rust/provekit-walk/tests/fixtures/region_two_unrelated.rs
| // Cycle detection | ||
| if let Some(aid) = adt_id { | ||
| if !visited.insert(aid) { | ||
| return false; // already visited, no interior mut found | ||
| } | ||
| } | ||
|
|
There was a problem hiding this comment.
Make the cycle check path-local, not global.
visited is never unwound, so a sibling branch that reuses the same ADT id with different type arguments can be skipped incorrectly. For example, if one field visits Wrapper<u32> first, a later Wrapper<Cell<u32>> will hit Line 43 and return false before inspecting the interior-mutating generic. That under-reports PossibleAliasing for generic wrappers.
Use path-local cycle detection here: either remove the ADT id from visited on unwind, or key the visit by the fully instantiated type rather than only by def_id.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/aliasing.rs` around lines 41 - 47, The
cycle detection currently uses the global `visited` set keyed only by `adt_id`,
causing sibling branches with different type arguments (e.g., `Wrapper<u32>` vs
`Wrapper<Cell<u32>>`) to be skipped; make the check path-local by either
removing the `adt_id` from `visited` when unwinding this visit or by changing
the key to the fully instantiated type (include type parameters) instead of just
`def_id`; update the logic around the `if let Some(aid) = adt_id { if
!visited.insert(aid) { return false } }` block in aliasing.rs and ensure
`PossibleAliasing` detection now considers the per-path instantiation so generic
wrappers with interior-mut types are not under-reported.
| impl AliasingMemento { | ||
| pub fn to_jcs_value(&self) -> Arc<Value> { | ||
| Value::object([ | ||
| ("kind", Value::string("aliasing-memento")), | ||
| ("formal_a", Value::string(self.formal_a.clone())), | ||
| ("formal_b", Value::string(self.formal_b.clone())), | ||
| ("status", Value::string(self.status.as_str())), | ||
| ]) | ||
| } |
There was a problem hiding this comment.
Canonicalize aliasing pairs before hashing them.
check_aliasing_discharged() already treats (a,b) and (b,a) as the same relation, but to_jcs_value() preserves whichever order the producer emitted and aliasing_mementos_to_value() sorts on those raw fields. Two equivalent bundles can therefore discharge identically yet produce different autoMintedMementos bytes/CIDs. Normalize the pair before encoding/sorting, and include status in the comparator so same-name duplicates are deterministic.
Proposed fix
impl AliasingMemento {
+ fn canonical_pair(&self) -> (&str, &str) {
+ if self.formal_a <= self.formal_b {
+ (&self.formal_a, &self.formal_b)
+ } else {
+ (&self.formal_b, &self.formal_a)
+ }
+ }
+
pub fn to_jcs_value(&self) -> Arc<Value> {
+ let (formal_a, formal_b) = self.canonical_pair();
Value::object([
("kind", Value::string("aliasing-memento")),
- ("formal_a", Value::string(self.formal_a.clone())),
- ("formal_b", Value::string(self.formal_b.clone())),
+ ("formal_a", Value::string(formal_a.to_string())),
+ ("formal_b", Value::string(formal_b.to_string())),
("status", Value::string(self.status.as_str())),
])
}
}
fn aliasing_mementos_to_value(mementos: &[AliasingMemento]) -> Arc<Value> {
let mut sorted: Vec<&AliasingMemento> = mementos.iter().collect();
sorted.sort_by(|a, b| {
- a.formal_a
- .cmp(&b.formal_a)
- .then_with(|| a.formal_b.cmp(&b.formal_b))
+ let (a1, a2) = a.canonical_pair();
+ let (b1, b2) = b.canonical_pair();
+ a1.cmp(b1)
+ .then_with(|| a2.cmp(b2))
+ .then_with(|| a.status.as_str().cmp(b.status.as_str()))
});
let items: Vec<Arc<Value>> = sorted.iter().map(|m| m.to_jcs_value()).collect();
Value::array(items)
}Also applies to: 404-411, 544-552
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/contract.rs` around lines 200 - 208,
to_jcs_value() is emitting alias pairs in the original order which leads to
non-deterministic hashes/CIDs because (a,b) and (b,a) are considered equivalent
by check_aliasing_discharged(); update to_jcs_value() (and the related
aliasing_mementos_to_value() comparator) to canonicalize the pair ordering
(e.g., sort the two formals lexicographically) before constructing the JCS Value
and ensure the comparator/sort also includes the status field so identical-name
duplicates are deterministic, keeping the symbol names to_jcs_value(),
aliasing_mementos_to_value(), and check_aliasing_discharged() as points of
change.
| pub formal_regions: Vec<Option<String>>, | ||
| pub return_sort: Sort, | ||
| pub return_region: Option<String>, |
There was a problem hiding this comment.
Commit the new lifetime metadata into the canonical contract value.
FunctionContractMemento now stores formal_regions and return_region, but build_value()/build_memento_value() never serialize them. After LLBC region enrichment, recomputing the CID will still hash the same bytes as a contract with no lifetime metadata, so the new C.9 data is not actually part of contract identity.
Proposed fix
fn build_value(
fn_name: &str,
formals: &[String],
formal_sorts: &[Sort],
+ formal_regions: &[Option<String>],
return_sort: &Sort,
+ return_region: Option<&str>,
pre: &IrFormula,
post: &IrFormula,
body_cid: Option<&str>,
effects: &EffectSet,
locus: &Locus,
auto_minted_mementos: &[AliasingMemento],
) -> Arc<Value> {
let formals_arr: Vec<Arc<Value>> = formals.iter().map(|n| Value::string(n.clone())).collect();
let formal_sorts_arr: Vec<Arc<Value>> =
formal_sorts.iter().map(|s| sort_to_value(s)).collect();
+ let formal_regions_arr: Vec<Arc<Value>> = formal_regions
+ .iter()
+ .map(|r| match r {
+ Some(name) => Value::string(name.clone()),
+ None => Value::null(),
+ })
+ .collect();
let body_cid_val: Arc<Value> = match body_cid {
Some(c) => Value::string(c.to_string()),
None => Value::null(),
};
+ let return_region_val: Arc<Value> = match return_region {
+ Some(r) => Value::string(r.to_string()),
+ None => Value::null(),
+ };
Value::object([
("schemaVersion", Value::string("1")),
("kind", Value::string("function-contract")),
("fnName", Value::string(fn_name.to_string())),
("formals", Value::array(formals_arr)),
("formalSorts", Value::array(formal_sorts_arr)),
+ ("formalRegions", Value::array(formal_regions_arr)),
("returnSort", sort_to_value(return_sort)),
+ ("returnRegion", return_region_val),
("pre", formula_to_canonical(pre)),
("post", formula_to_canonical(post)),
("bodyCid", body_cid_val),
("effects", effects.to_value()),
("locus", locus.to_value()),
("autoMintedMementos", aliasing_mementos_to_value(auto_minted_mementos)),
])
}Also applies to: 486-518, 525-537
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/contract.rs` around lines 353 - 355,
FunctionContractMemento now contains new lifetime metadata fields formal_regions
and return_region but build_value() and build_memento_value() do not serialize
them, so the canonical contract bytes (and resulting CID) omit lifetime data;
update build_value() and build_memento_value() to include serializing
FunctionContractMemento.formal_regions and .return_region into the canonical
contract/memento representation (follow the existing ordering/encoding used for
other fields) so that the LLBC-enriched regions become part of the contract
identity.
| /// Check that every `Effect::PossibleAliasing` pair of formals has a | ||
| /// matching AliasingMemento in `auto_minted_mementos`. Returns | ||
| /// `Ok(())` if aliasing is fully discharged or no PossibleAliasing | ||
| /// effects are present. Returns the first undischarged pair as an error. | ||
| pub fn check_aliasing_discharged(&self) -> Result<(), OpacityError> { | ||
| for effect in &self.effects.effects { | ||
| if let Effect::PossibleAliasing { formals } = effect { | ||
| if formals.len() < 2 { | ||
| continue; | ||
| } | ||
| for i in 0..formals.len() { | ||
| for j in (i + 1)..formals.len() { | ||
| let a = &formals[i]; | ||
| let b = &formals[j]; | ||
| let covered = self.auto_minted_mementos.iter().any(|m| { | ||
| (m.formal_a == *a && m.formal_b == *b) | ||
| || (m.formal_a == *b && m.formal_b == *a) | ||
| }); | ||
| if !covered { | ||
| return Err(OpacityError::AliasingNotDischarged { | ||
| formal_a: a.clone(), | ||
| formal_b: b.clone(), | ||
| }); | ||
| } | ||
| } | ||
| } | ||
| } | ||
| } | ||
| Ok(()) | ||
| } |
There was a problem hiding this comment.
Route aliasing discharge through the verifier lookup, not only the embedded bundle.
This path only checks self.auto_minted_mementos, and OpacityMementoLookup has no aliasing hook. For the new shared-&T PossibleAliasing cases, that means a verifier-supplied aliasing proof can never unblock composition here unless the contract itself is mutated to carry it. The discharge API should go through the same pool abstraction the rest of opacity uses.
Also applies to: 608-613, 843-859
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/contract.rs` around lines 394 - 423,
The check_aliasing_discharged implementation currently only inspects
self.auto_minted_mementos and therefore never considers verifier-supplied
aliasing proofs; change it to query the canonical memento pool/lookup
abstraction (OpacityMementoLookup) used elsewhere in opacity rather than
directly iterating auto_minted_mementos: replace the coverage check in
check_aliasing_discharged with a call into the lookup (or pool) API (e.g., a
method like lookup.has_aliasing_memento(formal_a, formal_b) or equivalent) so
verifier-provided mementos are considered, and apply the same refactor to the
analogous checks mentioned in the other spots (the other aliasing-discharge
loops at the two similar sites) so all aliasing discharge paths go through the
shared lookup abstraction.
| let mut region_map: HashMap<u32, String> = HashMap::new(); | ||
| if let Some(generics) = f.raw().get("generics") { | ||
| if let Some(regions) = generics.get("regions").and_then(|v| v.as_array()) { | ||
| for r in regions { | ||
| if let (Some(idx), Some(name)) = ( | ||
| r.get("index").and_then(|v| v.as_u64()).map(|v| v as u32), | ||
| r.get("name").and_then(|v| v.as_str()), | ||
| ) { | ||
| // TODO(#384 C.9): HRTB / late-bound regions have null names. | ||
| // When name is "'a" we use it verbatim; when null, the | ||
| // resolve_region_json fallback produces "'r<N>". | ||
| let name_str = if name == "''" || name.is_empty() { | ||
| format!("'r{}", idx) | ||
| } else { | ||
| name.to_string() | ||
| }; | ||
| region_map.insert(idx, name_str.clone()); | ||
| // Charon may use Body(N) where N is idx or idx+1. | ||
| // Map both to catch either encoding. | ||
| region_map.entry(idx.saturating_add(1)).or_insert_with(|| name_str); | ||
| } else if let Some(idx) = r.get("index").and_then(|v| v.as_u64()).map(|v| v as u32) { | ||
| // Null name: use fallback. | ||
| let name_str = format!("'r{}", idx); | ||
| region_map.insert(idx, name_str.clone()); | ||
| region_map.entry(idx.saturating_add(1)).or_insert_with(|| name_str); |
There was a problem hiding this comment.
Avoid storing 0-based and 1-based region ids in the same map.
This map aliases distinct lifetimes as soon as there is more than one region. With 'a at index 0 and 'b at index 1, Line 340 first makes key 1 -> 'a, then Line 337 for the second region overwrites key 1 -> 'b. Any Body(1) that uses the 1-based encoding now resolves to the wrong lifetime.
Use one canonical key space here and make the fallback explicit during lookup instead of inserting both conventions into the same HashMap.
| let pre_with_regions = if region_facts.is_empty() { | ||
| pre_formula.clone() | ||
| } else if matches!(&pre_formula, IrFormula::Atomic { name, args } if name == "true" && args.is_empty()) { | ||
| simplify_conjunction(region_facts) | ||
| } else { | ||
| let mut operands = vec![pre_formula.clone()]; | ||
| operands.extend(region_facts); | ||
| IrFormula::And { operands } | ||
| }; |
There was a problem hiding this comment.
Propagate the new Outlives facts into the post contract too.
post_formula is finalized before region_facts exist, so these signature-level lifetime constraints only land in pre_with_regions. That breaks the existing invariant in this function that pre contributions still hold at return, and it drops Outlives facts from the return-side contract.
Proposed fix
- let post_formula = simplify_conjunction(post_contribs);
+ // Defer post_formula until region_facts are available.
...
let pre_with_regions = if region_facts.is_empty() {
pre_formula.clone()
} else if matches!(&pre_formula, IrFormula::Atomic { name, args } if name == "true" && args.is_empty()) {
simplify_conjunction(region_facts)
} else {
let mut operands = vec![pre_formula.clone()];
- operands.extend(region_facts);
+ operands.extend(region_facts.clone());
IrFormula::And { operands }
};
+
+ post_contribs.extend(region_facts);
+ let post_formula = simplify_conjunction(post_contribs);🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/llbc_lift.rs` around lines 398 - 406,
pre_with_regions currently merges region_facts into the pre contract but
post_formula is finalized earlier so Outlives facts are not propagated to the
return-side; mirror the same merging logic for the post contract: build a
post_with_regions by checking if region_facts.is_empty() then clone
post_formula, else if post_formula matches IrFormula::Atomic { name == "true",
args.is_empty() } then use simplify_conjunction(region_facts), else create
operands = vec![post_formula.clone()] ; operands.extend(region_facts) and set
IrFormula::And { operands }; then use post_with_regions where post_formula was
previously used so Outlives facts are preserved at return.
| // Effect-based classification: PossibleAliasing is an LLBC-only effect | ||
| // (AST cannot see borrow shape). When formulas agree but LLBC carries | ||
| // PossibleAliasing that AST doesn't, classify as LlbcExtra(BorrowState). | ||
| if agreement == LayerAgreement::Identical { | ||
| let llbc_has_aliasing = llbc.effects.effects.iter().any(|e| matches!(e, Effect::PossibleAliasing { .. })); | ||
| let ast_has_aliasing = ast.effects.effects.iter().any(|e| matches!(e, Effect::PossibleAliasing { .. })); | ||
| if llbc_has_aliasing && !ast_has_aliasing { | ||
| return LayerAgreement::LlbcExtra(LlbcExtraCategory::BorrowState); | ||
| } |
There was a problem hiding this comment.
Borrow-state differences are classified here, but still lost from the merged contract.
This new branch correctly notices LLBC-only PossibleAliasing, but marry() still starts from ast.clone(). The substrate-facing merged contract therefore drops the LLBC-only borrow metadata/evidence (PossibleAliasing, auto_minted_mementos, and the new region fields), so the new C.8/C.9 information never reaches the record that downstream composition actually consumes.
Suggested direction
let mut merged = ast.clone();
+merged.effects = merge_effect_sets(&ast.effects, &llbc.effects);
+merged.auto_minted_mementos = llbc.auto_minted_mementos.clone();
+merged.formal_regions = llbc.formal_regions.clone();
+merged.return_region = llbc.return_region.clone();You’ll likely also want a deterministic merge for EffectSet plus coverage around married contracts that carry PossibleAliasing.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/src/marriage.rs` around lines 215 - 223,
The Identical-agreement branch detects LLBC-only PossibleAliasing but marry()
still begins from ast.clone(), dropping LLBC borrow metadata; change marry() so
when you return LayerAgreement::LlbcExtra(LlbcExtraCategory::BorrowState) you
build the merged contract by starting from a merge of ast and llbc (not
ast.clone()), deterministically combining EffectSet (merge llbc.effects into the
merged.effects with a stable ordering), and also copying LLBC-only fields
(auto_minted_mementos, the new region fields, and any PossibleAliasing effects)
into the merged contract; update or add tests around
marry()/LayerAgreement::LlbcExtra and Effect::PossibleAliasing to cover married
contracts that must preserve LLBC borrow evidence.
| "regions_outlive": [ | ||
| [ | ||
| { | ||
| "Body": 0 | ||
| }, | ||
| { | ||
| "Body": 1 | ||
| } | ||
| ] | ||
| ], |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Locate the regions_outlive consumption in the lifter and region-related code.
rg -n --type=rust "regions_outlive" -A 5 -B 2Repository: TSavo/provekit
Length of output: 2487
🏁 Script executed:
#!/bin/bash
rg -n --type=rust "region_longer|Outlives|outlives" -A 5 -B 2Repository: TSavo/provekit
Length of output: 22374
🏁 Script executed:
fd -type f "region_longer" --extension rsRepository: TSavo/provekit
Length of output: 229
🏁 Script executed:
fd "region_longer" -name "*.rs"Repository: TSavo/provekit
Length of output: 289
🏁 Script executed:
fd "region_longer" --type fRepository: TSavo/provekit
Length of output: 194
🏁 Script executed:
cat implementations/rust/provekit-walk/tests/fixtures/region_longer.rsRepository: TSavo/provekit
Length of output: 126
regions_outlive pair encodes the wrong outlives direction.
The Rust source is longer<'a, 'b: 'a>, meaning 'b (index 1) outlives 'a (index 0). In llbc_lift.rs (lines 367–368), the semantics are explicit: each pair encodes "region_a outlives region_b", and the lifter emits Outlives(region_a, region_b) where the first argument is the longer-lived region. The correct encoding for 'b: 'a is [Body(1), Body(0)], but the fixture has [Body(0), Body(1)], which emits Outlives('a, 'b) instead. The test region_longer_emits_outlives_b_a (line 3037) has a name that explicitly promises the correct direction but only validates that both regions are present, not their order—allowing this bug to pass undetected.
🐛 Proposed fix
- "regions_outlive": [
- [
- {
- "Body": 0
- },
- {
- "Body": 1
- }
- ]
- ],
+ "regions_outlive": [
+ [
+ {
+ "Body": 1
+ },
+ {
+ "Body": 0
+ }
+ ]
+ ],🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/tests/fixtures/region_longer.llbc` around
lines 57 - 66, The fixture encodes the outlives pair in the wrong direction: in
the Rust source longer<'a, 'b: 'a> region index 1 ('b) outlives index 0 ('a), so
the "regions_outlive" pair should be [ { "Body": 1 }, { "Body": 0 } ] not [ {
"Body": 0 }, { "Body": 1 } ]; update the regions_outlive entry in the fixture so
the first element is Body(1) and the second is Body(0) so that the lifter
(llbc_lift.rs) will emit Outlives(region_a, region_b) with the longer-lived
region as the first argument and make the test region_longer_emits_outlives_b_a
reflect the intended direction.
| "id": 4, | ||
| "kind": { | ||
| "Assign": [ | ||
| { | ||
| "kind": { | ||
| "Local": 0 | ||
| }, | ||
| "ty": { | ||
| "Untagged": { | ||
| "Ref": [ | ||
| { | ||
| "Static": true | ||
| }, | ||
| { | ||
| "Untagged": { | ||
| "Literal": { | ||
| "UInt": "U32" | ||
| } | ||
| } | ||
| }, | ||
| "Shared" | ||
| ] | ||
| } | ||
| } | ||
| }, | ||
| { | ||
| "Use": { | ||
| "Copy": { | ||
| "kind": { | ||
| "Local": 1 | ||
| }, | ||
| "ty": { | ||
| "Untagged": { | ||
| "Literal": { | ||
| "UInt": "U32" | ||
| } | ||
| } | ||
| } | ||
| } | ||
| } | ||
| } | ||
| ] | ||
| }, | ||
| "comments_before": [] |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Check if any test references region_static and what fields it inspects.
rg -n "region_static" -A 10 -B 2
# Check if the body traversal in llbc_lift.rs processes local assignments and validates type consistency.
rg -n --type=rust "body\|locals\|StorageLive\|Assign" implementations/rust/provekit-walk/src/llbc_lift.rs | head -40Repository: TSavo/provekit
Length of output: 4784
🏁 Script executed:
#!/bin/bash
# Look at the lift_llbc_function implementation to see if it processes the body
rg -n "fn lift_llbc_function" implementations/rust/provekit-walk/src/llbc_lift.rs -A 30
# Check if there's any type validation or consistency checking
rg -n "type.*valid\|check.*type\|type.*check" implementations/rust/provekit-walk/src/llbc_lift.rs -iRepository: TSavo/provekit
Length of output: 2953
🏁 Script executed:
#!/bin/bash
# Get the full implementation of lift_llbc_function_with_registry
rg -n "fn lift_llbc_function_with_registry" implementations/rust/provekit-walk/src/llbc_lift.rs -A 200 | head -250Repository: TSavo/provekit
Length of output: 9301
🏁 Script executed:
#!/bin/bash
# Check if there's any type validation logic in body processing
rg -n "type.*mismatch\|mismatch.*type\|type.*error\|invalid.*type" implementations/rust/provekit-walk/src/llbc_lift.rs -i
# Check the detect_effects_llbc function to understand what it does
rg -n "fn detect_effects_llbc" implementations/rust/provekit-walk/src/llbc_lift.rs -A 20
# Check for Assign statement handling in the body processing
rg -n "Assign\|statement" implementations/rust/provekit-walk/src/llbc_lift.rs | head -30Repository: TSavo/provekit
Length of output: 3833
Body statement id=4 has a structural type mismatch in the fixture.
Statement id=4 copies local 1 (type u32) into local 0 (type &'static u32). This violates LLBC type consistency: a value of type u32 cannot be assigned to a reference-typed slot without a Ref operation. For the source fn give_static() -> &'static u32 { &7 }, a structurally valid body would use a promoted constant reference, not a plain Copy of an integer value.
The test region_static_emits_static_region() only validates signature-level region extraction (formals, formal_regions, return_region) and never traverses the function body. The lifter's body-processing functions extract patterns and effects but do not perform type consistency validation, so this mismatch is benign in practice. However, the fixture should be corrected to emit valid LLBC.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@implementations/rust/provekit-walk/tests/fixtures/region_static.llbc` around
lines 228 - 271, Statement id=4 in the fixture for function give_static
incorrectly assigns a plain Copy of local 1 (type u32) into local 0 (type
&'static u32); change the second Assign element for statement id=4 so that it
produces a reference-to-promoted-constant (i.e., a Ref/Promoted or otherwise a
Literal reference with Static=true) rather than a Copy of an integer: update the
part that currently emits "Use: Copy: Local 1" to emit a reference/Literal that
matches local 0's type (&'static u32), ensuring the Assign for local 0 is
structurally a Ref to a static/promoted u32 consistent with the function
give_static signature.
…checks Both PR #419 (aliasing + PossibleAliasing) and main (pin-invariant + PinnedReference, drop effects) added to the Effect enum and composition logic. Semantic resolution: keep both Effect::PossibleAliasing and Effect::PinnedReference in the non_opacity_pure pattern matches, as both are opacity effects that must be discharged before composition. Conflict 1 (discharge check): HEAD added PossibleAliasing discharge, main added PinnedReference discharge — kept both branches. Conflicts 2-4 (pattern matches): HEAD's PossibleAliasing + main's PinnedReference merged into single unified list for outer_non_opacity_pure and inner_non_opacity_pure.
|
Merge conflict resolved: contract.rs had conflicting discharge checks for PossibleAliasing (HEAD) and PinnedReference (main). Kept both: OpacityMementoLookup trait has has_aliasing_memento and check_opacity_effects handles both Effect::PossibleAliasing (auto-discharged) and Effect::PinnedReference (pool lookup). Non-opacity-pure pattern matches updated to include all four opacity effects. Build and tests pass. |
|
Superseded by per-issue PRs that landed via the work-order template: #439 (AliasingMemento discharge / #416), #441 (region-quantifier composition / #412), #444 (marriage hookup / #413), #446 (C.9 integration test scaffolding / #414), and the C.8 lifter side via the same family. Content is now fully duplicated on main; closing without merge to avoid conflict noise. |
|
Superseded by PR #458 (clean rebase on current main). Closing in favor of the replacement PR. |
… pool - invokeSolver() now uses the worker pool instead of spawn-per-call - Each (check-sat) query uses (push)/(pop) for scope isolation - Eliminates startup overhead and process contention on shared CI runners - Tests now pass consistently without timeout flakes Relates: TSavo#429 TSavo#419 TSavo#439
Closes #409 (C.8 aliasing) and #410 (C.9 Outlives). Closes C.8 and C.9 from parent issue #384.
C.8 — Aliasing (2a14c6c)
Effect::PossibleAliasingfor&Tformal pairs with interior mutability. Auto-mintsDisjointAliasingMementos for&mut Tpairs.src/aliasing.rshas_unsafecell_transitiveclassifier with cycle detectionsrc/contract.rsPossibleAliasing,AliasingMemento,AliasingStatus,auto_minted_mementossrc/llbc_lift.rslift_llbc_function_with_registrysrc/marriage.rsPossibleAliasing→LlbcExtra(BorrowState)C.9 — Outlives (a8176c4)
Sort::Regionterms +Outlives(r1, r2)predicates from Charon LLBC region tables.src/contract.rsformal_regions,return_region,region_factsfieldssrc/sort_translate.rsextract_region_namefor Ref typessrc/llbc_lift.rstests/fixtures/region_*.llbcsrc/marriage.rsLlbcExtra(LifetimeRelative)Tests
cargo check --workspacecleanSummary by CodeRabbit
Release Notes
New Features
Tests