Skip to content

execution_tape: add aggregate ABI shape metadata#89

Merged
waywardmonkeys merged 1 commit into
forest-rs:mainfrom
waywardmonkeys:execution-tape-agg-shape-abi
May 31, 2026
Merged

execution_tape: add aggregate ABI shape metadata#89
waywardmonkeys merged 1 commit into
forest-rs:mainfrom
waywardmonkeys:execution-tape-agg-shape-abi

Conversation

@waywardmonkeys
Copy link
Copy Markdown
Contributor

Keep ValueType::Agg as the runtime ABI kind, but add optional FunctionArgAggShapeEntry metadata to the Program container so frontends can refine aggregate arguments for verification. ProgramBuilder now accepts FunctionAbi in checked function entry points while preserving FunctionSig call sites via Into.

Seed verifier aggregate facts from ABI argument shapes at function entry, including tuple element types, struct type ids, and array element ids. This lets closure bodies project typed values from the hidden environment argument without routing internal capture reads through host calls.

Migration: existing FunctionSig-based builder calls continue to compile; code that needs typed aggregate arguments can use FunctionSig::with_arg_agg_shape or FunctionSig::closure_body_with_env_shape.

Keep ValueType::Agg as the runtime ABI kind, but add optional FunctionArgAggShapeEntry metadata to the Program container so frontends can refine aggregate arguments for verification. ProgramBuilder now accepts FunctionAbi in checked function entry points while preserving FunctionSig call sites via Into<FunctionAbi>.

Seed verifier aggregate facts from ABI argument shapes at function entry, including tuple element types, struct type ids, and array element ids. This lets closure bodies project typed values from the hidden environment argument without routing internal capture reads through host calls.

Migration: existing FunctionSig-based builder calls continue to compile; code that needs typed aggregate arguments can use FunctionSig::with_arg_agg_shape or FunctionSig::closure_body_with_env_shape.
@waywardmonkeys waywardmonkeys merged commit ba76d66 into forest-rs:main May 31, 2026
15 checks passed
@waywardmonkeys waywardmonkeys deleted the execution-tape-agg-shape-abi branch May 31, 2026 12:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant