shoney.arickathil
8f6ff1e865
The hybrid-boundary inversion is closed: a statically provable interface
violation now fails at COMPILE time instead of reaching wovm as an ICALL
that traps WO_T_BOUNDS at runtime.
- types.ml class_satisfies: the same rule emit.ml's `satisfies` builds
vtable rows from (instance method with matching name + parameter count
for every interface method; `static fn` never satisfies) — one rule, two
consumers, so the check and the vtable can never disagree.
- check_iface_boundary fires wherever a confidently class-typed value flows
into an interface-typed slot: call arguments against the callee's declared
parameters (free fns, methods off confident receivers, interface-method
sigs, statics — resolved exactly as confident_typ resolves returns),
annotated `let`s, and `return`s. Silent when underivable.
- The same per-argument pass extends the ?T boundary to CALL ARGUMENTS
(the previous slice covered stores/returns/operands): nil into a
non-nullable parameter is WO-E212, an unnarrowed ?T argument is WO-E211.
- tests/corpus/trap/unsatisfied-interface -> compile-fail/ with
fixture.code WO-E205, per the fixture's own standing instruction; its
header comment rewritten to the wired reality.
- The new arg checks caught a real mistyped signature in the sample:
log-watcher's rpc_error/rpc_result/call_tool declared `id: json.Value`
while every caller legitimately passes nil (JSON-RPC id-absent) — now
`?json.Value`; dispatch/call_tool/cron-row sites moved to the
bind-then-narrow idiom (including an `or`-guard narrowing:
`if spath == nil or spat == nil { return }`).
- Catalog: E205 gains its main-table row; the "owed gap" section is
rewritten as closed. Board known-gap struck through.
Verified: woc-test 540/0 + test_diag 14/0; oop-e2e 83/0 (fixture now
compile-fail, satisfying-class negative probe compiles clean); oop-accept
ALL MET; log-watcher 7/0; employee 8/0; gc-cycle clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
22 lines
614 B
Text
22 lines
614 B
Text
-- WO-E205 (wired 2026-08-18; formerly trap/unsatisfied-interface, which
|
|
-- pinned the old runtime-trap behavior as a KNOWN GAP). `Rock` has no
|
|
-- `current_price` method, so it does not structurally satisfy `Priced` --
|
|
-- provable statically (the class's whole method set is known), so by the
|
|
-- hybrid-boundary doctrine it fails at COMPILE time, at the `quote(r)`
|
|
-- call site, never as the ICALL no-vtable-entry trap.
|
|
interface Priced {
|
|
fn current_price() -> Int
|
|
}
|
|
|
|
class Rock {
|
|
n: Int
|
|
}
|
|
|
|
fn quote(p: Priced) -> Int {
|
|
return p.current_price()
|
|
}
|
|
|
|
fn main() {
|
|
let r = Rock { n: 1 }
|
|
print_int(quote(r))
|
|
}
|