Core-2 Realizations and Evidence

Status: normative preview; native binding proposals, scalar map typing and named source constraints available; refinement admission unavailable

C2-REAL-001 — Declaration. A realization is a directed refinement edge between a named public contract and a component or physical model. The source form is fixed by the grammar:

public realization AddOnFabric
    refines arithmetic.Add
    with circuits.AddUnit
    profile clocked
    claims exact;

The elaborated circuit/model supplies target assumptions and observation bindings through named constraints. Hardware profiles are combinational, clocked, asynchronous and intrinsic; physical profiles are steady, transient, harmonic, eigenvalue and coupled. A mixed implementation names its externally observable profile and includes every nested region/analysis obligation in the evidence closure. A realization cannot use a hardware profile for a physical model or erase nested intrinsic obligations by choosing a clocked wrapper.

C2-REAL-002 — Contract relation. Refinement checks an explicit observation map from implementation traces to contract traces, including inputs, outputs, errors, termination/progress, effects, cleanup, ordering and externally visible resource guarantees. Finite hardware state is not automatically a realization of unbounded software state. Hardware may stutter internally only when the contract’s observations permit it. Any domain may propose a realization; a missing peripheral/storage law or unsupported observation map rejects it. State atomicity, Flow durability and Optimize budgets remain obligations even when their implementation is spatial. Realization is not a callable crossing.

C2-REAL-003 — Claims. exact requires equivalence under the original contract’s declared observations and assumptions. It introduces no new timing or approximation latitude. bounded(ContractLimit) and statistical(ContractLimit) reference an existing named contract allowance: bounds specify norm, units, domain and tolerance; statistical allowances specify distribution/population, confidence, sample assumptions and failure limits. A realization cannot add an allowance to the contract it refines. An exact claim about a contract that already permits bounded numerical observations means satisfaction of that contract, not exact real arithmetic. Claim strength and evidence strength are explicit and separately checked.

C2-REAL-004 — Equal admission. Authored, compiler-generated and Optimize-generated realizations produce the same logical record and undergo the same checks. Generator identity belongs to lineage, not public contract identity. A proposal is untrusted until checked. Admission verifies the closed dependency set, claims, assumptions, target bindings and evidence; promotion atomically selects an admitted immutable realization. Failed admission leaves the previously selected realization unchanged. Quarantine and rollback preserve the rejected identity and reason. Physical reconfiguration is a separate capability-bearing action, not an automatic consequence of semantic promotion.

C2-REAL-005 — Native binding preparation. The bounded realization-bindings feature resolves one public source declaration against an actual checked Core-1 public message and an actual public hardware root. Generated proposals traverse the same grammar and binding checks. The owned zerglang.realization-binding/1 preparation record retains the original Core-1 contract ID unchanged, its separate baseline body ID, and the native hardware model’s identity with its original format. These are distinct pins, not new portable realization/body identities or interface/5 records.

Preparation admits the supported combinational, clocked/CDC and asynchronous native model profiles, retaining their existing bounds and rejection of unsupported nested disciplines. Intrinsic and physical bindings remain unsupported. The frozen Core-1 typed-message contract exports no named bounded/statistical allowance; this tranche therefore accepts only exact. The claim is a proposed obligation, not evidence that it holds. Preparation neither maps observations nor checks equivalence; its record states checked: bindings-only, observation_map: null, observation_admission: pending, and false refinement, promotion, authority and physical-evidence flags. Missing peripheral/storage laws, type relations and temporal obligations must still reject later refinement admission; a successful binding alone cannot admit any such behavior or select an implementation. The API, canonical field order, limits and examples are specified in docs/core2-realization-bindings.md in the repository.

C2-REAL-006 — Pure scalar observation maps. scalar-observation-maps checks an explicit native serial-settled-scalar-call/1 trace projection for a pure Algorithm leaf and a combinational model. Each original scalar parameter maps to exactly one root input, and the result maps to one root output. All external ports must be covered exactly once, with original parameter ordinals retained. Int8/16/32/64 use explicit two’s-complement Bits encodings; UInt8/16/32/64 use explicit unsigned encodings; Bool uses an explicit Bit encoding. Nominal wire kind, direction and exact width must match. There is no implicit X/Z conversion, truncation, sign reinterpretation or inferred mapping.

