feat(laurel): dynamic method dispatch + behavioral-subtyping (Liskov) checking by fabiomadge · Pull Request #3 · fabiomadge/Strata

fabiomadge · 2026-06-25T08:39:40Z

Dynamic method dispatch + behavioral-subtyping (Liskov) checking

Stacked on strata-org#1394 (laurel-polymorphism-landing). This PR's diff shows only the dispatch feature; review after the polymorphism PR. It will be retargeted to the org base once strata-org#1394 merges.

Adds runtime virtual dispatch for composite methods and the behavioral-subtyping check that makes it sound.

What it does

Virtual dispatch. A method call on a Parent-typed reference that actually holds a Child now runs Child's override. Each overridden method m gets a generated dispatcher T$m over the per-type implementations T$m$impl, branching on the runtime type tag, most-derived-first:
if self is O then (self as O)#O$m$impl(...) else ... else D$m$impl(self, ...).
Postconditions are tag-conditioned so a call through a base reference still gets the precise guarantee of the dynamic type.
Behavioral subtyping (Liskov). A new CheckOverrideRefinement pass emits synthetic checker procedures enforcing precondition contravariance (requires Parent.pre; assert Child.pre) and postcondition covariance (assume Child.post; assert Parent.post). It reuses the normal contract→Core lowering — no new Core construct. A Liskov-violating override is rejected.
Generic inheritance. Generic families (SBox<T> extends Box<T>) dispatch virtually and are Liskov-checked, riding the existing procedure monomorphizer — zero new monomorphization machinery (the integration that validated the polymorphism design).
Heap-status unification. unifyDispatchFamilyHeap propagates a dispatcher's read/write heap-status down to every $impl it calls and re-closes the transitive fixpoint, so mixed-modifies families (base no-op, override mutates) thread $heap uniformly and the dispatcher if joins.

Soundness coupling

A single shared gate isVirtualDispatchMethod keys both dispatcher generation and Liskov checking, maintaining the invariant {virtually-dispatched} == {Liskov-checked} — a method can't get a virtual dispatcher without also being refinement-checked. The modifies-subset obligation falls out for free via the dispatcher frame (a frame-widening override is correctly rejected).

Scope / coverage

Verified sound + complete across non-generic, generic, void-heap-writer, and mixed-modifies families. New corpus cases in a dedicated dynamicDispatchCorpus list (generic_dispatch_*, void_heapwriter_dispatch_*, mixed_modifies_*). Full lake test green (only the pre-existing ion-java JAR failure).

Known deferred follow-up (not blocking): the isVirtualDispatchMethod gate-coupling is currently spread across three sites (dispatcher body order, the gate predicate, the Liskov pass); an ergonomic refactor to make the coupling structurally obvious is a C-internal cleanup.

Update — two-state Liskov fix + test coverage (post-coverage-audit)

A coverage audit of the dispatch tests surfaced one real defect and several untested shapes; both are now addressed here.

