navicore/patch-seq

Fork 0

Stack pollution detection - words leaving extra values #228

New issue

Closed

opened 2026-01-10 23:11:22 +00:00 by navicore · 4 comments

navicore commented

2026-01-10 23:11:22 +00:00

(Migrated from github.com)

Problem

The type checker catches type mismatches and underflow, but there's no explicit check that words don't leave garbage on the stack beyond their declared effect.

Example

: leaky ( Int -- Int ) 42 ;  // Pushes extra value - currently caught?
: sneaky ( Int -- Int ) dup ; // Returns 2 values instead of 1

Current Behavior

This may be caught implicitly via stack shape mismatch during unification, but:

No specific "stack pollution" error message
No explicit tests verifying this is caught
Edge cases in branches/loops may escape detection

Feasibility Questions

If the stack is 5 Ints and the word eats 2 instead of the declared 1, or writes 3 instead of the declared 2, is this caught?
Does the row polymorphism (..rest) accidentally allow extra values to "hide"?
Are there paths through conditionals where pollution could escape?

Proposed Work

Add explicit tests attempting stack pollution in various contexts
Verify unification catches all cases
Add specific error message if not already present
Document the guarantee (or lack thereof)

Acceptance Criteria

Test suite proving pollution is caught in: simple words, branches, loops, quotations
Clear error message for pollution cases
Documentation of the safety guarantee

## Problem The type checker catches type mismatches and underflow, but there's no explicit check that words don't leave garbage on the stack beyond their declared effect. ## Example ```seq : leaky ( Int -- Int ) 42 ; // Pushes extra value - currently caught? : sneaky ( Int -- Int ) dup ; // Returns 2 values instead of 1 ``` ## Current Behavior This may be caught implicitly via stack shape mismatch during unification, but: 1. No specific "stack pollution" error message 2. No explicit tests verifying this is caught 3. Edge cases in branches/loops may escape detection ## Feasibility Questions - If the stack is 5 Ints and the word eats 2 instead of the declared 1, or writes 3 instead of the declared 2, is this caught? - Does the row polymorphism (`..rest`) accidentally allow extra values to "hide"? - Are there paths through conditionals where pollution could escape? ## Proposed Work 1. Add explicit tests attempting stack pollution in various contexts 2. Verify unification catches all cases 3. Add specific error message if not already present 4. Document the guarantee (or lack thereof) ## Acceptance Criteria - [ ] Test suite proving pollution is caught in: simple words, branches, loops, quotations - [ ] Clear error message for pollution cases - [ ] Documentation of the safety guarantee

navicore commented

2026-01-10 23:17:02 +00:00

(Migrated from github.com)

Test Results: Stack Pollution Detection

Added 12 tests to typechecker.rs to probe stack pollution detection.

✅ Caught (7 tests passed)

Test	Scenario
`test_pollution_extra_push`	`( Int -- Int ) 42 ;` - pushes extra value
`test_pollution_extra_dup`	`( Int -- Int ) dup ;` - dup produces 2
`test_pollution_consumes_extra`	`( Int -- Int ) drop drop 42 ;` - consumes 2
`test_pollution_in_then_branch`	`if 1 2 else 3 then` - branches differ
`test_pollution_in_else_branch`	`if 1 else 2 3 then` - branches differ
`test_pollution_both_branches_extra`	`if 1 2 else 3 4 then` - both extra
`test_pollution_branch_consumes_extra`	Branch consumes more than available

❌ NOT Caught (2 tests failed - GAPS FOUND)

Test	Scenario	Expected
`test_pollution_quotation_wrong_arity_output`	`( Int -- Int ) [ dup ] call ;`	Should reject: quotation produces 2 values
`test_pollution_quotation_wrong_arity_input`	`( Int -- Int ) [ drop drop 42 ] call ;`	Should reject: quotation consumes 2 values

Analysis

The type checker correctly catches pollution for direct code, but quotation effects are not properly verified when call is applied.

When [ dup ] call runs:

Quotation [ dup ] is inferred as ( ..a T -- ..a T T )
call applies this effect to current stack
Final stack has 2 values, but declared output is 1
This mismatch should be caught but isn't

Root Cause Hypothesis

The quotation's effect is inferred independently, but the final stack after call isn't being unified against the word's declared output type. The unification may be treating the inferred row variable as flexible rather than rigid.

Valid Tests (all passed)

test_no_effect_annotation_pollution - inferred effects work
test_valid_effect_exact_match - exact matches work
test_valid_polymorphic_passthrough - polymorphic identity works

Next Steps

Investigate why quotation effects don't propagate correctly through call
May need to ensure final stack is unified against declared output with rigid row variables
Consider if quotation effect inference needs stricter validation

