Future positive/negative expectations and logical identity vectors.
Core-2 Conformance Examples and Identity Vectors
Status: specification expectations; these examples do not execute in Stage0
The snippets use the Core-2 grammar. Examples with external names specify their fixture contracts in prose; future executable cases must include those complete source/model closures. They are not executable ZL512 tasks or compiler tests. Diagnostic expectations apply only after the implementation admits the named preview/features; otherwise C2-DIAG-002 requires unsupported admission.
Finite hierarchy and logic
module examples.inverter;
public compiled hardware component Invert(in a: Bit, out y: Bit) {
region logic: combinational {
connect y = ~a;
}
}
public compiled hardware component Buffer(in a: Bit, out y: Bit) {
net middle: Bit;
instance first: Invert(a = a, y = middle);
instance second: Invert(a = middle, y = y);
}
For a=0 the output is 0; for a=1 it is 1, independently of instance declaration
order. Both instances have the same discipline; no inter-discipline bridge is
needed. Replacing second with an instance of Buffer creates recursive
elaboration and requires ZL-C2-ELAB-0001. Adding a second assignment to
middle requires ZL-C2-DRIVER-0001. Width zero requires
ZL-C2-LOGIC-0001. An implicit connection from Logic to Bit also requires that
code; explicit conversion of [1,X,0] returns the first unknown bit index 1.
Four-state vectors: 0 AND X = 0, 1 OR Z = 1, X XOR 0 = X;
wired(Z,1,Z) = 1, wired(0,1) = X, and wired(Z,Z) = Z.
An unknown mux selector with branches [1,0,Z] and [1,1,Z] produces
[1,X,Z]. Reordering wired drivers preserves results; reordering mux branches
does not generally preserve the function when the selector is known.
Simultaneous clocked state
module examples.pipeline;
public compiled hardware component Pipeline(in tick: Clock, in rst: Reset,
in d: Bit, out y: Bit) {
clock c = rising(tick) reset rst active high mode synchronous;
constraint input_timing = Contracts.synchronous_input(d, c);
region registers: clocked {
register first: Bit on c = Bit.zero;
register second: Bit on c = Bit.zero;
process sample on c {
next first = d;
next second = first;
}
connect y = second;
}
}
Fixture d is synchronous to c and stable in its sampling window. Starting at
(first,second)=(0,0), two edges with d=1 produce (1,0), then (1,1).
Reversing the two next statements preserves both traces. Reset asserted at
an active edge produces (0,0). A backend with no supported initialization/reset
implementation rejects the target rather than changing initial behavior.
This negative fragment reads one clock’s register from another without a bridge:
public compiled hardware component BadCDC(in a: Clock, in b: Clock, out y: Bit) {
clock ca = rising(a);
clock cb = rising(b);
region left: clocked {
register held: Bit on ca = Bit.zero;
process toggle on ca { next held = ~held; }
}
region right: clocked {
register sampled: Bit on cb = Bit.zero;
process sample on cb { next sampled = left.held; }
connect y = sampled;
}
}
Expected: ZL-C2-CDC-0001, including when a and b happen to edge together.
The positive fixture inserts a bridge declaration in place of the direct read:
bridge crossing: Bridges.SyncBit(source = left.held, destination = cb);
Bridges.SyncBit is a fixture-defined component with an output sampled, a
declared two-register synchronizer, a single-bit stable-source assumption,
destination clock cb and latency/failure envelope accepted by the contract.
next sampled = crossing.sampled; then has a valid structural CDC boundary.
Changing the source to a changing multibit word invalidates that bridge.
Clockless feedback and intrinsic binding
public compiled hardware component Oscillator(out y: Bit) {
region ring: asynchronous {
state phase: Bit = Bit.zero;
assume evolution = Laws.transport_toggle(phase, SI.ns(1));
process toggle when true { drive phase = ~phase; }
connect y = phase;
}
}
The fixture law drives the initial complement at t=0, schedules each drive one
nanosecond later, and reevaluates on phase changes. Expected post-event outputs
at t=0,1,2,3 ns are 0,1,0,1. It is observed over a finite horizon, not required
to settle forever. Removing the delay/feedback law requires
ZL-C2-ASYNC-0001; zero-delay microstep exhaustion requires
ZL-C2-CONVERGENCE-0001. Changing transport to inertial scheduling must preserve
that distinction in the body identity and pulse-filtering traces.
An intrinsic declaration uses the same component structure with
region substrate: intrinsic and named constraints:
constraint target = Fixtures.target_part;
constraint layout = Fixtures.placed_and_routed;
constraint envelope = Fixtures.measured_envelope;
public realization ToneDetector
refines contracts.ToneDiscrimination
with circuits.MeasuredDetector
profile intrinsic
claims statistical(contracts.ToneDiscrimination.population_limit);
The three constraint lines are component-body fragments. Fixtures bind part,
package, speed grade, route/placement digests, individual device IDs A/B,
temperature/supply ranges, calibrated measurement procedures and held-out
population rules. Promotion with passing matching evidence is admitted.
Applying A’s evidence to unmeasured C or to a changed route requires
ZL-C2-INTRINSIC-0001 or ZL-C2-EVIDENCE-0001 at the corresponding gate.
Adding the statistical allowance only in the realization requires
ZL-C2-REALIZATION-0001.
Strong and weak physical models
public physical model HeatedRod {
mesh rod = Fixtures.unit_rod;
parameter k: Quantity<ThermalConductivity> = Fixtures.conductivity;
field temperature: Scalar<Temperature> on rod.nodes;
equation balance strong Math.div(k * Math.grad(temperature)) == Fixtures.zero_source;
condition boundary left on rod.left = SI.kelvin(300);
condition boundary right on rod.right = SI.kelvin(400);
analysis equilibrium: steady {
constraint unknowns = Fields.single(temperature);
constraint conditions = Conditions.all();
constraint acceptance = Fixtures.rod_tolerance;
observe midpoint = Fields.sample(temperature, Fixtures.midpoint);
}
}
The fixture is a one-meter oriented segment mesh with positive constant k,
no source, pointwise prescribed endpoint temperatures, a scalar H1 trial
space and linear interpolation. The expected steady solution is
T(x)=300 K + (100 K/m)x; midpoint=350 K and left/right oriented fluxes cancel.
Acceptance is absolute midpoint error <=0.01 K plus the declared residual and
flux bounds. A duplicate node reference or reversed cell orientation requires
ZL-C2-MESH-0001. Replacing a boundary temperature with SI.volt(300) requires
ZL-C2-DIMENSION-0001. Removing both endpoint conditions without a nullspace
contract prevents solver admission with ZL-C2-MODEL-0001.
An alternative weak equation for that model is:
equation balance weak for v in Fixtures.zero_boundary_H1
Math.integral(rod, Math.dot(k * Math.grad(temperature), Math.grad(v))) == Fixtures.zero_work;
The fixture test space contains dimensionless scalar functions vanishing at
both endpoints; zero_work has the integral’s resulting dimension. This
equation replaces the strong equation, rather than adding a second constraint.
The same linear temperature profile is expected. An incorrectly dimensioned
right-hand side fails dimension checking. Strong/weak equivalence requires
the stated regularity, boundary and integration-by-parts argument.
Coupled models and foundational bridges
public physical model ElectroThermal {
mesh device = Fixtures.device_mesh;
couple transport: Couplings.ElectroThermal(
electrical = Fixtures.conduction,
thermal = Fixtures.heat,
projection = Fixtures.conservative_projection);
bridge sensor: Bridges.SampleAndQuantize(
source = transport.temperature,
sampling = Fixtures.aperture,
quantization = Fixtures.quantization);
analysis run: coupled {
constraint members = transport.analyses;
constraint schedule = Fixtures.coupling_schedule;
constraint acceptance = Fixtures.coupled_tolerance;
observe code = sensor.code;
}
}
Fixtures define electrical Joule heating as the thermal source, temperature-
dependent conductivity, explicit field projections and units, coupled residual
norms, finite time horizon, iteration limit and sample/quantization laws.
For a constant source exactly at a code-bin center and zero declared noise,
the expected code is that bin’s code. A mismatched energy-flux orientation
fails conservation; omitted sample aperture/rounding fails with
ZL-C2-BRIDGE-0001; iteration-limit exhaustion returns
ZL-C2-CONVERGENCE-0001. ADC wrapper expansion must expose the same sampling,
quantization and uncertainty contract as its foundational composition.
Protocol, promotion and edition cases
| Case | Positive expectation | Negative counterpart |
|---|---|---|
| edition/profile | explicit hardware-preview admits supported hardware; physics-preview admits supported models | bare Core-2: ZL-C2-EDITION-0001; model in hardware-preview: ZL-C2-PREVIEW-0001 |
| declaration | compiled hardware component and non-callable physical model keep distinct kinds | physics message: ZL-C2-SYNTAX-0001 |
| capability/effects | matching live fabric authority and declared effects admit exchange | expired/other-target authority: ZL-C2-CAPABILITY-0001; missing effect: ZL-C2-BOUNDARY-0001 |
| software lowering | bounded memory and matching storage/peripheral laws preserve State/Flow observations | lost commit atomicity or replay durability: ZL-C2-REALIZATION-0001 |
| publication | specified Core-2 is visible while implementation remains unavailable | claiming executable preview without feature evidence fails C2-GATE-002 |
| adapter | matching request ID, confined digested outputs, all requested reports returned | wrong ID/missing report: ZL-C2-ADAPTER-0001 |
| fabric recovery | replay consumes recorded receipt; deduplicated retry returns prior result | uncertain physical effect without receipt: ZL-C2-INDETERMINATE-0001 |
| solver plan | complete dimensional model and plan with passing applicable error evidence | residual-only evidence when error bound is required: ZL-C2-SOLVER-0001 |
| generated plan | authored and generated equivalent records pass the same admission | untrusted generated native executable or exhausted recursion budget: ZL-C2-SOLVER-0001 |
| promotion | matching admitted realization becomes selected atomically | stale evidence leaves prior selection unchanged: ZL-C2-EVIDENCE-0001 |
| artifact | canonical typed graph closes all references | dangling reference, duplicate key or altered digest: ZL-C2-ARTIFACT-0001 |
| unsupported | declared unsupported target/report remains visible | unsupported report cannot satisfy required evidence: ZL-C2-EVIDENCE-0001 |
| corpus | imported 256 + hardware 128 + physics 128; profile-scoped maturity | scaffold counted as verified, omitted unsupported task or mutated historical identity fails C2-BENCH-004/005 |
| stable gate | all inherited/independent/device/solver/mutation evidence supplied | fake independent wrapper or missing ZDE projection fails C2-GATE-001/004 |
Logical identity vectors
These vectors specify equality/inequality relationships, not invented binary hashes. Each baseline and change must be made into a golden typed-graph pair when its encoding tranche is implemented. Unmentioned independent identities stay unchanged; dependency-derived identities change with their inputs.
| Baseline and one change | Required identity relation |
|---|---|
| Buffer source; whitespace/comment-only rewrite | contract/body/realization unchanged; source lineage changes |
| Pipeline; reverse independent next statements after canonicalization | contract unchanged; normalized simultaneous-update body unchanged |
| Pipeline; make second read a newly updated first | rejected semantics, never an equivalent implementation |
| Fixed public contract; replace clocked implementation with admitted async implementation | contract unchanged; body/realization/implementation change |
| Public clocked contract; change admitted latency interval | contract changes |
| Resolved net; permute unordered drivers | body unchanged |
| Mesh; reverse an element connectivity orientation | invalid mesh rejected; never canonicalized back silently |
| Physical contract; change declared node coordinate | contract/model body change |
| Same physical model; refine only solver mesh with projection evidence | model contract unchanged; plan/implementation/evidence change |
| Same model; change a constitutive equation or boundary temperature | model contract/body change |
| Same exact claim; add a new measured report | subject/contract unchanged; evidence/lineage change |
| Portable design; change target part or place/route result | portable contract unchanged; target implementation/artifact/evidence change |
| Intrinsic public contract; widen temperature envelope | intrinsic contract/realization and required evidence change |
| Same SolverPlan; choose a different preconditioner/tolerance | model contract unchanged; SolverPlan/implementation change |
| Source-authored versus generated identical checked realization | contract/body/realization unchanged; generator lineage changes |
| Same reported hash bytes in two identity kinds | identities unequal because domains differ |
Clause coverage
| Clause families | Positive/negative case groups |
|---|---|
| C2-DOM, C2-PREVIEW, C2-SRC | edition/profile, declaration, publication, hierarchy |
| C2-HW, C2-LOGIC | hierarchy/logic, CDC, clockless feedback |
| C2-CLOCK, C2-ASYNC, C2-INTRINSIC | pipeline, BadCDC, oscillator, ToneDetector |
| C2-PHYS, C2-LIB, C2-BRIDGE | HeatedRod, weak form, ElectroThermal, sampler |
| C2-REAL, C2-EVID | lowering, promotion, intrinsic binding and identity vectors |
| C2-EFF, C2-CAP, C2-BOUND | capability/effects, lowering and fabric recovery |
| C2-ART, C2-ID, C2-IFACE, C2-DIAG | artifact, unsupported, publication and identity vectors |
| C2-ADAPTER, C2-SOLVER | protocol, solver plan, generated plan and recovery |
| C2-BENCH, C2-GATE | corpus, publication and stable-gate cases |