Two-state (old()) Liskov refinement fix. The behavioral-subtyping post-checker was emitted heap-neutral, so HeapParameterization never gave it an inout $heap and PushOldInward collapsed every old(field) to the current heap — making any old(...)-using refinement obligation vacuous, so a Liskov-violating two-state override (e.g. parent ensures c#v >= old(c#v), child ensures c#v == old(c#v) - 1) was silently accepted at definition time. (Not exploitable end-to-end — call sites re-prove refinement via the dispatcher frame — but a definition-time diagnostics gap.) Fixed by making the post-checker two-state-faithful: it emits a bodyless $childspec companion carrying the child's post + modifies (→ heap-writer) and calls it, proving the parent's post via its own ensures (so ModifiesClauses conjoins the parent frame). Reuses the same machinery that already rejects frame-widening at dispatch call sites. As a bonus this subsumes the previously-deferred modifies-subset check (a frame-widening override is now rejected at definition time too). Scope was pinned by an adversarial design sweep (54 probes executed against the real pipeline): the fix needs only old() — fresh() is NotYetImplemented at the Core translator and Set frames have no surface syntax, so both are unreachable.

Refactor. Extracted the shared mkCallAssigningOutputs (the dispatcher and the Liskov checker both hand-rolled the same .StaticCall/.Assign-over-outputs shape) into MapStmtExpr, alongside the contract/boolean helpers extracted earlier.

Tests. Moved the dispatch corpus into its own DynamicDispatchTest.lean (one-feature-per-test-file), and added shape-coverage cases the audit found working but unpinned: sibling / non-linear hierarchy (the only shape exercising the most-derived-first dispatcher ordering), multi-output dispatch, multi-arg-in-postcondition, field-receiver dispatch, transitive (in-body) dispatch, a non-overridden method coexisting with an overridden one, a reader-only family, the reverse mixed-modifies direction, and the old() violation/sound twins. Full lake test green (only the pre-existing ion-java JAR failure).

Adds CheckOverrideRefinementPass, run first in the pipeline (while methods are still on their composites). For every non-generic composite method that overrides an ancestor method, it emits synthetic checker procedures verifying behavioral subtyping: * precondition contravariance — Parent.pre ⇒ Child.pre * postcondition covariance — Child.post ⇒ Parent.post A checker is an ordinary procedure (`requires Parent.pre opaque { assert Child.pre }`, etc.), so it reuses the existing contract→Core lowering with no new construct, and a failure surfaces as a normal 'assertion could not be proved' at the offending override. This closes two soundness gaps that were latent under static dispatch and become load-bearing for dynamic dispatch: a Liskov-violating override (e.g. Parent `ensures r>=0`, Child `ensures r==-5`) was previously ACCEPTED, and a modular helper assuming the parent's contract verified a guarantee that a violating override would break at runtime. Purely additive (appends checkers); generic families are gated out for now (a checker's `self: C<T>` param can't be seeded by the procedure monomorphizer) — they keep static dispatch, which is sound.

Makes non-generic method dispatch DYNAMIC: a call on a statically-Parent-typed receiver holding a more-derived value now runs the derived override (Java/C# semantics), where before it statically bound the declared type's method. LiftInstanceProcedures now, for a method overridden within a (non-generic) inheritance family, lifts each type's real body to `T$m$impl` and generates the public `T$m` as a runtime-tag DISPATCHER: if self is O1 then O1$m$impl(self as O1, ..) else .. else T$m$impl(self, ..) over the descendant-overriders (most-derived first, via computeAncestors order). The dispatcher's postconditions are tag-conditioned: the owner's own posts guarded by the fallthrough condition, plus `(self is Oi) ==> Oi.post` for each overrider — so a caller that knows the runtime tag recovers the override's stronger contract through a Parent reference. (Uses the heap-neutral `as` lowering fixed earlier.) Sound by construction: each branch's $impl postcondition discharges the dispatcher's corresponding clause, and the Liskov pass (previous commit) guarantees every override refines its parent, so the owner contract holds on every path. Methods overridden nowhere keep the plain static lift (byte-identical), and generic inheriting families keep static dispatch (a follow-up: dispatcher `is`/`$impl` references over generics aren't yet discovered by the procedure monomorphizer). Adds a dynamicDispatchCorpus: virtual dispatch through a Parent reference, modular dynamic dispatch, a 3-level refining hierarchy, Liskov-violation rejections, and soundness (false-assert) twins.

…ride gate Retrospective cleanup of the Liskov + dynamic-dispatch code. Two pure refactors and one soundness fix that the dedup surfaced. REFACTOR (items 1-2, behavior-preserving): - Extract shared StmtExprMd builders into MapStmtExpr: andMd/impliesMd/notMd, conjoinAnd, and alignParamMap/renameProcLocals (positional source->target param renaming). CheckOverrideRefinement (renameLocals+alignParams+conjoinConditions) and LiftInstanceProcedures.dispatcherPosts both hand-rolled these; they now share one implementation. Byte-identical renaming at both sites (inputs-then-outputs, outputs win on collision, zip-truncate on arity mismatch, only .Var(.Local) leaves); the And-folds are SMT-equivalent (leading-true is the .And identity). renameProcLocals argument order is load-bearing (source = the contract's owner). SOUNDNESS FIX (item 3): the dispatcher gate (familyIsGeneric, keyed on composite type params) and the Liskov-checker gate (keyed on parameter TYPES, skipping .Applied/.TVar) were expressed differently and DIVERGED. A method whose parameter had an .Applied type (e.g. b: Box<int>) on a non-generic composite got a virtual DISPATCHER but NO refinement checker, so a Liskov-violating override (child ensures r == -1 under parent ensures r >= 0) was silently ACCEPTED instead of rejected. (The dispatcher's tag-conditioned posts kept it from a verifiably-false guarantee at call sites, so it was an incoherent-program-accepted bug, not an exploitable miscompile -- but the verifier should reject it.) Both passes now gate on ONE shared predicate isVirtualDispatchMethod (in LiftInstanceProcedures), so the invariant {virtually-dispatched methods} = {Liskov-checked methods} holds by construction and the gates cannot drift again. Adds corpus cases liskov_applied_param_violation_caught / _sound_ok. All Laurel tests + Core/MapStmtExpr consumers green.

… families Removes the familyIsGeneric gate that restricted virtual dispatch (and override- refinement checking) to non-generic families. A generic inheriting family like SBox<T> extends Box<T> now dispatches dynamically and is Liskov-checked, same as a non-generic one. Scoping predicted two gaps; de-risking confirmed they were all of them (no third gap), and a full regression is clean. GAP B (tag-test type shape): the dispatcher BODY already tested self is SBox<T> (applied), but dispatcherPosts built the tag-conditioned postconditions with a bare .UserDefined SBox, which re-resolution's Synth.isType rejects as an un-applied generic. Factored a shared appliedTagType helper used by BOTH the body and the posts so the two tag-tests cannot drift (a drift would test a different type than the body dispatches on -- a soundness hole or a resolution failure). For non-generic families appliedTagType returns the same bare .UserDefined as before (behavior-preserving). GAP A (checker monomorphization): a Liskov checker over a generic override has a self : C<T> parameter, but mkChecker set typeArgs := [], so indexGenerics never indexed it as a poly proc and its C<T> survived un-monomorphized. The checker now carries the child composite's type params (ct.typeArgs ++ child.typeArgs), mirroring how lifted methods do, so it monomorphizes per instantiation. The shared isVirtualDispatchMethod gate still couples dispatcher + checker, so the soundness invariant {virtual} = {Liskov-checked} holds for generic families too. Adds corpus cases: generic_dispatch_runtime_override(+_wrong), generic_liskov_violation_caught, generic_dispatch_multi_instantiation. NOTE: a non-generic composite extending a generic INSTANTIATION (IntBox extends Box<int>) still does not type-check -- a pre-existing generic-upcast limitation, unrelated to dispatch (the upcast var b: Box<int> := new IntBox fails on its own).

…patcher fallthrough) A method that was BOTH overridden (dispatched) AND a void heap-writer (a modifies clause, no return value) failed to translate with "Internal error: resolution after 'ModifiesClausesTransform': 'if' branches have incompatible types 'Heap' and 'void'". Root cause in buildDispatcherBody: the dispatcher is an if-chain whose `then` branches are always `.Block`s but whose `else` (fallthrough) was a BARE call. An `if` synthesizes and joins both branch types (Synth.ifThenElse), and for a void heap-writer the `$heap`-threaded call synthesizes a different type bare vs as a block tail (Heap vs void), so the join failed. Non-void dispatchers were unaffected because their branches carry an explicit value (the assigned output), making both sides agree; void non-heap and heap-writer-without-override were unaffected because no dispatcher `if` is generated. Fix: wrap the fallthrough in a `.Block` so it is structurally symmetric with the `then` branches. Verified: void heap-writer dispatch now translates and (with a postcondition) dispatches dynamically — Parent ref holding Child conveys the override's `ensures c#v == N`, false reads fail. Int-returning, generic, and void-non-heap dispatch all still pass; full Laurel regression clean. Adds corpus cases void_heapwriter_dispatch_translates / _wrong. This was a pre-existing gap in virtual dispatch (commit 81261df01), fail-loud so sound, now closed — surfaced while scoping the modifies-subset Liskov work.

…ch) + correct stale generic-dispatch comments MIXED-MODIFIES DISPATCH BUG (found by the campaign retrospective adversary; the same class as the void-heap-writer bug fixed in c050fc69c, one generalization out). A virtual-dispatched override family where parent and child differ in heap-status — parent method heap-neutral, override declares `modifies` (or vice versa) — failed to translate: the dispatcher's `if` chain joined a $heap-threaded branch (value Heap) with a void branch and died with "Internal error: 'if' branches have incompatible types 'Heap' and 'void'". Heap-writer status is computed PER `$impl`, so a mixed family's dispatcher branches disagreed. Fix (HeapParameterization.unifyDispatchFamilyHeap): a dispatch family's `$impl` procs must share heap read/write status. The dispatcher is already classified read/write transitively (it calls a reader/writer branch), so propagate that DOWN to every `$impl` it calls, then re-close the transitive fixpoint. Now both branches thread $heap uniformly. Identified structurally (a "dispatcher" is any proc calling an `…$impl`), not by a bespoke name shape. Verified: mixed families translate and dispatch correctly (the override's post is conveyed through a base reference); uniform families, plain heap-writers, and int dispatch are unaffected. A genuine Liskov FRAME-WIDENING override (parent modifies nothing, child modifies c) is now correctly REJECTED — the dispatcher cannot prove the parent's empty frame when the override mutates c (the modifies-subset obligation, enforced for free via the dispatcher frame). Full Laurel regression clean. Also (retrospective GO cleanups, comments only): corrected three stale comments (LiftInstanceProcedures, CheckOverrideRefinement, the corpus header) that still claimed generic inheritance families "keep static dispatch / are gated off" — contradicted by commits 8/9 which made generic dispatch+Liskov work. (The bodyPostconditions dedup was SKIPPED: moving it to LaurelAST means cutting a mutual block, and the reverse import is a cycle — not worth disrupting for 4 trivial lines.) Adds corpus cases mixed_modifies_dispatch_translates / mixed_modifies_frame_widen_rejected.

