feat(walk): C.8 aliasing + C.9 Outlives — #384 Tier C gap closure (retry) by TSavo · Pull Request #458 · TSavo/provekit

TSavo · 2026-05-06T12:54:32Z

Replaces #419 with a clean branch based on current main.

Closes #409 (C.8 aliasing) and #410 (C.9 Outlives). Closes C.8 and C.9 from parent issue #384.

C.8 — Aliasing

Effect::PossibleAliasing for &T formal pairs with interior mutability. Auto-mints Disjoint AliasingMementos for &mut T pairs.

C.9 — Outlives

Sort::Region terms + Outlives(r1, r2) predicates from Charon LLBC region tables.

Tests

202 total (12 walk + 6 C.8 + 7 C.9 + pre-existing)
cargo check --workspace clean

Summary by CodeRabbit

Tests
- Updated walk demo fixture with revised function behavior.
Features
- Extended system to model drops of types with error reporting for unhandled drops.

…int AliasingMemento for &mut formals (closes #409)

…tagged wrap, CID commitment, kebab-case, discharge gating

@region

…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.

…sing branch

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.

…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.

coderabbitai · 2026-05-06T12:54:49Z

Caution

Review failed

The pull request is closed.

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: ce770f13-d630-4523-b354-09d31f0a2ec1

📥 Commits

Reviewing files that changed from the base of the PR and between 3631149 and 50e1262.

📒 Files selected for processing (2)

implementations/rust/provekit-walk/src/bin/walk_demo.rs
implementations/rust/provekit-walk/src/contract.rs

Walkthrough

This PR introduces a Drop effect variant to the contract system to model type drops, with handling across serialization, sorting, opacity checks, and composition logic. It also updates a test fixture in the walk demo.

Changes

Demo Fixture Update

Layer / File(s)	Summary
Test Fixture `implementations/rust/provekit-walk/src/bin/walk_demo.rs`	Embedded bare-demo source updated: function `f` now panics when `x < 10` and returns `x + 1` instead of `x * 2`.

Drop Effect Implementation

Layer / File(s)	Summary
Effect Enum Definition `implementations/rust/provekit-walk/src/contract.rs` (lines 143–149)	New `Drop { name: String }` variant added to the `Effect` enum to represent drops of named types.
Serialization & Sorting `implementations/rust/provekit-walk/src/contract.rs` (lines 280–287, 320–324)	`to_value()` extended to encode `Drop` as `kind: "drop"` with name field; `sort_key()` adds deterministic ordering for `Drop` and `PossibleAliasing` variants.
Error Handling `implementations/rust/provekit-walk/src/contract.rs` (lines 677–680)	New `DropNotDischarged { name: String }` variant added to `OpacityError` to report undischarged drop contracts.
Opacity Discharge Logic `implementations/rust/provekit-walk/src/contract.rs` (lines 745–749)	`check_opacity_effects()` extended: if a `Drop` effect lacks a lifted drop contract in the pool, return `DropNotDischarged`.
Composition Filtering `implementations/rust/provekit-walk/src/contract.rs` (lines 913–925)	`compose_function_contracts_checked()` expanded to treat `Drop` and `PinnedReference` as non-opacity blockers; composition returns `Ok(None)` when undischargeable non-opacity blockers remain post-discharge.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~20 minutes

Possibly related PRs

TSavo/provekit#426: Implements the Drop effect variant and associated opacity discharge semantics specified in the Drop RFC, making it directly related to this PR's introduction of Drop handling.

Poem

A hopper's joy when drops align,
No leaks in logic, clean design—
From serialized to sorted clean,
The Drop effect now guards the scene. 🐰✨

✨ 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 issue/419-retry

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

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

TSavo added 8 commits May 5, 2026 17:08

feat(walk): C.8 aliasing — Effect::PossibleAliasing + auto-mint Disjo…

5a14c6c

…int AliasingMemento for &mut formals (closes #409)

fix(walk): P1 aliasing corrections — ADT traversal, def_id shapes, Un…

8a50f14

…tagged wrap, CID commitment, kebab-case, discharge gating

Merge origin/main — resolve conflicts, add Drop effect wiring to alia…

cc6ff12

…sing branch

Merge main into feat/384-c8-aliasing

047f9a8

Merge origin/main into feat/384-c8-aliasing, resolve conflicts

50e1262

Copilot AI review requested due to automatic review settings May 6, 2026 12:54

TSavo mentioned this pull request May 6, 2026

feat(walk): C.8 aliasing + C.9 Outlives — #384 Tier C gap closure #419

Closed

TSavo merged commit 2760e36 into main May 6, 2026
5 of 9 checks passed

TSavo deleted the issue/419-retry branch May 6, 2026 12:55

Copilot started reviewing on behalf of TSavo May 6, 2026 12:55 View session

TSavo review requested due to automatic review settings May 6, 2026 13:18

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(walk): C.8 aliasing + C.9 Outlives — #384 Tier C gap closure (retry)#458

feat(walk): C.8 aliasing + C.9 Outlives — #384 Tier C gap closure (retry)#458
TSavo merged 8 commits into
mainfrom
issue/419-retry

TSavo commented May 6, 2026 •

edited by coderabbitai Bot

Loading

Uh oh!

coderabbitai Bot commented May 6, 2026 •

edited

Loading

Review failed

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

TSavo commented May 6, 2026 • edited by coderabbitai Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

C.8 — Aliasing

C.9 — Outlives

Tests

Summary by CodeRabbit

Uh oh!

coderabbitai Bot commented May 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review failed

Walkthrough

Changes

Estimated code review effort

Possibly related PRs

Poem

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

TSavo commented May 6, 2026 •

edited by coderabbitai Bot

Loading

coderabbitai Bot commented May 6, 2026 •

edited

Loading