GitHub

Surface → Core-N0 T2 Contract

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

1. Claim

For a T2A-admitted Surface kernel K, typed input manifest M, exact dynamic input vector x, and sufficient Core evaluation budget:

normalize(eval_Surface(K, bind(M, x)).result)
=
normalize(eval_Core(verify(elaborate_T2A(K, M)), x).result)

The relation covers successful returned scalar values. Elaboration rejection, input binding rejection, and Core evaluation-budget exhaustion are distinct typed failure domains and are not equated with bridge-interpreter errors. Runtime log events created by the bridge’s assignment implementation are not Core effects and are outside this pure-kernel relation.

2. Request

An elaboration request contains:

statements
ordered inputs: [(name, Bool | I64 | F64)...]
result variable name
max_source_steps
max_core_nodes

Input names must be non-empty and unique. The result must exist on every syntactic path, including a branch whose condition is a literal, and have one scalar type.

Binding requires exactly the manifest arity, order, and scalar tag. I64 is never coerced to F64, nor vice versa.

3. Admitted Surface

Statements:

name = expression
if bool_expression
    statements
else
    statements
end

Expressions:

Bool literal
numeric literal
input or local variable
F64 expression + F64 expression
F64 expression - F64 expression

Assignments create new immutable Core locals. Reassignment is admitted only when the scalar type is unchanged on that path.

The parser represents a negative source literal as a unary expression, so it is rejected in T2A even though a negative Number(f64) constructed directly in the AST can be classified by the numeric boundary rule.

4. Explicit exclusions

T2A rejects:

  • Rite, Unsafe, function definitions, calls, and closures;
  • expression statements, loops, Each, While, and Return;
  • actions, imports, IO, FFI, and unsafe memory;
  • text, bytes, lists, maps, fields, and indexing;
  • integer or mixed numeric arithmetic;
  • multiplication, division, modulo, bitwise operations, and shifts;
  • equality, relational comparison, boolean operators, and unary operators;
  • annotations that T2A does not understand;
  • unbound names, type-changing reassignment, or path-dependent result types.

Rejection is a typed elaboration error with a structural path and a source span when the Surface AST provides one. It never invokes the AST interpreter, VM, trace JIT, or an Any fallback.

5. Scalar observation

Differential evidence compares this normalized domain:

Bool      → exact boolean
I64       → exact signed 64-bit value
F64       → exact IEEE-754 bits
all NaNs  → 0x7ff8000000000000

Non-NaN F64 bits are preserved, including the sign of zero. T2A currently compares bridge and Core execution in the same process and host floating-point environment. It does not yet claim cross-target reproducibility under altered rounding modes, FTZ, or DAZ behavior.

6. Canonical form and determinism

  • Input order fixes parameter IDs.
  • Source traversal is left-to-right.
  • Output contains exactly one pure P1V0 function with ID 0 and no region parameters.
  • Parameters receive locals 0..N in manifest order; all later local IDs increase monotonically across the whole artifact.
  • Every Surface assignment becomes a let with RValue::Use; every nested F64 operation becomes its own preceding ANF let.
  • There is no constant folding in T2A.
  • The then branch is fully elaborated before the else branch, using one global local-ID allocator and separate cloned environments.
  • The remaining continuation is duplicated into both branches.
  • Core sealing uses Semantic Encoding v1.
  • Sufficient budget values do not affect the emitted Core or semantic hash.

Surface variable spelling is not encoded after alpha-renaming into Core local IDs.

The locked vector for $result = $x + $y with ordered F64 inputs x, y is:

source_steps = 4
core_nodes   = 3
semantic_hash = 52ee627ea5c1685d00d88b6bcbc0947a4c44ff539ad6685349135f67b4d0b468

7. Budgets and safety caps

max_source_steps bounds visited statement/expression nodes, including visits caused by continuation duplication.

max_core_nodes bounds emitted let, if, and return terms.

T2A also enforces non-configurable safety caps:

inputs       ≤ 256
source_steps ≤ 256
core_nodes   ≤ 256

Zero or exhausted source and Core budgets have distinct error codes and fail before an artifact is returned. A request above a cap is rejected before lowering, and a partial artifact is never sealed or evaluated.

8. Admission path

Surface AST + typed manifest
→ T2A validation
→ deterministic ANF elaboration
→ Core artifact sealing
→ independent Core verifier
→ VerifiedArtifact
→ canonical Core interpreter

The elaborator cannot construct a successful report unless the independent Core verifier accepts the sealed artifact.

9. Evidence

T2A requires:

  • positive scalar/assignment/branch cases;
  • both dynamic branch directions;
  • validation of unsupported constructs in both syntactic branches, even when one condition is statically known;
  • repeated elaboration and fixed-vector hash stability;
  • numeric edge values admitted by the profile;
  • exact input arity/tag rejection without numeric coercion;
  • Surface bridge ↔ Core differential cases;
  • unbound, type mismatch, missing result on one branch, unsupported construct, and exact-minus-one/zero budget negatives;
  • a source-boundary test proving the Core semantic nucleus still imports no Surface AST, runtime, VM, or egg, including future Rust source files added under src/core.

10. Definition of done

T2A is complete when the implementation and evidence above pass the full workspace test, strict lint, formatting, governance, and documentation-link gates. Completion of T2A does not complete Roadmap Stage 1 or admit function elaboration.