The behavioral-subtyping post-checker emitted by CheckOverrideRefinement was heap-neutral (empty modifies, body only `assert`), so HeapParameterization never gave it an inout `$heap`. PushOldInward then collapsed every `old(field)` in the assumed Child.post / asserted Parent.post to the current heap, making any two-state (`old(...)`) refinement obligation VACUOUS — a Liskov-violating two-state override (e.g. parent `ensures c#v >= old(c#v)`, child `ensures c#v == old(c#v) - 1`) was silently accepted at definition time. (Single-state posts were unaffected, which is why the bug was specific to `old()`.) Not exploitable end-to-end — call sites re-prove refinement via the dispatcher frame — but a definition-time diagnostics gap. Fix: make the post-checker two-state-faithful by reusing the proven dispatcher-frame mechanism rather than hand-rolling havoc. For each overriding method emit a bodyless `$childspec` companion carrying the CHILD's post + modifies (`impl.isNone && !modif.isEmpty` => HeapParameterization classifies it a heap-writer), and rewrite the post-checker to CALL it and prove the PARENT's post via its own `ensures`, carrying the PARENT's modifies. Calling a heap-writer makes the checker a transitive heap-writer, so it gains an inout `$heap` and `old()` survives PushOldInward; CallElim havocs the heap per the companion (child) frame and assumes Child.post, then the checker must re-establish Parent.post AND the parent frame over the havoc'd heap. This is the same path that already rejects frame-widening at dispatch call sites. The pre-checker (single-state contravariance) is unchanged. Scope (established by an adversarial design sweep + executing 54 probes against the real pipeline): the fix only needs `old()` — `fresh()` is NotYetImplemented at the Core translator (any fresh() post fails translation, fail-loud not wrong-accept) and `Set` frames have no surface syntax (unconstructible). All 14 previously-vacuous two-state violations are now caught (single-field, multi-field, generic, skip-level, nested old(), old() in forall, both-wildcard); no sound override is over-rejected. mixed_modifies_frame_widen_rejected now fails ×2 (was ×1): the frame-widening is correctly caught BOTH at the dispatcher call site AND, now, at definition time by this post-checker — two correct rejections of the same violation. 5 new corpus cases (old_liskov_*). Full lake test green (only the pre-existing ion-java JAR).