The checker revalidates actual software/hardware dependencies against the binding’s contract, baseline-body and native-model pins. Calls, owned cleanup, effect/capability-bearing behavior, other software domains, temporal profiles, inout ports and additional public observations need separate projection laws and are unsupported here. Parameter/local/result types must belong to the fixed-width subset. Absent checked local-type metadata requires C2-REAL-010, not bypassing this gate. Some minimal/older ZLM2 payloads omit local declarations; reconstruction does not change ZLM2 bytes. Payloads retaining checked local types are not excluded merely because they were loaded. The original contract is unchanged.

The owned zerglang.scalar-observation-map/1 record has checked: typed-map-only. It specifies serial nonoverlapping invocation and one settled combinational sample per invocation, under the original preconditions, with no added timing or approximation latitude. It does not prove that software or hardware obeys that relation. Universal equivalence, no-trap behavior under original preconditions, termination, cleanup preservation, ordering and resource guarantees remain explicit pending obligations. Refinement, promotion, authority and physical-evidence flags remain false. A later gate must discharge every obligation; a type-correct map alone cannot promote a realization. General temporal/peripheral/storage maps remain separate work. The API and canonical fields are specified in docs/core2-scalar-observations.md in the repository.

C2-REAL-007 — Named scalar source constraints. The scalar-observation-source feature lowers component-level proposed constraints with contextual constructors Realization.scalar_call_v1(qualified.contract), Realization.parameter_v1(relation, ordinal, input, encoding), and Realization.result_v1(relation, output, encoding). Encodings are explicit Realization.twos_complement, Realization.unsigned_binary, or Realization.boolean_bit. These are closed versioned forms, not runtime calls. Constraint names are unique in the local component namespace. Forward references to a local relation are allowed; each relation requires one explicit result. Only local ports with matching nominal kind, fixed width and direction bind. Assumptions, unknown constructors, residual expressions/calls, unknown names and duplicate role/port coverage fail closed. Static parameter ordinals retain the original software declaration order and are bounded to 0 through 31.

Elaboration retains owned proposal/source-lineage tables in zerglang.hardware-structure/6, with software_binding: pending and false refinement, promotion, authority and physical-evidence flags. These separate tables do not change existing circuit execution records or native model IDs. Graphs without them retain their existing structural format. The graph does not by itself resolve a software module or admit a trace projection. Selecting a named root-owned relation requires its exact original software symbol to match the actual binding and delegates the rows to C2-REAL-006’s checker, with the same dependency pins, coverage checks and pending proof obligations. Explicit and source-authored rows produce the same canonical map; display names, source order and provenance remain outside that map. At most 32 proposed relations and 1056 mapping rows may occur in the expanded closure; allocations and scans consume existing elaboration budgets. Full realization compilation, portable identities and proof/promotion remain separately gated. The source API, structural field order and examples are in docs/core2-scalar-observations.md in the repository.

C2-REAL-008 — Native canonical proposal assembly. realization-proposals joins an actual checked binding and typed observation map into one owned zerglang.realization-proposal/1 record. Source and generated inputs use the same gate. Assembly rechecks actual software/hardware dependencies and compares the supplied map against the freshly checked canonical map, including original dependency pins, symbol, rows and pending obligations. A stale body/model map cannot be attached to a fresh binding based only on compatible port types. The original public contract ID remains unchanged; baseline-body and native model pins retain separate meanings. Source/generator provenance remains in lineage, outside the canonical proposal.

This tranche admits precisely the pure scalar/combinational C2-REAL-006 projection. Unsupported temporal, effect, ownership and domain laws reject, rather than erasing errors, cleanup, atomicity, durability, budgets or timing. The record retains an exact proposed claim with no invented allowance and all pending map obligations. checked: typed-proposal-only and false refinement/promotion/authority/physical-evidence flags cannot be interpreted as admission. Portable IDs, general lowering, full source compilation and evidence promotion remain separate gates. The owned API and fixed native JSON order are specified in docs/core2-realization-proposals.md in the repository.

C2-EVID-001 — Evidence record. Evidence binds claim identity, subject identities, checker/tool identities, input/fixture identities, assumptions, observation maps, budgets, results, applicability and provenance. Check outcomes are pass, fail, unsupported or inconclusive. Only pass satisfies an applicable obligation. Cancellation, missing reports, stale subject digests and truncated measurements never become pass. A subject cannot include its evidence digest in its own identity preimage: evidence references subjects, and promotion records reference both, avoiding cyclic identities.

