Migrated from Method backlog
This issue was created from a legacy filesystem backlog card. GitHub Issues are now the live work tracker; repository docs remain Method evidence.
Source backlog: docs/method/backlog/up-next/KERNEL_dynamic-footprint-binding-runtime.md
Original lane: up-next
Original legend: KERNEL
Original backlog card
Dynamic Footprint Binding Runtime
- Lane:
up-next
- Legend:
KERNEL
- Rank:
1
Why now
Echo now has the first compile-checked proof that a Wesley-generated bounded
rewrite interface can prevent undeclared capability access.
That proof still assumes a flat footprint. Real hot-graph rewrites need
dynamic binding:
- direct slot binding from args
- relation-based slot binding
- closure derivation over runtime graph truth
Without an explicit runtime model for those bindings, the stack risks either
freezing at toy footprints or reopening ad hoc traversal in handwritten Rust.
Hill
Echo defines the runtime binding model for structured footprints so that:
- Wesley owns static slot/closure grammar
- Echo owns concrete binding and closure resolution
- implementations still cannot escape the declared capability surface
Done looks like
- one Echo design note states the static-schema / dynamic-binding split
- one runtime-facing backlog item names the binding steps:
- bind direct slots
- bind relation-derived slots
- resolve declared closures
- enforce cardinality/basis validity
- one motivating rewrite shape, such as
ReplaceRangeAsTick, is described in
those terms
- the next runtime proof slice is obvious: bind one structured rewrite without
reopening arbitrary traversal
Repo Evidence
docs/invariants/DECLARATIVE-RULE-AUTHORSHIP.mddocs/design/0012-dynamic-footprint-binding-runtime.mddocs/method/backlog/up-next/PLATFORM_footprint-honesty-rewrite-proof-slice.mdcrates/echo-wesley-gen/tests/rewrite_api_contract.rs
Migrated from Method backlog
This issue was created from a legacy filesystem backlog card. GitHub Issues are now the live work tracker; repository docs remain Method evidence.
Source backlog:
docs/method/backlog/up-next/KERNEL_dynamic-footprint-binding-runtime.mdOriginal lane:
up-nextOriginal legend:
KERNELOriginal backlog card
Dynamic Footprint Binding Runtime
up-nextKERNEL1Why now
Echo now has the first compile-checked proof that a Wesley-generated bounded
rewrite interface can prevent undeclared capability access.
That proof still assumes a flat footprint. Real hot-graph rewrites need
dynamic binding:
Without an explicit runtime model for those bindings, the stack risks either
freezing at toy footprints or reopening ad hoc traversal in handwritten Rust.
Hill
Echo defines the runtime binding model for structured footprints so that:
Done looks like
ReplaceRangeAsTick, is described inthose terms
reopening arbitrary traversal
Repo Evidence
docs/invariants/DECLARATIVE-RULE-AUTHORSHIP.mddocs/design/0012-dynamic-footprint-binding-runtime.mddocs/method/backlog/up-next/PLATFORM_footprint-honesty-rewrite-proof-slice.mdcrates/echo-wesley-gen/tests/rewrite_api_contract.rs