checkpoint#25
Open
nikomatsakis wants to merge 47 commits into
Open
Conversation
Fix output renaming bug and implement normalize_ty_for_pop. These land together — renaming without normalization breaks the accidental Var::This workaround; normalization without renaming has nothing to normalize. Output renaming fix (expressions.rs): - Apply with_this_stored_to(this_var) to output alongside input types - Thread output through type_method_arguments_as so each with_var_stored_to(input_name, input_temp) is applied to it Normalization module (pop_normalize.rs — new file): - normalize_ty_for_pop: walks type structure, normalizes perms referencing popped vars via red_perm expansion + dead-link stripping - strip_popped_dead_links: Mtd(popped)::tail → drop Mtd (shareable + mut tail); Rfd(popped)::tail → Shared (shareable + mut tail); errors on dangling borrows (ref from given, unshareable guards) Call rule wiring: - Normalize output before pop_fresh_variables - check_type on normalized output catches ill-formed Or Also adds Perm::flat_or() flattening constructor in perm_impls.rs. All 609 tests pass.
Add 10 interpreter tests in src/interpreter/tests/normalization.rs covering the same patterns as the type system normalization tests: - given_from[self] resolution (basic + different caller perm) - given_from[x] with named parameter (basic + give result) - Borrow chaining through ref (param + self) - Multi-place ref/mut/given_from producing Or - No leaked method bindings after sequential calls 9 tests pass with current (pre-normalization) snapshots. 1 test is #[ignore]'d because it triggers the Var::This collision bug in the interpreter (will be un-ignored in Phase 3b).
…ion assertion) Split the original Phase 3b into two steps: - Phase 3b: Remove the type binding injection workaround and add a check_type preservation assertion on result types. This exposes the bug cleanly — tests fail because result types reference method-scoped variables no longer in the caller's env. - Phase 3c: Add normalize_ty_for_pop to the interpreter, resolving all method-scoped references. Tests pass again with the preservation assertion as a permanent safety net.
… assertion Remove the method_type_bindings hack that leaked method-scoped variable names into the caller's env. Add a check_type preservation assertion in call_method that verifies result types only reference variables in the caller's scope. This exposes 19 existing interpreter test failures — all preservation violations where result types contain method-scoped references like given_from[_N_self] or mut[_N_x]. These will be fixed by Phase 3c when normalize_ty_for_pop is wired into the interpreter. Changes: - Delete method_type_bindings collection and injection loop - Add check_type assertion after call_method returns - Make types module public for the import - Update normalization tests: 6 pass, 5 ignored (preservation violations) - Replace ref-self test with two clearer tests
…dd Phase 4 Phase 3c (interpreter) adds normalize_ty_for_pop at two points: 1. eval_block exit: normalize against block-scoped variables 2. call_method return: normalize against method parameters Phase 4 (type system) adds the matching change: pop let-bound variables at block exit and normalize. Currently the type system never pops let-bound variables, so this is a new capability.
Add normalization at two points in the interpreter: 1. Method return (call_method): Normalize result type against method parameters before the preservation assertion. Resolves method-scoped variables (e.g., given_from[_N_self] → ref[caller_var]) to caller-scoped permissions. 2. Block exit (eval_block): Normalize final values and early-return values against block-scoped variables. Detects genuine dangling borrows (ref from owned block-local that will be deinitialized). Key addition: copy-type permission stripping. When normalizing ApplyPerm(perm, ty) where ty is copy (e.g., Int, shared classes), the permission is stripped entirely — a copy type doesn't need a permission chain since the value is independent of its source. Restructured 7 tests that returned non-copy borrowed values from Main.main (genuine dangling borrows) to use print() and return () instead. Tests still exercise the same place-operation mechanics. Made liveness module public for interpreter access. All 620 tests pass, 0 ignored.
9 tests in src/type_system/tests/block_normalization.rs: - 6 pass currently (call-site normalization or no local refs) - 3 fail until Phase 4b: dangling borrow detection (ref/mut from owned block-local) and block-local variable scoping (locals should not leak into outer env after block exit)
Pop block-scoped variables at block exit and normalize the result type against them. This catches dangling borrows (ref/mut from owned block-locals) and prevents block-local variables from leaking into the outer env. Changes: - blocks.rs: type_block now snapshots vars before/after statements, normalizes result via normalize_ty_for_pop, and pops block-scoped vars - env.rs: Added local_variable_names() and pop_block_variables() helpers - 7 existing test snapshots updated (errors now fire earlier from block-exit normalization instead of deeper in the type system) - All 629 tests pass
…ared helper - Extract dead_link_is_strippable judgment in redperms.rs: encapsulates the shared 'shareable type + mut-based tail' check used by both subtyping (red_chain_sub_chain) and normalization (strip_popped_dead_links) - Rewrite strip_popped_dead_links as a judgment_fn in pop_normalize.rs: recursive Head/Tail pattern matching replaces imperative while loop - Update red_chain_sub_chain to use dead_link_is_strippable (removes duplicated prove_is_shareable + prove_is_mut logic) - Add RedChain::cons(link, tail) helper for constructing chains in judgments - Make Head/Tail tuple struct fields pub for cross-module pattern matching - Separate dangling_borrow_error() function produces clean error messages by analyzing the chain structure (preserves existing error message format) - All 629 tests pass with identical error messages
Convert all normalization functions to judgment_fn! style: - normalize_ty_for_pop: pattern-matches on Ty variants (NamedTy, Var, ApplyPerm) - normalize_params_for_pop: recursive Cons/nil list processing - normalize_param_for_pop: dispatches on Parameter::Ty/Perm - normalize_perm_for_pop: early-return if no popped refs, else red_perm + strip - strip_all_chains: recursive universal strip (all chains must succeed) Key changes: - Replaced collect+existential with recursive strip_all_chains (universal semantics: ALL chains must strip successfully, not just some) - Callers in blocks.rs/expressions.rs use judgment call syntax - Callers in interpreter use .into_singleton() for ProvenSet extraction - Removed dangling_borrow_error() - standard judgment errors suffice - Reverted collect pub(crate) - no longer needed from pop_normalize - 14 test snapshots updated with judgment-style error messages - All 629 tests pass
- Use NamedTy::new(name, norm_params) instead of manual struct construction - Extract prepend() helper for recursive list building in judgment rules - Simplify red_perm_to_perm to take &Vec<RedChain> directly - Remove unnecessary RedPerm::clone/Set::clone intermediate conversions - Use .iter().cloned() on judgment result references instead of T::clone - Remove unused RedPerm import
Let impl Upcast handle the &Ty -> Ty coercion. For non-Arc fields like perm: &Perm, just pass perm directly.
Use &**x for &Arc<T> -> &T deref, letting impl Upcast handle cloning, instead of T::clone(x).
New sections: - Cons/() for collection building in judgment return positions - Struct patterns directly in conclusions (not separate let destructure) - Upcast in return values (auto-wrapping enum variants) - Complementary cuts (both sides of if/else guards) - Upcasted iterator adapter - into_singleton()? works directly without map_err - Expanded upcast coercion chain table (Ty→Parameter, Perm→Parameter)
…se fix) Switch from local path to git dependency on nikomatsakis/a-mir-formality-ndm, branch dada-model-pin. This merges two branches: - parser-better-ambig (PR #283): fixes left-recursive parsing to find all seeds, adds #[reject] attribute for cross-type disambiguation - fix/collection-parse: generalizes each_comma/delimited_nonterminal over collection type (needed for Set<T> fields in grammar) Grammar changes to handle the fixed left-recursion: - Add #[precedence(1, left)] on Perm::Apply for left-associative composition - Add #[reject(Perm::Apply(..), _)] on Ty::ApplyPerm to resolve Perm/Ty boundary ambiguity (prefer 'given (given Data)' over '(given given) Data') - Add CoreParseBinding impl for Parameter (new trait requirement) - Port method_impls.rs and named_ty_impls.rs to new CPS parser API Snapshot updates from upstream typo fix (evaluted -> evaluated) and left-associative perm parsing.
Replace the assert_interpret! macro with a unified version supporting:
- type: ok / type: error(expect) for type-checker outcome
- interpret: ok(expect) / interpret: fault(expect) for interpreter outcome
- optional prefix: expr for injecting shared definitions
Add helper functions: parse_program, check_program_result, assert_type_ok,
assert_type_err, assert_interpret_result. Make run_interpreter pub.
Convert all 64 existing assert_interpret!({ ... }, expect![...]) calls to
assert_interpret!({ ... }, type: ok, interpret: ok(expect![...])).
Old macros (assert_interpret_only!, assert_interpret_fault!, etc.) are
unchanged and will be migrated in later phases.
Update WIP doc with corrected counts (was 178, actually 64 assert_interpret!
plus 114 assert_interpret_only!) and add Phase 2a for _only! migration.
Type checker rejects the share_skips_borrowed_subfield test (prove_mut_predicate fails for given permission). Converted to type: error with snapshot.
loop_body_value_is_freed: type checker rejects (no loop/break rules). Converted to type: error with snapshot.
4 pass type checker (type: ok), 2 fail (loop/break not supported): - block_early_break_drops_locals: type: error - loop_break_drops_locals: type: error
8 pass type checker (type: ok), 1 fails: - is_last_ref_per_allocation: type: error (prove_copy_predicate for given)
7 pass type checker (type: ok), 4 fail (type: error): - interp_give_shared - interp_ref_shared - interp_share_recursive - interp_array_class_shared_no_move
23 pass type checker (type: ok), 10 fail (type: error): - give_from_shared, give_from_shared_nested, give_shared_multiple_times - give_shared_nested_subfield, give_field_through_shared_path - ref_from_shared, ref_from_shared_nested, ref_from_shared_nested_subfield - share_nested_objects, share_already_shared_is_noop
44 pass type checker (type: ok), 11 fail (type: error): - shared array ops and nested array scenarios where type checker doesn't fully handle shared/given permission interactions
struct_move_param_give_twice_faults: type checker rejects (type: error), interpreter faults as expected.
All 9 are rejected by the type checker (type: error, interpret: fault): - give_from_given_uninitializes_source, drop_given_nested_uninitializes - mut_field_through_shared, mut_field_through_ref, mut_field_uninitialized - mut_of_copy_type_faults, mut_of_shared_faults, mut_of_uninitialized_faults - mut_dangling_after_give
2 rejected by type checker (type: error, interpret: fault): - array_give_uninitializes_source - given_array_double_give_faults 6 future-panic tests (type: ok, interpret: fault) — type checker correctly accepts; faults are runtime bounds/initialization checks: - array_give_uninitialized_faults, array_give_out_of_bounds - array_write_out_of_bounds, array_drop_out_of_bounds - array_drop_uninitialized_faults, array_zero_length_access_faults 3 soundness gaps (type: ok, interpret: fault) — BUG: type checker accepts but interpreter faults on use-after-array_drop: - array_drop_element, array_drop_shared_class_element, array_drop_p_given_range
All 10 fail type-checking (type: error) — the type checker doesn't yet fully support the permission patterns Vec uses. All interpret ok. Converted to assert_interpret! with prefix: vec_prelude().
- Remove assert_interpret_only!, assert_interpret_after_err!, assert_interpret_fault! macros - Remove old helper functions: test_interpret, test_interpret_only, test_interpret_after_err - Remove vec_test! macro from vector.rs - Remove stale comments referencing old macros in array.rs, basics.rs, drop_body.rs - Update AGENTS.md with new assert_interpret! macro documentation - Mark all WIP phases complete, document soundness gaps found
Tests returning shared values (via .share, .give from shared, .ref from shared) incorrectly declared non-shared return types (e.g., -> Data instead of -> shared Data), causing spurious type-checker failures. Fixed in: - mdbook.rs: 4 tests (interp_give_shared, interp_ref_shared, interp_share_recursive, interp_array_class_shared_no_move) - place_ops.rs: 10 tests (give_from_shared, give_from_shared_nested, give_shared_multiple_times, give_shared_nested_subfield, ref_from_shared, ref_from_shared_nested, ref_from_shared_nested_subfield, share_nested_objects, share_already_shared_is_noop, give_field_through_shared_path) All 14 now pass type-checking (type: ok). Remaining type: error + interpret: ok tests (25): - 11 prove_copy_predicate (deeper type-checker issues with shared arrays) - 10 variance_predicate (Vec type-checker gap) - 3 type_statement (no loop/break support) - 1 prove_mut_predicate (share.rs)
Catalog of all 25 type: error, interpret: ok tests organized by root cause: - 11 prove_copy_predicate (given is copy) - 10 variance_predicate (Vec type params) - 3 type_statement (loop/break) - 1 prove_mut_predicate (given is mut) Also documents the 9 type: ok, interpret: fault tests (6 future-panic, 3 soundness gaps).
All 11 tests stored shared values into positions typed as bare T (= given T). Since shared is not a subtype of given, the type checker correctly rejected them. Fixes: - array.rs (10): changed element types to shared Array[T] in array_new/write/give/drop params; fixed access perms given->shared when reading from shared arrays; fixed return type mismatches - drop_body.rs (1): changed field type to shared Array[Int] Remaining type:error/interpret:ok tests: 14 (all known type system gaps: 10 Vec variance, 3 loop/break, 1 given-is-mut)
This test was testing paths no longer needed.
…ic in methods and drop bodies check_method only added variance assumptions (relative/atomic) for method-level parameters, not class-level ones. This caused all 10 Vec tests to fail type-checking because T is relative couldn't be proven inside method bodies. - Add Env::with_variance_assumed() helper to centralize the pattern - Pass class-level vars (substitution) into check_method and check_drop_body - Add 'where T is relative' to Iterator class (needed for field 'vec: P Vec[T]') - All 10 vector.rs tests now pass type-checking (type: error -> type: ok)
Spin out the 3 remaining loop/break type-error-analysis cases into a new control-flow.md design document. This broadens the scope to cover all non-straightline control flow issues: - if/else: branches treated sequentially, no env fork/join - loop: no back-edge in liveness, env leaks from body - break: no loop context, dead code liveness propagates No code changes — design still in progress.
Add an `elaborator` module with an `ElaboratedProgram` wrapper around `Arc<Program>`. The only constructor, `ElaboratedProgram::elaborate`, runs a (currently no-op) elaboration pass before wrapping, so storing an `ElaboratedProgram` proves elaboration has taken place. `ElaboratedProgram` is a plain struct with hand-derived traits and `cast_impl!` rather than a `#[term]`, to avoid the auto-generated `::new(Arc<Program>)` constructor that would bypass elaboration. It implements `Deref<Target = Program>` so callers see it as a `Program` transparently. Thread through: - `Env` now stores `ElaboratedProgram`; `Env::program()` still returns `&Program` via deref. - `check_program`, `check_decl`, `check_class` judgments take `ElaboratedProgram`. - `Interpreter` stores an owned `ElaboratedProgram`, dropping its `'a` lifetime. One `drop_value` site clones the `ClassDecl` to satisfy the borrow checker now that `self.program` is owned. - `src/lib.rs` and all test macros in `src/test_util.rs` route through `ElaboratedProgram::elaborate`, so every test exercises elaboration. Elaboration itself is a no-op for now; see md/wip/introduce-elaborator.md.
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
1 participant
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.
No description provided.