## Test Results: Stack Pollution Detection Added 12 tests to `typechecker.rs` to probe stack pollution detection. ### ✅ Caught (7 tests passed) | Test | Scenario | |------|----------| | `test_pollution_extra_push` | `( Int -- Int ) 42 ;` - pushes extra value | | `test_pollution_extra_dup` | `( Int -- Int ) dup ;` - dup produces 2 | | `test_pollution_consumes_extra` | `( Int -- Int ) drop drop 42 ;` - consumes 2 | | `test_pollution_in_then_branch` | `if 1 2 else 3 then` - branches differ | | `test_pollution_in_else_branch` | `if 1 else 2 3 then` - branches differ | | `test_pollution_both_branches_extra` | `if 1 2 else 3 4 then` - both extra | | `test_pollution_branch_consumes_extra` | Branch consumes more than available | ### ❌ NOT Caught (2 tests failed - GAPS FOUND) | Test | Scenario | Expected | |------|----------|----------| | `test_pollution_quotation_wrong_arity_output` | `( Int -- Int ) [ dup ] call ;` | Should reject: quotation produces 2 values | | `test_pollution_quotation_wrong_arity_input` | `( Int -- Int ) [ drop drop 42 ] call ;` | Should reject: quotation consumes 2 values | ### Analysis The type checker correctly catches pollution for direct code, but **quotation effects are not properly verified when `call` is applied**. When `[ dup ] call` runs: 1. Quotation `[ dup ]` is inferred as `( ..a T -- ..a T T )` 2. `call` applies this effect to current stack 3. Final stack has 2 values, but declared output is 1 4. **This mismatch should be caught but isn't** ### Root Cause Hypothesis The quotation's effect is inferred independently, but the final stack after `call` isn't being unified against the word's declared output type. The unification may be treating the inferred row variable as flexible rather than rigid. ### Valid Tests (all passed) - `test_no_effect_annotation_pollution` - inferred effects work - `test_valid_effect_exact_match` - exact matches work - `test_valid_polymorphic_passthrough` - polymorphic identity works ### Next Steps 1. Investigate why quotation effects don't propagate correctly through `call` 2. May need to ensure final stack is unified against declared output with rigid row variables 3. Consider if quotation effect inference needs stricter validation

navicore commented

2026-01-10 23:18:52 +00:00

(Migrated from github.com)

Root Cause Identified

The call builtin has signature:

( ..a Q -- ..b )

Where ..a and ..b are independent row variables. This means:

..a captures the stack below the quotation
Q captures the quotation type
..b is completely unconstrained - it doesn't use the quotation's actual effect!

The Problem

When we have:

: test ( Int -- Int ) [ dup ] call ;

Stack starts as ( ..rest Int ) (from declared input)
Push quotation: ( ..rest Int Quot[..x T -- ..x T T] )
Apply call signature ( ..a Q -- ..b ):
- ..a unifies with ( ..rest Int )
- Q unifies with Quot[...]
- ..b is fresh and NOT constrained by the quotation's effect
Result stack is ..b (unconstrained)
Word's declared output ( ..rest Int ) unifies with ..b - always succeeds!

The quotation's actual effect ( ..x T -- ..x T T ) is never applied.

The Fix

infer_word_call needs special handling for call:

if name == "call" {
    // Pop quotation from stack
    let (remaining_stack, quot_type) = current_stack.pop()?;
    
    // Extract quotation's effect
    let quot_effect = match quot_type {
        Type::Quotation(effect) => effect,
        Type::Closure { effect, .. } => effect,
        _ => return Err("call requires quotation"),
    };
    
    // Apply the quotation's effect to remaining stack
    return self.apply_effect(&quot_effect, remaining_stack, "call");
}

This would properly propagate the quotation's stack effect through call.

Scope

This affects:

call builtin
Possibly bi, dip, keep, and other combinators that invoke quotations
Each combinator may need special handling to properly propagate quotation effects

