From 666fd2d973d7351d8f7d2e8b00fc4a11570f7a1f Mon Sep 17 00:00:00 2001 From: Codex Bot Date: Thu, 22 Oct 2026 15:41:17 +0800 Subject: [PATCH] Track conservative source effect proofs in GUI contracts --- README.md | 6 +++-- src/README.md | 2 +- src/endor_host.rs | 64 +++++++++++++++++++++++++++++++++++++++++++++++ vendor/aster | 2 +- 4 files changed, 70 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 0fbe458..942fee9 100644 --- a/README.md +++ b/README.md @@ -196,7 +196,7 @@ Native visual methods are now available on Block: `measure(mount, Constraints(mi Outside a renderer layout call, native measurement queries find intrinsic native subtree size and clamp it to the given constraints. During layout, native base methods use the staged measured children of that occurrence. Native Row/Column arrangement uses child sizes, padding and gaps; it does not stretch children to fill the supplied bounds. Hit testing uses local coordinates against the current Mount dimensions. Coordinates/dimensions must be finite and remain within the native layout limit. Width/height and constraint ranges cannot be negative or inverted. The value constructors preserve fields as ordinary objects with declared-field type checks; methods also validate their geometry when used. Whole-program static typing remains pending. -Visual, EventTarget, Children and Presentable are explicit managed Trait definitions. Block declares Visual (measure/arrange/paint/hitTest) and EventTarget (on/dispatch/onEvent); ContainerBlock declares Children (append/insert/remove/replace/move/children), inherited by Page. `ui.supports(value, capability)` queries an instance; `ui.implements(type, capability)` queries a type. `ui.implement(type, capability)` checks required methods and establishes an explicit relation. Matching member names alone never declare a capability. Aster checks source positional parameter counts, including self, when registering, creating subclasses or replacing methods; declaration and ancestor updates also validate existing affected descendants. Source and native positional intervals are checked against the canonical call count, including self; native methods without metadata cannot declare a capability; source argument/return annotations are checked at invocation as described below. Typed requirements also compare parameter/return types and known native effects. Runtime calls check actual results across delegation. Static source effect inference and formal trait syntax remain pending. +Visual, EventTarget, Children and Presentable are explicit managed Trait definitions. Block declares Visual (measure/arrange/paint/hitTest) and EventTarget (on/dispatch/onEvent); ContainerBlock declares Children (append/insert/remove/replace/move/children), inherited by Page. `ui.supports(value, capability)` queries an instance; `ui.implements(type, capability)` queries a type. `ui.implement(type, capability)` checks required methods and establishes an explicit relation. Matching member names alone never declare a capability. Aster checks source positional parameter counts, including self, when registering, creating subclasses or replacing methods; declaration and ancestor updates also validate existing affected descendants. Source and native positional intervals are checked against the canonical call count, including self; native methods without metadata cannot declare a capability; source argument/return annotations are checked at invocation as described below. Typed requirements also compare parameter/return types and known native effects. Runtime calls check actual results across delegation. A conservative bytecode proof recognizes source functions with no unproved operations as ReadOnly; full transitive source effect inference and formal trait syntax remain pending. A plain source object can declare Presentable by implementing `present(self, window: Window): Block` and calling `ui.implement(MyType, Presentable)`. `ui.present(value)` invokes this method with the calling window and checks the returned actual Block; `ui.open(value)` also opens the result in a Page. Block values pass through directly. The existing summary viewer remains the fallback for unregistered values, and merely viewing a function does not execute it. Presentation runs through the same bounded VM call sequence; there is no recursive host evaluator. A source adapter can keep the original object through fields/callbacks/bindings; [presentable.endor](examples/presentable.endor) shows a source-preserving view and GUI calls to the original object's method. Presentation methods are ordinary calls; visual measure/arrange/paint/hitTest still run read-only and check their nominal results at runtime. Source implementations of EventTarget.on/dispatch must provide the contract's canonical 3/2 arguments after self; native methods retain their existing optional convenience arguments. @@ -430,7 +430,7 @@ Public ui functions, captured state set/increment methods and native constructor Source overrides now check contravariant parameters and covariant returns at class construction, method replacement and before invocation with dynamically resolved annotations. Ancestor replacement checks overriding descendants before mutation. Forward names may defer until invocation, where unresolved or incompatible contracts fail before the body. Known native effects may only shrink; source effects remain unknown and read-only execution retains its barriers. -Visual, EventTarget, Children and Presentable now use typed Trait requirements. Registration checks parameter/return substitution and known native effects before recording the declaration, including existing descendants. Runtime calls recheck dynamic annotations and final Trait results, including delegated source/native returns. Concrete implementations retain wider parameters and optional convenience forms. Source effects remain unknown; static effect inference remains pending. See [method-contracts.endor](examples/method-contracts.endor) for real Endor widening parameters to Object and returning a MeasureResult subclass. Existing [visual-protocols.endor](examples/visual-protocols.endor) and [layout-negotiation.endor](examples/layout-negotiation.endor) exercise the typed visual methods with actual Endor code. +Visual, EventTarget, Children and Presentable now use typed Trait requirements. Registration checks parameter/return substitution and known native effects before recording the declaration, including existing descendants. Runtime calls recheck dynamic annotations and final Trait results, including delegated source/native returns. Concrete implementations retain wider parameters and optional convenience forms. Source functions outside the conservative read-only bytecode proof remain unknown; full transitive effect inference remains pending. See [method-contracts.endor](examples/method-contracts.endor) for real Endor widening parameters to Object and returning a MeasureResult subclass. Existing [visual-protocols.endor](examples/visual-protocols.endor) and [layout-negotiation.endor](examples/layout-negotiation.endor) exercise the typed visual methods with actual Endor code. Event listeners and onClick callbacks must be Functions with known metadata accepting zero arguments or one Event. If both forms work, the dispatcher passes Event. Binding computes and Task callbacks must accept zero arguments, checked before replacing a binding, adding a connection or scheduling work. Native and source callbacks follow the same rule. See [native-signatures.endor](examples/native-signatures.endor) for real native one-argument and zero-argument handlers. Event and ObjectList subclass allocators also check declared field suffixes before allocation. @@ -477,3 +477,5 @@ native callback are not implemented. See [owned-tasks.endor](examples/owned-task for real Endor code and native buttons. Typed capability methods cannot be shadowed by instance attributes. Aster checks ordinary writes, type attachment and capability declaration before changing state; queries and method invocation reject backing-store conflicts introduced through trusted host access. The render cache subscribes to these method attribute keys and validates dirty Blocks before native dispatch, so direct storage changes cannot silently leave source calls and rendering on different methods. Removing the conflicting attribute restores the instance. Class method overrides and event subscriptions keep their existing APIs. + +Aster `ObjectStore::call_effect` queries known native or conservatively proved source effects, including bound methods, without executing the function. Proved source ReadOnly methods constrain known native overrides. Shared local assignment, dynamic calls and other unproved instructions remain unknown; the runtime read-only barrier still follows actual calls and delegation. This does not establish a full source call graph or prove trusted host I/O safe. diff --git a/src/README.md b/src/README.md index 8f84dc5..b6e6238 100644 --- a/src/README.md +++ b/src/README.md @@ -5,7 +5,7 @@ | main.rs | Native window event loop, namespace state and API startup | | api.rs | Code CRUD, live Console/reset and compatibility evaluation endpoints, worker-owned session, request observation, coalesced native viewport/background-task updates, epoch checks, stale source/destination tab-drop rejection and diagnostics | | activity.rs | Bounded in-memory HTTP exchanges with marked previews and allowlisted request headers | -| endor_host.rs | Aster compilation, fresh PUT candidates retained after successful publication, shared Console/program VM, asynchronous completion/fault boundaries, bounded execution, root cleanup and AST developer tree for function/class/member assignment nodes | +| endor_host.rs | Aster compilation, fresh PUT candidates retained after successful publication, shared Console/program VM, asynchronous completion/fault boundaries, bounded execution, conservative compiled source effect query coverage, root cleanup and AST developer tree for function/class/member assignment nodes | | endor_script.rs | Batch complete inputs for Aster's Interactive parser/compiler, retain Module entry, and rebase Aster spans to the original snapshot | | ui_bridge.rs | Inheritable native nominal constructors with source fields, shared type method tables and bound receiver dispatch, configured unified Function classification and source/field/override checks with deferred typed public/native constructor signatures and split option/field preflight plus shared native arity intervals plus resolved types/unions/effects on methods, tab registry, stable-slot insertion, source-dispatched tab reorder/drop and callback registration checks, Page lifecycle/navigation and immutable frame extraction | | binding.rs | Target-owned managed property bindings, weak Subscription tokens, zero-argument callback preflight, read-only compute and borrowed dependency/output caches | diff --git a/src/endor_host.rs b/src/endor_host.rs index cfe271c..08904b3 100644 --- a/src/endor_host.rs +++ b/src/endor_host.rs @@ -3938,6 +3938,70 @@ page.render(block) ); } + #[test] + fn source_effect_queries_use_compiled_instructions_without_running_functions() { + let mut session = ReplSession::new(234).unwrap(); + session + .execute( + r#" + function simple(value: Number): Number { return value } + function forward(value: Number): Number { return simple(value) } + class ReadOnlyModel { + function check(self: ReadOnlyModel, value: Number): Number { return value } + } + model = ReadOnlyModel() + "#, + "app.main", + ) + .unwrap(); + let globals = session.candidate.globals.unwrap(); + for (name, expected) in [ + ("simple", Some(endor_core::CallEffect::ReadOnly)), + ("forward", None), + ] { + let Value::Object(function) = session + .candidate + .vm + .dict_get(globals, &Value::Text(name.into())) + .unwrap() + .unwrap() + else { + panic!("function") + }; + assert_eq!( + session + .candidate + .vm + .object_store() + .call_effect(function) + .unwrap(), + expected + ); + } + let Value::Object(model) = session + .candidate + .vm + .dict_get(globals, &Value::Text("model".into())) + .unwrap() + .unwrap() + else { + panic!("model") + }; + let Value::Object(bound) = session.candidate.vm.bind_attr(model, "check").unwrap() else { + panic!("bound") + }; + assert_eq!( + session + .candidate + .vm + .object_store() + .call_effect(bound) + .unwrap(), + Some(endor_core::CallEffect::ReadOnly) + ); + session.candidate.vm.release(bound).unwrap(); + } + #[test] fn typed_method_shadows_invalidate_cached_ancestors_and_can_be_removed() { let mut session = ReplSession::new(233).unwrap(); diff --git a/vendor/aster b/vendor/aster index 0513b96..cd25f81 160000 --- a/vendor/aster +++ b/vendor/aster @@ -1 +1 @@ -Subproject commit 0513b96dfbc3a93fbca7e885c9883c1f5b84e6fc +Subproject commit cd25f819f2dd3e9e81ae4a39176d42dec1d1954d