C2-EVID-002 — Profile obligations. The gate requires all applicable rows, including obligations inherited through the realization dependency closure.

Subject	Required evidence
portable digital	equivalence of admitted functional observations; sequential temporal relation for stateful designs; target constraints and independent materialization checks
asynchronous	functional relation plus protocol (if used), hazard, progress, delay/fork assumptions and timing evidence
intrinsic	exact measured devices, target/route/placement identity, instrumentation/calibration, environment envelope, repeatability and held-out population evidence when generalized
physical	typed observations, applicable residual/conservation/stability checks, error estimator or validated bounds, convergence study and independent reference comparison
mixed	each constituent’s obligations plus bridge/coupling error and event-order evidence

Formal tools must state the proof model and assumptions; a bounded proof claims only its bound unless induction or another argument closes it. Tests may supplement a proof or support a permitted empirical claim; they cannot convert a sampled claim into unrestricted universal equivalence. Solver output alone is not proof of the physical model’s fidelity to a device.

C2-EVID-003 — Invalidation. Changes to observations, implementation, toolchain, target, placement/routing, mesh, solver plan, calibration or validity envelope invalidate the evidence that depends on them. Reuse requires an explicit checked equivalence or transport argument. Environmental drift ends admission when it leaves the validated envelope; the runtime records that state and follows the contract’s stop/fallback policy. No automatic fallback may violate the original contract or issue unauthorized device actions.

For C2-ID-004 scalar proposals, the exact baseline software body and native execution/preparation model are separate evidence subjects. Equality of the portable logical realization identity never overrides a changed baseline or model pin. Rebinding can preserve the logical edge but not a stale proof result.

C2-EVID-004 — Bounded scalar reference evaluation. scalar-evaluation evaluates a C2-REAL-008/C2-ID-004 pure scalar/combinational proposal against the original checked software and native reference simulator. It is a functional-observation check, not an independently materialized target proof, complete refinement admission, or a promoted realization. Both dependencies are freshly checked against the original contract, baseline-body and native model pins before any execution. An unchanged logical edge never authorizes a new baseline. Stale dependencies reject with ZL-C2-EVIDENCE-0001 and produce no report or hardware operation.

The first profile, finite-scalar-reference/1, requires at most twelve total parameter bits and no original preconditions or postconditions. Other valid scalar proposals return unsupported, never an assumed condition or truncated input domain. Existing scalar type/map and combinational admission bounds remain mandatory. Software result widths remain the original fixed-width type, including 64-bit results and Bool. Calls, capabilities, cleanup and other domain/temporal laws remain outside the scalar map. A zero-parameter message has one input tuple, not zero cases.

Enumeration is parameter-ordinal-lsb/1: ascending unsigned concatenated bit patterns with parameter zero occupying the least significant bits, followed by successive original parameter ordinals. Each parameter is decoded using its checked explicit encoding; signed values are sign-extended for the original fixed-width software interpreter. Every hardware input is supplied simultaneously for each sample. The first sample has logical timestamp zero; subsequent samples increment by one. These are serial settled samples, not physical clock or frequency claims. The unchanged bounded software interpreter is the reference; neither source rewriting nor a duplicated arithmetic oracle defines software behavior.

Limits are max_cases in 0…4096 and max_software_steps in 0…1048576, defaulting to 256 and 1048576. The software-step budget is total across all cases, never reset between invocations. Zero budgets are zero, not unlimited. Existing simulation model/sample/trace/work bounds apply independently. Unsupported input width precedes unsupported contract conditions; both precede zero-budget handling, then live simulation admission. Unsupported or zero-budget reports perform no simulation or capability consumption.

Every open and sample uses fresh Simulator admission for the exact native model and explicit hardware effects. A report, effect, model ID or old admission does not substitute for a live grant. At each attempted case, obtain a settled hardware result first, then run the bounded software interpreter. No cached result from a failed sample is compared. Matched cases count only completed, equal, non-faulting pairs. Grant-counter differences report admitted operation, work and byte charges for this evaluation, including admitted attempts whose later allocation fails. No charges are refunded; callers must synchronize handles so unrelated consumption cannot occur during the call. Counter reads observe liveness but do not create or cache authority.