## Root Cause Identified The `call` builtin has signature: ``` ( ..a Q -- ..b ) ``` Where `..a` and `..b` are **independent** row variables. This means: - `..a` captures the stack below the quotation - `Q` captures the quotation type - `..b` is **completely unconstrained** - it doesn't use the quotation's actual effect! ### The Problem When we have: ```seq : test ( Int -- Int ) [ dup ] call ; ``` 1. Stack starts as `( ..rest Int )` (from declared input) 2. Push quotation: `( ..rest Int Quot[..x T -- ..x T T] )` 3. Apply `call` signature `( ..a Q -- ..b )`: - `..a` unifies with `( ..rest Int )` - `Q` unifies with `Quot[...]` - `..b` is fresh and **NOT constrained by the quotation's effect** 4. Result stack is `..b` (unconstrained) 5. Word's declared output `( ..rest Int )` unifies with `..b` - always succeeds! The quotation's actual effect `( ..x T -- ..x T T )` is never applied. ### The Fix `infer_word_call` needs special handling for `call`: ```rust if name == "call" { // Pop quotation from stack let (remaining_stack, quot_type) = current_stack.pop()?; // Extract quotation's effect let quot_effect = match quot_type { Type::Quotation(effect) => effect, Type::Closure { effect, .. } => effect, _ => return Err("call requires quotation"), }; // Apply the quotation's effect to remaining stack return self.apply_effect(&quot_effect, remaining_stack, "call"); } ``` This would properly propagate the quotation's stack effect through `call`. ### Scope This affects: - `call` builtin - Possibly `bi`, `dip`, `keep`, and other combinators that invoke quotations - Each combinator may need special handling to properly propagate quotation effects

navicore commented

2026-01-10 23:22:43 +00:00

(Migrated from github.com)

Fix Implemented

Added special handling for call in infer_word_call (typechecker.rs:1017-1071):

fn infer_call(&self, current_stack: StackType) -> Result<(StackType, Subst, Vec<SideEffect>), String> {
    // Pop the quotation from the stack
    let (remaining_stack, quot_type) = current_stack.clone().pop()?;
    
    // Extract the quotation's effect
    let quot_effect = match &quot_type {
        Type::Quotation(effect) => effect.clone(),
        Type::Closure { effect, .. } => effect.clone(),
        Type::Var(_) => { /* fall back to polymorphic behavior */ }
        _ => return Err("call: expected quotation or closure"),
    };
    
    // Freshen and apply the quotation's effect
    let fresh_effect = self.freshen_effect(&quot_effect);
    self.apply_effect(&fresh_effect, remaining_stack, "call")
}

Test Results

All 9 pollution tests now pass:

✅ test_pollution_extra_push
✅ test_pollution_extra_dup
✅ test_pollution_consumes_extra
✅ test_pollution_in_then_branch
✅ test_pollution_in_else_branch
✅ test_pollution_both_branches_extra
✅ test_pollution_branch_consumes_extra
✅ test_pollution_quotation_wrong_arity_output (previously failing)
✅ test_pollution_quotation_wrong_arity_input (previously failing)

Full test suite passes (255+ tests).

Other Combinators

Checked times, while, until - these correctly use the same row variable throughout their signatures:

times: ( ..a Quotation[..a -- ..a] Int -- ..a )

The row variable ..a is shared, so the quotation's effect is properly constrained by unification. Only call had independent row variables.

Note on `dip`, `keep`, `bi`

These combinators don't exist in the language yet. If/when added, they should follow the pattern of using shared row variables, not the broken call pattern.

## Fix Implemented Added special handling for `call` in `infer_word_call` (typechecker.rs:1017-1071): ```rust fn infer_call(&self, current_stack: StackType) -> Result<(StackType, Subst, Vec<SideEffect>), String> { // Pop the quotation from the stack let (remaining_stack, quot_type) = current_stack.clone().pop()?; // Extract the quotation's effect let quot_effect = match &quot_type { Type::Quotation(effect) => effect.clone(), Type::Closure { effect, .. } => effect.clone(), Type::Var(_) => { /* fall back to polymorphic behavior */ } _ => return Err("call: expected quotation or closure"), }; // Freshen and apply the quotation's effect let fresh_effect = self.freshen_effect(&quot_effect); self.apply_effect(&fresh_effect, remaining_stack, "call") } ``` ### Test Results All 9 pollution tests now pass: - ✅ `test_pollution_extra_push` - ✅ `test_pollution_extra_dup` - ✅ `test_pollution_consumes_extra` - ✅ `test_pollution_in_then_branch` - ✅ `test_pollution_in_else_branch` - ✅ `test_pollution_both_branches_extra` - ✅ `test_pollution_branch_consumes_extra` - ✅ `test_pollution_quotation_wrong_arity_output` (previously failing) - ✅ `test_pollution_quotation_wrong_arity_input` (previously failing) Full test suite passes (255+ tests). ### Other Combinators Checked `times`, `while`, `until` - these correctly use the **same** row variable throughout their signatures: ``` times: ( ..a Quotation[..a -- ..a] Int -- ..a ) ``` The row variable `..a` is shared, so the quotation's effect is properly constrained by unification. Only `call` had independent row variables. ### Note on `dip`, `keep`, `bi` These combinators don't exist in the language yet. If/when added, they should follow the pattern of using shared row variables, not the broken `call` pattern.

navicore commented

2026-01-10 23:27:35 +00:00

(Migrated from github.com)

https://github.com/navicore/patch-seq/pull/232