GitHub

Surface Direct Functions T2B Contract

Status: implemented and validated
Architecture decision: ADR-0012
Core profile: P1V0

1. Claim

For a T2B-admitted program P, exact entry inputs x, and sufficient evaluation budget:

normalize(eval_Surface(P, x).result)
=
normalize(eval_Core(verify(elaborate_T2B(P)), x).result)

The claim covers successful scalar results. Elaboration, binding, and evaluation-budget failures remain distinct typed domains. Bridge assignment log events are outside this pure relation.

2. Source shape

annotated function declaration*
T2A entry statement*

Function declarations must be one contiguous top-level prefix. Nested functions or a declaration after an entry statement fail closed.

The entry keeps T2A’s ordered Bool | I64 | F64 manifest and declared result variable.

3. Signature syntax

~ fn name($p0: Bool, $p1: I64, $p2: F64) -> F64
    statements
    ^ result_expression
~ end

Every parameter and return requires exactly one scalar annotation. Names are case-sensitive. Num, Any, predicates, missing annotations, duplicate function names, and duplicate parameter names are rejected.

Limits:

declared functions       <= 32
parameters per function  <= 32
entry inputs              <= 256
source steps              <= 256
Core nodes                <= 256

4. Function semantics

A function body has exactly one explicit value-bearing Return, and it is the last top-level statement. Earlier statements use the T2A Assign/If profile. Branch bodies cannot contain Return.

Functions can read only their parameters and locals. Surface global lookup and capture are rejected rather than silently converted into closure behavior.

All T2B functions are pure and region-free. Their declared result expression must exactly match the annotated scalar result.

5. Calls

Only name(arguments...) with a direct declared function name is admitted. Builtins, values-as-callees, inline functions, closures, and dynamic calls are rejected.

  • argument count and scalar tags match exactly;
  • arguments elaborate left-to-right;
  • a call nested in an expression becomes one ANF RValue::Call;
  • a final ^ name(arguments...) becomes Term::TailCall;
  • forward, recursive, and mutually recursive references are structurally admitted because the complete signature table is built before bodies lower.

Non-tail recursion is bounded by the Core evaluation call-depth budget. Tail recursion is bounded by the evaluation step budget.

6. Canonical form

  • Entry is function ID 0.
  • Declared functions receive IDs 1 onward in source order.
  • Functions serialize in increasing ID order.
  • Each function resets local numbering: parameters are locals 0..N, then ANF locals increase monotonically within that function.
  • Surface function, parameter, and local spelling is absent from Core semantic encoding.
  • No inlining, constant folding, dead-function elimination, or call-graph reordering occurs in T2B.
  • Sufficient elaboration budget values cannot change the artifact or semantic hash.

The locked vector for one annotated identity(F64) -> F64 function and one entry call is:

source_steps = 7
core_nodes   = 4
semantic_hash = 63b41e503505c86ce409c0c61ea57dfb1d2afe91d672e0061992fd4b8c2b5209

7. Budgets

Source and Core budgets are global across declarations, all function bodies, and the entry body. A function declaration, statement, and expression each consume a source step. Every Core let, if, tailcall, and return consumes a Core node.

Exhaustion returns a typed elaboration error before any artifact is exposed.

8. Admission path

Surface AST + entry manifest
-> prefix/signature validation
-> complete direct-function table
-> deterministic per-function ANF elaboration
-> entry elaboration
-> Core artifact sealing
-> independent Core verification
-> canonical Core interpreter

The bridge typechecker and runtime are differential oracles, not T2B admission authorities.

9. Evidence required

  • parser preservation of all scalar annotations;
  • direct, nested, forward, recursive, and mutually recursive call structure;
  • both ordinary Call and proper TailCall lowering;
  • left-to-right argument and branch/continuation behavior;
  • exact arity, parameter, and return-type negatives;
  • missing annotation, Any/Num, global capture, builtin/dynamic callee, early/empty/implicit return, misplaced/nested function, and budget negatives;
  • alpha-renaming, repeated-run, sufficient-budget, and fixed-vector hash stability;
  • bounded Surface bridge versus verified Core differential corpus;
  • full workspace, strict lint, format, governance, and documentation-link gates.

10. Non-claims

T2B is not closure conversion, a general function compiler, P1/P2, Projection Birth, Nauxogenesis, or dependency closure. It does not reduce the current Rust/Cargo/egg debt.