Outcomes are distinct:

Outcome	Meaning in this profile
pass	Every tuple in the complete supported finite domain was compared successfully, without a software fault
fail	The first output mismatch or software arithmetic fault violates this proposed no-trap scalar relation; retain that input tuple and known results
unsupported	The valid proposal has more than twelve input bits or original pre/postconditions needing another proof-domain law
inconclusive	Case/total-software-step budget, simulation/resource/authority unavailability or incomplete evaluation prevented a verdict

Infrastructure, interpreter resource/internal/input failures and hardware-simulation failures are conservatively inconclusive, not software counterexamples and never pass. Only the original interpreter’s integer arithmetic fault is a software-fault counterexample within this admitted no-precondition/no-postcondition scalar profile; its existing diagnostic code ZL-FAULT-0001 alone does not distinguish arithmetic faults from invalid interpreter arguments. Unknown interpreter failures remain inconclusive. This does not invent an error projection for a broader contract. Reasons have fixed order complete, output-mismatch, software-fault, input-width, contract-assumptions, case-budget, software-step-budget, simulation-unavailable, software-unavailable. The C view uses zero-based enum positions for these reasons and for pass/fail/unsupported/ inconclusive. Diagnostics from failed runtime operations are retained as owned codes; an inconclusive budget uses ZL-C2-CONVERGENCE-0001. A successfully constructed non-pass report is data, not an API failure. Invalid API arguments or out-of-range limits reject with ZL-OPTIONS-0001 and no partial report.

The immutable native report zerglang.scalar-evaluation/1 retains exact typed subject/context identities, enumeration, all budgets, outcome/reason, attempted and matched counts, software steps, consumed simulation resources, and the last attempted tuple with separately valid software/hardware result bits. Only fail sets counterexample true. No-attempt reports have a null last_case; unsupported input width has null total_cases (zero in the C view), not an empty input set. Last-case results are cleared before each attempt. Counts and diagnostics survive destruction of all input owners. Canonical JSON ordering and API details are in docs/core2-scalar-evaluation.md in the repository; the report is bounded at 65535 bytes plus its owned terminator.

Checker semantics is zerglang.scalar-reference-checker/1. Checker provenance is explicitly not-attested and independent_materialization is false. Pending obligations remain full-refinement, independent-materialization, target-constraints, checker-provenance and promotion. Refinement_verified, promotion_admitted, authority and physical_evidence remain false, even on pass. There is no report importer, portable evidence identity, trust shortcut, accepted-realization pointer update or fabric configuration in this tranche. Exact checker/toolchain attestation, temporal/async/intrinsic/physics gates and atomic promotion/invalidation remain separate mandatory work. Default legacy formats and stable Core-2 activation do not change.

C2-EVID-005 — Checked scalar reference-evidence identity. This clause supersedes only C2-EVID-004’s exclusion of a portable evidence identity for the bounded scalar report. C2-EVID-004’s evaluation laws, all other exclusions and all pending admission obligations remain unchanged. An identity of reference check data is not admitted evidence, authenticated checker provenance or a passing refinement result.

The allocated subject format is scalar-reference-evidence/1, in the C2-ID-002 evidence domain (tag 7), with framing version 1. Its payload is the exact compact ASCII zerglang.scalar-evaluation/1 report, without its owned C terminator. The top-level canonical order is schema, edition, preview, profile, checker, subject, trace_law, enumeration, limits, model_limits, outcome, reason, input_bits, total_cases, attempted_cases, matched_cases, software_steps, simulation_consumed, counterexample, last_case, diagnostic, pending_obligations, refinement_verified, promotion_admitted, authority, physical_evidence. Nested key order, encodings and field meanings are delegated to docs/core2-scalar-evaluation.md, section “Canonical report”, in the repository. The full report, not a selected subset or supplied digest, is the payload. The maximum payload is 65535 bytes; the 26-byte format label and 40-byte envelope header give a maximum complete preimage of 65601 bytes.

Construction must take an actual immutable native report and an independently chosen current checked C2-ID-004 realization context. It must compare complete typed realization, component-contract and component-body identities, and the original software-contract, baseline-body and native-model pins. The original pins retain their own formats; they are not relabeled as portable Core-2 identities. A stale baseline or model rejects with ZL-C2-EVIDENCE-0001 even if the logical realization identity is unchanged. No caller-supplied JSON, bare digest or unchecked frame can construct this checked context.

