Positive and negative future semantic expectations, schema and identity vectors.
Core-3 Conformance Cases
C3-CONFORM-001 — Evidence level of these fixtures
These are required future semantic outcomes, not executable results from the
current compiler. conformance-vectors.json separates logical shape fixtures
from canonical identity vectors. The shape fixtures intentionally use synthetic
external references; they establish record structure only, not resolvable
dependencies, checked proof, authenticity, admission, or execution. The identity
vectors include complete envelope/preimage/digest data and require no model.
accepted below means the named judgment succeeds with the stated checked
dependencies and authority supplied. It does not mean stable edition activation.
Each rejection names the decisive rule and diagnostic; an implementation that
does not support the judgment must report unsupported instead of pretending
to have performed it.
C3-CONFORM-002 — Proof core and composition
The Logic.identity and Logic.compose source fragments in
proof language are positive baselines. Check identity
against forall (P:Prop) -> forall (p:P) -> P; check composition against the
exact displayed dependent-product type, with no extra axioms.
| ID | Input or perturbation | Expected outcome |
|---|---|---|
| P01 | Identity and composition baselines; closed empty imported environment | Checked, empty axiom footprint |
| P02 | Ask identity’s proof to establish forall (P:Prop) (Q:Prop) -> forall (p:P) -> Q |
Rejected, ZL-C3-STATEMENT-0001 |
| P03 | Compose f:P->Q with g:R->S without a proof relating Q and R |
Rejected, ZL-C3-TYPE-0001 |
| P04 | Proposition P and a missing proof/hole presented as completed |
Rejected, ZL-C3-TYPE-0001; no hole-to-axiom fallback |
| P05 | Rename bound variables of identity while preserving de Bruijn structure | Same logical term/identity; source provenance may differ |
| P06 | Out-of-scope variable index 2 in identity’s two-binder body |
Rejected, ZL-C3-TYPE-0001 |
| P07 | define bad : Prop using () = Prop; |
Rejected, ZL-C3-TYPE-0001: Prop has type Type(0), not Prop |
| P08 | Claim Sort(0):Sort(0) or constrain u=succ(u) |
Rejected, ZL-C3-UNIVERSE-0001 |
| P09 | Treat a data type in Type(0) as a type in Type(1) without a lift | Rejected, ZL-C3-TYPE-0001; no cumulative coercion |
| P10 | Nat with zero/successor and its generated recursor; prove n+0=n by induction over checked addition |
Checked, empty footprint, including n=0 |
| P11 | Bad has constructor field forall (x:Bad) -> False |
Rejected, ZL-C3-INDUCTIVE-0001 |
| P12 | Direct/mutual global definitions call themselves to construct False | Rejected, ZL-C3-TERMINATION-0001 |
| P13 | Recursive surface definition cites a termination annotation but supplies no recursor/accessibility proof | Rejected, ZL-C3-TERMINATION-0001 |
| P14 | Distinct already-checked proofs of the same proposition used in conversion | Definitionally equal; this does not establish a missing proof |
| P15 | Prop existential witness projected into Nat | Rejected, ZL-C3-INDUCTIVE-0001 |
| P16 | False elimination, or Eq.refl transport, into Type under the generated singleton/empty recursor | Checked; no arbitrary data-bearing Prop elimination |
| P17 | Positive nested or mutually recursive inductive beyond the first profile | Unsupported, ZL-C3-UNSUPPORTED-0001, not assumed positive |
| P18 | Conversion budget zero before a necessary reduction | Inconclusive, ZL-C3-BUDGET-0001; not a disproof |
C3-CONFORM-003 — Assumptions and extraction
| ID | Input or perturbation | Expected outcome |
|---|---|---|
| A01 | Explicit classical-em theorem under policy admitting its exact profile | Checked with classical-em footprint |
| A02 | Same proof under constructive-only policy | Rejected, ZL-C3-AXIOM-0001 |
| A03 | Imported opaque theorem depends on axiom bad:False, while producer claims no axioms |
Rejected footprint claim, ZL-C3-AXIOM-0001; actual dependency stays visible |
| A04 | A well-typed theorem conditional on explicitly admitted custom bad:False |
Checked only under that disclosed inconsistent assumption; no consistency or unconditional truth claim |
| A05 | External solver returns pass without a checked certificate | Not proof evidence; reject a proof-required obligation with ZL-C3-EVIDENCE-0001 |
| A06 | Checked Nat identity construction and its identity theorem, extracting at zero and successor values | Algorithm behavior preserves values; explicit arbitrary-precision/resource contract |
| A07 | Bare Exists(Nat,pred) theorem, with or without classical reasoning |
Rejected for extraction, ZL-C3-EXTRACTION-0001 |
| A08 | Retained computational closure calls classical-choice | Rejected, ZL-C3-EXTRACTION-0001, naming the noncomputable constant |
| A09 | Actual Nat computation plus policy-admitted classical proof confined to erased fields | Extraction permitted; classical footprint remains on the contract |
| A10 | Extract Nat into UInt64 without range proof at 18446744073709551616 | Rejected, ZL-C3-EXTRACTION-0001; no wrap-to-zero |
| A11 | Host cannot allocate a retained Nat value | Declared runtime resource error, not contradiction of logical termination |
| A12 | Higher-order retained argument or unresolved dependent layout | Unsupported, ZL-C3-UNSUPPORTED-0001 |
C3-CONFORM-004 — Verification model boundaries
| ID | Subject and challenge | Expected outcome |
|---|---|---|
| V01 | Algorithm UInt64 increment at max value; proof uses unbounded integer addition | Reject model mismatch, ZL-C3-MODEL-0001 |
| V02 | Algorithm deliberately diverges; vacuous partial postcondition is proved | Partial claim only; cannot satisfy total obligation |
| V03 | Compute vector length zero and length one; correctly quantified index bounds | Bounds proof covers empty domain and index zero respectively |
| V04 | Compute access at index equal to length, or unchecked aliased parallel writes | Reject proof-required admission, ZL-C3-EVIDENCE-0001 |
| V05 | Reassociate strict floats using a theorem about real associativity | Reject model mismatch, ZL-C3-MODEL-0001 |
| V06 | State invariant holds initially and for every admitted commit; aborted transaction has outbox request | Invariant preserved; no outbox/model dispatch from abort |
| V07 | State proof omits conflict/abort transitions allowed by the selected isolation model | Reject incomplete model binding, ZL-C3-MODEL-0001 |
| V08 | Flow replay under recorded code epoch and activity results | Same declared observations without repeating activities |
| V09 | Flow finite trace presented as unbounded liveness without fairness proof | Reject insufficient evidence, ZL-C3-EVIDENCE-0001 |
| V10 | Optimize finite set [3,1,1], minimize value with stable order | Optimum 1 with the declared first-tie selection, under a complete finite certificate |
| V11 | Optimize best observed sample called a global optimum over an unsearched space | Reject insufficient evidence, ZL-C3-EVIDENCE-0001 |
| V12 | Hardware equivalence covers all Boolean inputs for an acyclic two-state model | Bounded complete Boolean claim only, not four-state/timing/device evidence |
| V13 | Same evidence reused for X/Z input, changed reset/CDC law, or physical timing | Reject model mismatch, ZL-C3-MODEL-0001 |
| V14 | Physics conservation theorem under exact stated equations/conditions | Checked model theorem; empirical fidelity remains a separate obligation |
| V15 | Replace mesh, boundary conditions, units, or norm while reusing old proof | Reject stale binding, ZL-C3-MODEL-0001 |
| V16 | Change implementation body but retain contract name and cached receipt | Reject stale dependent evidence, ZL-C3-EVIDENCE-0001 |
| V17 | Reuse unaffected standalone lemma after unrelated body/prose change | Lemma remains checked; interpretation/bridge admission still revalidated |
| V18 | Prove replacement challenge True instead of the pinned functional contract |
Reject, ZL-C3-STATEMENT-0001 |
C3-CONFORM-005 — Intent resolution and runtime
Use the sorting intent in Intent authority, with ordered and permutation requirements, an explicit policy, authenticated delegated approval, and an exact formal contract. Supply separately granted effects and finite budgets; no row assumes authority merely because the policy is stored.
| ID | Request or perturbation | Expected outcome |
|---|---|---|
| I01 | Generated checked sorting code; input [3,1,3]; both required proofs pass | Completed with [1,3,3], proof evidence and approval separately recorded |
| I02 | Typed plan calling an existing checked sorter under the same contract | Same output/contract, distinct plan implementation and execution receipts |
| I03 | Either product on [] | Completed with []; both requirements still satisfied |
| I04 | Candidate returns sorted [1,3] for [3,1,3], dropping a duplicate | Reject before admission if proof-required; failed postcheck if explicitly runtime-checked, never successful permutation evidence |
| I05 | Formalization omits permutation, maps an unknown requirement, or weakens it after approval | Rejected, ZL-C3-FORMALIZATION-0001 |
| I06 | No-requirement source declaration, malformed request record, or mistyped input | Rejected before provider call: ZL-C3-SYNTAX-0001, ZL-C3-ARTIFACT-0001, or inherited type diagnostic respectively |
| I07 | Authorized agent approves its proposal under a policy permitting both roles | Approval accepted without a mandatory human gate |
| I08 | Same principal under independent-approval policy; or unauthenticated/out-of-scope approver | Rejected, ZL-C3-APPROVAL-0001 |
| I09 | Ambiguous prose; policy authorizes a specific recorded assumption | Continue with new explicit formalization and approval, not an invisible interpretation change |
| I10 | Ambiguity has no authorized resolution, or approval is unavailable | Unresolved, ZL-C3-FORMALIZATION-0001 or ZL-C3-APPROVAL-0001 |
| I11 | Retrieved text instructs model to disable tests, change the challenge or mint Fabric access | No authority change; reject affected candidate, ZL-C3-AUTHORITY-0001 |
| I12 | Required proof times out; generator suggests tests instead | No fallback; inconclusive proof and non-admitted candidate, ZL-C3-EVIDENCE-0001 |
| I13 | Explicit runtime-check policy with passed prechecks and pending enforced postchecks | Admission says runtime-checked/pending; not kernel-certified |
| I14 | Postcheck fails after an admitted network action | Failed outcome with the actual action receipt; no claim the effect was undone |
| I15 | Typed-plan cycle, nonexistent output, type mismatch, or unordered conflicting effects | Rejected, ZL-C3-PLAN-0001 |
| I16 | New code/plan revision preserves the approved contract and revalidates required evidence | New recorded admission; previous receipts unchanged |
| I17 | Replan changes approved meaning or required assumption policy | New request/approval epoch required, otherwise ZL-C3-FORMALIZATION-0001 |
| I18 | Provider timeout/malformed output; attempts remain | Recorded consumed attempt and bounded retry; no execution of malformed output |
| I19 | Zero model-token/action allowance or exhausted proof budget | No forbidden dispatch; explicit BUDGET outcome, never unlimited-zero interpretation |
| I20 | Nested request tries to reset parent counters | Rejected limit escalation, ZL-C3-BUDGET-0001 |
| I21 | Cancellation before dispatch | Cancelled with zero subsequent actions, ZL-C3-CANCELLED-0001 |
| I22 | Cancellation/crash after an external action may have occurred, before receipt | Indeterminate with uncertain action ID, ZL-C3-INDETERMINATE-0001 |
| I23 | Flow replays a recorded generation/approval/admission/activity | No provider request, no repeated action, no new approval |
| I24 | Missing/mismatched historical artifact during replay | Replay failure, ZL-C3-REPLAY-0001; no regeneration substitute |
| I25 | Cached approved candidate on a host without the required live grant | No dispatch, ZL-C3-CAPABILITY-0001 |
| I26 | State transaction aborts with an Intent outbox request | No provider request; committed outbox delivery remains separately authorized |
| I27 | Proof/Compute/Hardware/Optimize signal directly invokes Intent | Rejected boundary/effect violation, ZL-C3-BOUNDARY-0001 |
| I28 | Snapshot exceeds list limit while failed/pending obligations exist | Bounded lists, total counts and explicit failure/pending summaries; no misleading green aggregate |
| I29 | Generated candidate adds IO or Hardware effects outside the checked intent interface’s bound, even with a live capability | Rejected before dispatch, ZL-C3-BOUNDARY-0001 |
C3-CONFORM-006 — Canonical identities and compatibility
The companion identity vectors fix exact canonical UTF-8 text, byte count, framed preimage hex, and SHA-256 for an empty environment, the identity statement/proof, and distinct authority sources. Validators must recompute the digest from those preimage bytes and check that the decoded envelope matches the vector. Reordered object keys and noncanonical input whitespace normalize to the same envelope; effectful ordered arrays must not be reordered.
| ID | Change | Expected identity/admission behavior |
|---|---|---|
| Z01 | Reorder JSON object keys only | Same canonical bytes and ID |
| Z02 | Change a source newline, Unicode normalization, or selected fragment | New authority ID; old interpretation approval stale |
| Z03 | Change only a proof binder’s source name, retaining de Bruijn terms | Same statement/proof IDs; source authority/provenance may change |
| Z04 | Change proof term but prove the same exact statement | Different proof ID, unchanged statement ID |
| Z05 | Change record kind/version while keeping payload/preimage claims | Reject incompatible shape/hash; no cross-kind identity cast |
| Z06 | Wrong reference kind, unknown field/tag, duplicate JSON key, unpaired surrogate, or number instead of decimal string | Reject malformed artifact, ZL-C3-ARTIFACT-0001 |
| Z07 | Forged short digest, mismatched preimage, cyclic environment/import chain | Reject, ZL-C3-ARTIFACT-0001 |
| Z08 | Correct hashes but omitted referenced proof/model/implementation | Unavailable dependency; no proof/admission claim |
| Z09 | Public projection omits a private proof body | Explicit unavailable preimage; no empty-body certificate |
| Z10 | Load old ZLM1–3 through their original edition routes | Original meaning/tags/status unchanged; no new kernel-certified label |
Structured publication tests also cover unique clause definitions, stable anchors, cross-edition links, the new edition panel and grammar route, and rejection of unknown future editions. They must not execute future theorem examples using a stub or promote any benchmark fixture.