… Liskov checker The dynamic-dispatch dispatcher (buildDispatcherBody's callTo) and the two-state Liskov post-checker (refinementCheckers) both hand-rolled the identical shape: build a `.StaticCall`, and if the callee returns values wrap it in an `.Assign` over one `.Local` target per output (bare call when void). Extract it as `mkCallAssigningOutputs` in MapStmtExpr, alongside the andMd/alignParamMap helpers that were extracted from the same two passes earlier (03aea9f23). Removes the duplicated call-builder so the two sites can't drift. Pure refactor — behavior byte-identical; full lake test green (only the pre-existing ion-java JAR).

…ge cases Move the dynamicDispatchCorpus (dispatch + Liskov cases) out of PolymorphismCorpusTest into its own DynamicDispatchTest.lean, matching the repo's one-feature-per-test-file convention (dynamic dispatch is a distinct capability: runtime-tag dispatchers + override-refinement checking). Auto-discovered by the `StrataTest.+` glob; nothing imported the corpus, so the split is mechanical. Add 10 cases pinning dispatcher/checker shapes a coverage audit found working but untested: sibling / non-linear hierarchy (+ wrong twin) — the only shape exercising the most-derived-first qsort ordering; multi-output dispatch (+ wrong twin); multi-arg method with the argument in the postcondition; dispatch through a field receiver; transitive (in-body) dispatch; a non-overridden method coexisting with an overridden one; a reader-only family; and the reverse mixed-modifies direction (parent writer, child neutral). Full lake test green (only the pre-existing ion-java).

…nditions; deterministic sibling order Outcome of an adversarial design review of the dispatch + Liskov passes. The review confirmed the design is sound (the shared isVirtualDispatchMethod gate, qsort most-derived-first ordering incl. non-linear hierarchies, tag-conditioned posts, and the two-state companion encoding all hold up — verified by execution). It surfaced four small, soundness-neutral cleanups, applied here: 1. Virtual-dispatch family NAMING centralized into MapStmtExpr (liftedProcName, implProcName, implTag, isImplProc, dispatchCastName, refinementProcName). The `$impl` marker and its detection previously lived in TWO files — minted by implProcName (LiftInstanceProcedures) and matched by an inline `splitOn "$impl"` in HeapParameterization.unifyDispatchFamilyHeap — which could drift and silently break impl-callee detection (the mixed-modifies heap fix). Now one definition; isImplProc is documented as a SUBSTRING test (not endsWith) because monomorphization appends `$a{n}$…` after `$impl` (Box$get$impl$a1$int). Minted strings are byte-identical. 2. nonFreeConditions helper for the `filter (fun c => !c.free)` pattern (7 sites across the dispatcher posts and the Liskov pre/post checkers), with a doc note that a free (assumed) condition must never be exposed as a guarantee. 3. Liskov refinement checker name-mangling routed through refinementProcName (subsumed by #1). 4. descendantOverriders: equal-distance SIBLINGS now ordered by name. qsort is not stable, so sibling order was otherwise an arbitrary artifact of program.types declaration order; the tiebreaker makes it deterministic and source-order-independent. Sound either way (dispatch is by runtime tag, not branch position). Pure refactor + one determinism fix; full lake test green (only the pre-existing ion-java JAR). 32 dispatch cases replay unchanged.

The post-covariance checker asserted Parent.post after assuming Child.post, but with `preconditions := []` — it never assumed Parent.pre. Behavioral post-covariance is `Parent.pre ⇒ (Child.post ⇒ Parent.post)`: a caller invoking the parent contract has already established Parent.pre, so a sound covariant override whose post implies the parent's only UNDER the parent precondition (e.g. parent `requires a >= 0 ensures r >= 0`, child `ensures r == a`) was spuriously OVER-REJECTED. Fix: the post-checker now assumes Parent.pre (renamed into the child's parameter names). Parent.pre — NOT Child.pre: Child.pre is contravariantly weaker and assuming it would be unsound; Parent.pre ⇒ Child.pre is enforced separately by the pre-checker. Completeness fix (was over-rejection, never wrong-accept); the genuine-violation twin still fails even with Parent.pre assumed. Surfaced by rebasing onto a base that added ContractPass (strata-org#1352), which made `requires` clauses meaningful end-to-end and exposed this latent gap. 2 new corpus cases (liskov_post_covariance_under_parent_pre + its must-fail violation twin). Full lake test green (only pre-existing ion-java).

- DynamicDispatchTest liskov_post_covariance_under_parent_pre: drop the '(Was over-rejected when the post-checker had preconditions := [])' regression-history parenthetical; keep the assume-Parent.pre rationale. - mkCallAssigningOutputs doc: drop 'both previously hand-rolled this identical shape'; the shared-helper purpose stands on its own. Comment-only; no code change.

Second pass of the comment polish (lower-tier items from the review): - SMTEncoder: drop the 'generate base name using global counter' line that restated the adjacent code; keep the reserved-prefix/uniqueness rationale. - CheckOverrideRefinement findOverriddenParent: tighten the .drop 1 comment to the self-first justification. - MapStmtExpr implTag: reword 'bare separator-tagged MARKER, NOT a suffix' to a plain 'not necessarily a trailing suffix'; keep the isImplProc/never-endsWith rule. - MonomorphizeComposites topoSort: drop the INDEX restatement (see the detailed note above) and the recursion narration. - DynamicDispatchTest sibling case: drop the 'every other case is a linear chain' parenthetical; keep the qsort-load-bearing point. Comment-only; no code change. Note: the CheckOverrideRefinement pre/post trivial-holds pair was left intact — the two lines document distinct variance directions, not a true duplicate.

Convert the 34 inline \n-escaped src programs in DynamicDispatchTest to multiline r-strings + inter-case spacing, matching the readability pass applied to the polymorphism test files. Test-only; no coverage or behavior change.

…d oracles - Add as_guarded_downcast_value_observed (+ wrong twin + unguarded twin): in a heap-writer, write through the downcast ref (c#y := 9) and read back == 9, so a broken cast can't pass vacuously. Discriminates on all axes (guarded+correct verifies; wrong value fails; unguarded fails the is-obligation). - Document why as_guarded_downcast_heap_neutral keeps assert 1==1: an opaque param in a heap-neutral proc leaves c#y genuinely unconstrained, so a concrete-value assert would be unprovable — the value is pinned by the new heap-writing case. (The failsAtLeast -> failsExactly tightening of the two precond-gated cases landed on the poly branch and flows up via rebase.)

An `x as T` cast previously lowered to a statement block `{ assert (x is T); x }`. That is correct in a body but illegal in a contract formula (a pure expression), so `(p as Child)#y` in a pre/postcondition failed to translate (NotYetImplemented) — even though `p is Child` works there. This closes that asymmetry. Lowering: TypeHierarchy synthesizes one `function downcast$T(p: T): T requires (p is T) { p }` per composite; the `is T` guard is the pure `ancestorsPerType` select-chain, so it lives in a contract formula. Composite references flatten to `Composite` right after, so the identity body type-checks as `Composite → Composite`. HeapParameterization's two `AsType` arms emit `downcast$T(x)` (a forward reference to the next pass, resolved at the following re-resolve) via the shared `downcastProcName` so emitter and definition cannot drift. PrecondElim discharges the `is T` precondition as a well-definedness obligation wherever the helper is called — body or contract — so an unprovable downcast fails loud; no PrecondElim change was needed. Sound: an unguarded/invalid downcast still fails (the obligation is preserved, not dropped) — e.g. T5_inheritance's `a as Extender` (a: Base) still errors; its annotation widens from the inner `as` node to the enclosing statement, matching where the obligation now attaches. Two new GenericMethodTest cases pin the contract-cast (verifies) + its must-fail wrong twin. Full lake test green (only the pre-existing ion-java JAR).

…gelog phrasing in GenericMethodTest Review findings on GenericMethodTest: - Delete the stale section-doc line claiming '`extends` on a generic composite is still rejected loud' — flatly contradicted by the generic_extends_*/generic_upcast_* cases below it, which use generic `extends` and verify. - Pin diamond_field_generic_receiver to .rejected (some .UserError): bare .rejected only checks !translated, which a .StrataBug internal error also satisfies — so a regression from clean-reject to internal-error would keep the test green, defeating the exact guarantee its `why` promises. Confirmed it fires .UserError today. - Strip changelog/history phrasing from 4 comments + 5 why strings ('the bug fixed here', 'previously NotYetImplemented', 'the reverted unsound upcast', etc.), keeping the mechanism. Also cut the ~90-word heap-neutral `why` to its durable core. No coverage change; all 42 cases pass.

…(GenericMethodTest) Optional review follow-ups: - Pin .rejected (some .UserError) on the four wrong-target upcast cases (generic_upcast_remap/concretization_wrong_target, concrete_extends_geninst_wrong_target/ remap_swap) — same enforcement gap the diamond fix closed: bare .rejected can't tell a clean UserError from a StrataBug internal error. Confirmed all four fire .UserError. - Add 4 coverage-gap cases (all outcomes verified by probe): generic_upcast_same_inst_wrong_value (the missing must-fail twin), field_tvar_inherited_remap_write_correct (positive twin), diamond_single_parent_field (a uniquely-inherited field on a diamond shape still verifies — only the ambiguous field rejects), and as_guarded_downcast_generic_inst (the generics × as-cast intersection). 42 → 46 cases; full lake test green (only the pre-existing ion-java JAR).

A correctness pass over the file's comments found three issues (mechanism claims otherwise verified accurate): - Line 112: a circular sentence I introduced in the last trim ('emitted AFTER the parent ... so the parent must be emitted before the child' restated itself) — rewritten to state the actual reason (child's scope is built from the parent's). - Two changelog fragments that survived the earlier trim because they were mid-sentence, not trailing tags: 'an earlier non-substituting version accepted the WRONG supertype' and 'the old assert-block lowering was statement-shaped' — reworded to state current behavior. Comment-only; all 46 cases pass.

dispatch_sibling_holds_child2's comment/why claimed it exercises 'load-bearing most-derived-first qsort ordering' — but descendantOverriders (LiftInstanceProcedures) states sibling order is a determinism-only name tiebreaker, sound either way (dispatch is by runtime tag, a value is exactly one sibling's type). Reword to state what it actually pins: equal-distance-sibling dispatch by runtime tag, branch order irrelevant to correctness. (Load-bearing ordering is the linear ancestor-overlap case, dispatch_three_level.) Comment-only.

Describe the dispatch/Liskov mechanism as it IS rather than narrating what changed: drop 'was gated to static before', 'previously failed to translate', and 'was vacuously accepted when the checker was heap-neutral'; keep the mechanism (applied tag-tests, block-wrapped fallthrough, two-state $childspec companion) and what each case pins.

Remove per-case label comments that restate the case's own `why` field (Liskov enforcement labels, sound-override, field-receiver, reader-only, modular-dispatch, three-level, virtual-dispatch), the SHAPE-COVERAGE audit-history preamble, and the file-organization sentence in the module docstring. Kept the load-bearing section docstring (dispatcher mechanism) and the reverse-mixed-modifies cross-reference to its complement case. Comments only.

Three history sentences turned into forward-looking WHY: the post-checker's 'old buggy encoding emitted heap-neutral' blow-by-blow -> 'it MUST be a heap-writer, or a two-state post is vacuous' (the actual constraint, tightened); the shared-gate 'Previously ... DIVERGED ... closes that gap' -> 'the two gates MUST stay one predicate, or a violating override is silently accepted' (the invariant + its risk); dropped the module-doc 'This was previously deferred; the old() fix subsumed it' trailer. Load-bearing warnings kept. Verified by execution first: weaker-post/stronger-pre/two-state-old all REJECT, sound override VERIFIES. Comments only; builds + DynamicDispatchTest green.

…DispatchMethod The docstring stated the current truth (generic families supported: applied tag-tests + type-param-carrying checker) and THEN narrated the removed familyIsGeneric gate ('An earlier clause gated generics off; both gaps now fixed'). Dropped the history; the current statement stands on its own. Verified the dispatch hunk sound by execution first: virtual dispatch runs the override (asserting the parent value FAILS), tag-conditioned posts recover Parent.post through a Parent ref, generic SBox<T> dispatches. Comment only.

…raint (HeapParam) The AsType->downcast$T comment contrasted with 'the old { assert (x is T); x } block was illegal' — reworded to state the actual constraint directly (a contract formula cannot contain a statement assert-block, so the cast routes through the downcast$T helper call). Left unifyDispatchFamilyHeap's docstring intact (load-bearing: the Heap/void-join problem + promote-then-close mechanism). Verified by execution: mixed-modifies dispatch family translates + verifies (no Heap/void crash), as-in-contract works; the downcast guard- discharge matrix incl. the must-fail unguarded case is corpus-pinned. Comment only.

fabiomadge force-pushed the laurel-polymorphism-landing branch from 6f2fd1f to e17001b Compare June 26, 2026 14:51

fabiomadge force-pushed the laurel-dynamic-dispatch branch from 8a57084 to 3e738d8 Compare June 26, 2026 14:51

fabiomadge force-pushed the laurel-dynamic-dispatch branch 2 times, most recently from ec57e1e to 8519b99 Compare July 14, 2026 10:57

fabiomadge force-pushed the laurel-polymorphism-landing branch from 9bdcf19 to 622bfcd Compare July 14, 2026 11:43

fabiomadge force-pushed the laurel-dynamic-dispatch branch from 8519b99 to dced378 Compare July 14, 2026 11:43

fabiomadge force-pushed the laurel-polymorphism-landing branch from 622bfcd to e9410e9 Compare July 14, 2026 11:54

fabiomadge force-pushed the laurel-dynamic-dispatch branch 2 times, most recently from 422d757 to e6ce215 Compare July 14, 2026 13:19

fabiomadge force-pushed the laurel-polymorphism-landing branch from b2f93ed to 9657493 Compare July 14, 2026 14:17

fabiomadge force-pushed the laurel-dynamic-dispatch branch from e6ce215 to 1e750c4 Compare July 14, 2026 14:17

fabiomadge force-pushed the laurel-polymorphism-landing branch from 9657493 to 4350d40 Compare July 14, 2026 14:53

fabiomadge force-pushed the laurel-dynamic-dispatch branch 18 times, most recently from 14e04e8 to ce8a2db Compare July 16, 2026 10:20

fabiomadge force-pushed the laurel-dynamic-dispatch branch 3 times, most recently from 6f293ce to 2ed6dd9 Compare July 17, 2026 23:23

fabiomadge added 25 commits July 18, 2026 01:43

test(laurel): readable multiline src in DynamicDispatchTest

c363a28

Convert the 34 inline \n-escaped src programs in DynamicDispatchTest to multiline r-strings + inter-case spacing, matching the readability pass applied to the polymorphism test files. Test-only; no coverage or behavior change.

fabiomadge force-pushed the laurel-dynamic-dispatch branch from 2ed6dd9 to 5a32884 Compare July 17, 2026 23:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(laurel): dynamic method dispatch + behavioral-subtyping (Liskov) checking#3

feat(laurel): dynamic method dispatch + behavioral-subtyping (Liskov) checking#3
fabiomadge wants to merge 25 commits into
laurel-polymorphism-landingfrom
laurel-dynamic-dispatch

fabiomadge commented Jun 25, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

fabiomadge commented Jun 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Dynamic method dispatch + behavioral-subtyping (Liskov) checking

What it does

Soundness coupling

Scope / coverage

Update — two-state Liskov fix + test coverage (post-coverage-audit)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

fabiomadge commented Jun 25, 2026 •

edited

Loading