The semantic closure includes those subjects and pins, checker semantics and unattested provenance, observation law, enumeration, every evaluation/model limit, actual attempted/matched coverage, software and simulation charges, outcome/reason, last attempt and counterexample information, diagnostics, pending obligations and every admission flag. Changing a bound changes this identity even when the outcome stays pass. Source trivia preserving this closure does not change it. Appending this identity to another artifact does not change that artifact’s body or realization identity.

The context owns the exact preimage and remains valid after its input owners are destroyed. Verification must compare the complete preimage length and bytes with the independently selected checked context; rehashing a changed report does not admit it. Construction is pure and neither evaluates again nor consumes or creates a Simulator grant. All four outcomes can have data identities. report_checked and subject_context_checked are true, while evidence_admitted, checker_authenticated, authority and physical_evidence remain false for every outcome. The report’s false refinement/promotion flags and five pending obligations are retained unchanged. The API contract and reference vector are delegated to docs/core2-scalar-evidence.md in the repository. General evidence admission, attestation, target validation and realization promotion remain outside this allocation.

C2-REAL-009 — Bounded generated scalar datapath proposals. scalar-datapath-proposals accepts an actual checked Core-1 pure Algorithm message and proposes a combinational component and exact realization, retaining the original contract and baseline-body identities. This is candidate generation, not invocation, proof, promotion or permission to configure fabric. Compiled and interpreted software modalities use the same gate. The original checked semantic tree and IR must agree on each translated opcode, scalar type and immediate.

The first generator, zerglang.scalar-bitwise-lowering/1, admits Bool and Int8/16/32/64 or UInt8/16/32/64 parameters, locals and results, with no effects, capabilities, ownership cleanup, contract conditions, verification prefixes or non-Algorithm domain nodes. Checked local types must be available directly or through C2-REAL-010. No source rewriting invents those types. The closed instruction subset is exact typed scalar constants, initialized local loads/stores, fixed-width bitwise AND/OR/XOR, Boolean NOT, and one terminal return. Local stores preserve sequential value versions. Legacy annotations on loads/stores/Boolean NOT/return are accepted only when tracked exact types already establish their interpretation. Constants and bitwise binary operations require explicit fixed scalar annotations. Unknown operations, branches, calls, loops, arithmetic, casts or potentially faulting behavior reject, even when a later instruction would discard the value. No dead-code elimination erases effects or faults. Compute, floating-point, tensors, dynamic sizes and further numeric laws are outside this profile; they remain mandatory future realization work.

Bounds are 32 parameters, 128 local slots, 128 stack entries, 1024 instructions, and 65535 bytes plus terminator for each generated source/lineage output. The existing checked reflection preparation has a 1 MiB accepted-output bound. The generated namespace is caller-selected, valid qualified source identifiers, at most 255 bytes with segments at most 127 bytes, and differs from the original software module. Original qualified contract names must fit 1023 bytes. Names and types may not be injected as arbitrary source text. Further source, elaboration, model, mapping and netlist limits apply independently. Invalid arguments/names use ZL-OPTIONS-0001; unsupported subsets or exhausted generation bounds use ZL-C2-UNSUPPORTED-0001. Dependency gates retain their own diagnostics. No failure publishes a partially usable bundle.

Generated declarations are Datapath and Candidate. Ordered input ports p0…pN and result y retain explicit original scalar encodings under C2-REAL-007. Constants and operations produce sequentially named n0…nN nets with explicit Bit/Bits widths. Emitted source is parsed, elaborated and bound using the same public source, scalar-map and canonical-record gates as authored source, with the caller’s original model-preparation limits. The bundle owns the resulting checked hardware, proposal and C2-HW-005 netlist. The normal C2-ID-004 realization and C2-ID-005 implementation IDs remain distinct from the original software contract/body pins. Source formatting/offsets do not redefine those identities.

An owned zerglang.scalar-datapath-lineage/1 projection retains the generator version, original contract/body pins, complete realization and implementation identity tuples, preparation limits, instruction count, and ordered mappings from materialized source instructions to generated nets. Source offsets are unattested metadata, not authenticated source content; absent/empty spans have null byte offsets, not a fabricated source location. Provenance is explicitly not-attested. Refinement_verified, promotion_admitted, authority and physical_evidence remain false in views and lineage. The canonical field order and public ownership API are specified in docs/core2-scalar-datapath.md in the repository. No separate portable lineage/evidence ID or importer is allocated.

Native evaluation still requires the original software and a fresh scoped Simulator capability under C2-EVID-004. A generated candidate covering a larger domain does not enlarge that evaluator’s finite-domain bound or prove the candidate. Independent RTL test execution is verification of this generator, not target synthesis, attested materialization or accepted-realization promotion. Snapshot/ZDE integration is paired with ZER5-110/111; expose ownership, limits, separate identities, outstanding obligations and unattested lineage without a UI-only state store. Stable activation and old artifact/projection formats remain unchanged.

C2-REAL-010 — Read-only scalar-local typing. The hardware-preview scalar-local-reconstruction feature inspects an actual checked Core-1 pure Algorithm message, compiled or interpreted, retaining its original contract and baseline-body pins. It neither alters the checked module nor creates a new semantic identity. Bounds are 32 parameters, 128 local slots and stack entries, and 1024 instructions. Parameter/local/result types are Bool or signed/unsigned fixed integers 8/16/32/64. Ownership, cleanup drops, capability/effect-bearing behavior and other domain nodes are unsupported. Existing checked local tables must contain exact scalar declarations consistent with the parameter types; their acceptance is independent of whether the module was source-compiled or loaded. This declaration path is a typing report, not instruction translation.

Only absent local tables trigger reconstruction from exact checked parameter types and initialized, straight-line typed dataflow. Every instruction must agree with its checked semantic node on opcode, immediate and scalar kind. Loads require initialized slots; stores establish an unknown slot or preserve its exact existing type, including reassignment. Unused initialized locals are retained. Missing/uninitialized/ambiguous slots and conflicting annotations reject. Explicit constants establish their checked scalar kind. Unary negation, arithmetic, comparison and bitwise operations require exact operand annotations; comparison yields Bool. Boolean NOT and assertions preserve/check their operand types. Legacy annotations are allowed only on loads, stores, Boolean NOT, Boolean assertions and return where tracked exact types determine the result. No generic numeric, ownership, alias, aggregate or control-flow inference occurs. Branch joins, loops, calls and unknown operations reject reconstruction. A single terminal return must have exactly one value of the declared result type and every local must have an established exact type. Source syntax still requires local initialization; this feature does not relax the source checker.

Typing never executes, folds, discards or proves instructions. Arithmetic may still trap. C2-REAL-006 and C2-REAL-009 retain their independent instruction, dependency and fault-preservation gates; a successful typing report cannot authorize generation or evaluation of an unsupported body. Original bindings, maps, proposal and implementation identities remain unchanged by successful source/loaded reconstruction. No serialized local table is added to ZLM1/ZLM2.

The owned zerglang.scalar-local-types/1 JSON uses field order schema, checked (local-types-only), contract, baseline_body, reconstructed, locals, refinement_verified, promotion_admitted, authority, physical_evidence. Each local is ordered by slot with fields slot, type, parameter. Pins are lowercase hex; all four authority/evidence flags are false. The reconstructed flag describes metadata provenance, not trust strength. JSON is at most 16383 bytes plus a terminator. Views/JSON remain valid after module destruction and JSON after report destruction. Invalid arguments use ZL-OPTIONS-0001; unsupported or inconsistent typing uses ZL-C2-UNSUPPORTED-0001; inherited checked-module and preview errors retain their diagnostics. Failure publishes no partial report. This is an inspectable derived report, not an importable proof, portable evidence identity, executable artifact or live capability. The public API and paired snapshot/ZDE ownership projection are described in docs/core2-scalar-locals.md.

C2-EVID-006 — Scalar evidence framing arithmetic correction. This clause supersedes only C2-EVID-005’s numeric label length and maximum preimage length. The unchanged scalar-reference-evidence/1 spelling is a 27-byte format label. The 40-byte header therefore gives payload offset 67 and a maximum complete preimage of 65602 bytes for the unchanged 65535-byte payload limit. No format, domain, canonical key order, semantic closure or evidence authority changes.