Skip to content

§02b Jupiter — Certification & Attestation — Externally-observable properties

Mars® Spec§02b Jupiter — Certification & Attestation › Externally-observable properties

← ON_CHAIN_ANCHOR — verification-gated distributed-ledger commitment · Section index

8. Externally-observable properties

Conformance certificate:

Property Observable condition
SC1 — Differential admission/refusal at downstream gate Gate admits when certificate passes all checks; refuses when any check fails
SC2 — Recomputation-witness verification Re-derived verdict matches Field 4 verdict
SC3 — Cryptographic-signature verification The tamper-evident binding (Field 9) verifies over all invariant fields; a binding that covers only a subset of the invariant fields fails verification
SC4 — Falsifier-cascade observation Upon falsifier-condition occurrence, revocation cascades to downstream consumers within declared retention window
SC5 — Symmetric target-class enumeration Same certificate format applies to all three target classes
SC6 — Triad path declaration Field 3 carries path identifier from typed enumeration with matching evidence reference
SC7 — Interaction-protocol substitution Where target is interaction-mediated, verified target is the interaction protocol; certification path is interaction-protocol conformance testing
SC8 — Refusal of self-attestation Where deployment policy declares verifier independence, certificates with coincident verifier and target identities are refused with structural diagnostic
SC9 — Modality-agnostic conformance verification Same certificate structure and triad apply across non-linguistic modalities
SC10 — Target-of-analysis symmetry The interpretation-producing mapping that produced a Class B artifact is certifiable as a Class A program. An inspector verifies: (i) a valid Class A certificate exists for the interpretation-producing mapping; (ii) the Class B certificate’s Field 1 non-linguistic provenance chain references that Class A certificate; (iii) the Class B recomputation witness re-derives the interpretation verdict from the lift under the mapping’s governing specification. A Class B certificate that cannot be verified via these three checks fails SC10.
SC11 — Provenance-agnostic linguistic-artifact conformance Same process irrespective of producer — present system, another system, or human

Additional structural properties:

Properties G1, G4–G6, G9–G11 are defined here as their authoritative location. §02a §8 carries a cross-reference pointer to this section. G2, G3, G7, G8 are defined in §02a §8.

Property Observable condition
G1 — Pipeline-composed target requires topology record and stage witness chain Where the certified target is a Class A pipeline-composed artifact, Field 1 carries a pipeline-topology record and Field 7 carries a stage-level witness chain through the aggregation step; a certificate that omits either is observably non-conforming for this target class
G4 — Bootstrap provenance failure consequences declared Where a bootstrap provenance component is absent or unverifiable, the certificate carries a conditionally-conforming verdict (or non-conforming where multiple components fail) with a falsifier annotation recording the gap
G5 — Registry conflict resolved or declared Where two certificates share the same target, governing specification, certification path, and overlapping temporal validity windows, both carry a cross-certificate conflict flag and the conflict is either resolved or declared as differential certification
G6 — Composite-of-composites carries chain references, not inlined chains Where a constituent of an N-hop certificate is itself a composed certificate, the parent’s composition provenance record carries a content hash reference to the constituent’s chain, not an inlined copy
G9 — Provenance bundle co-presence (load-bearing) Field 4 and Field 7 are co-derived from the same analysis battery record: presenting a certificate where the verdict and witness originate from different battery runs produces a co-presence failure and immediate revocation; Field 2 governing-specification identity matches the specification referenced in Field 7’s recomputation; Field 9 binding is computed over the certificate’s own Fields 1–8, not imported from another certificate instance
G10 — No partial registration No certificate missing any of the nine structural invariants is present in the specification registry; a registry query for a partial certificate returns absent; the emission gate refuses registration until all nine invariants are co-present and verified
G11 — Admissibility relation registered and ADMIT/REJECT reproduced from it (load-bearing) The governing domain model’s admissibility relation is present as a registered artifact in the specification registry (§01 §6); an independent inspector re-derives the ADMIT or REJECT determination for any proposed composition from the registered relation alone; a governing specification produced by type-checking against an undeclared or unregistered admissibility rule is observably non-conforming; this property is load-bearing because the soundness anchor-inheritance records in the CertifiedBundle (B9) trace to order-typed soundness anchors that are themselves composed under the admissibility relation (§01 §6 order-typed soundness inheritance, D43) — a bundle whose anchor trail cannot be traced through a registered admissibility relation is structurally deficient

Delta-attestation lifecycle:

Property Observable condition
DA1 — Refusal-to-register on absent delta-attestation Submitting an amended artifact version without a corresponding delta-attestation object is refused at registration
DA2 — Recomputable delta-classification The delta-classification field value is reproduced by applying the declared classification function to the structural-difference record
DA3 — Recomputable attestation hash The attestation hash is reproduced from the recorded authority signatures over Fields (a)–(d)
DA4 — Class-specific differential cascade behavior Presenting amendments of each of the four classification values produces observably distinct cascade behaviors: no cascade (preserving), optional cascade (extending), required-with-deadline cascade (restricting), immediate cascade (breaking)
DA5 — Typed cascade record propagation Upon a scope-restricting or scope-breaking amendment, typed cascade records naming each affected downstream artifact are present in the audit trail within the declared retention window
DA6 — EUF-CMA-secure signatures The cryptographic signature on the delta-attestation object verifies under the declared scheme; tampered field content produces a failing verification
DA7 — Cross-portfolio cascade execution A scope-breaking amendment to a registered artifact produces observable invalidation of downstream non-language-provenance anchors, conformance certificates, actuation anchors, and scope-of-applicability certificates within the declared retention window
DA8 — Refusal of monotonic-non-cascade configuration Submitting a deployment configuration declaring that amendments to registered artifacts never require downstream re-discharge is refused at deployment registration

ON_CHAIN_ANCHOR (§6):

Property Observable condition
L1 — Verify-then-commit inversion (load-bearing) No state transition hash reaches the target ledger without a prior CERTIFY verdict from the procedural-verification gate; presenting a REFER or REFUSE verdict to the commitment mechanism produces no ledger write; presenting a CERTIFY verdict produces exactly one ledger write of the audit-record chain hash; a deployment that writes to the ledger before or independently of the verdict is observably non-conforming
L2 — Only the hash lands on-chain The on-chain entry for any commitment is exactly the chain hash of the audit record (32 bytes for SHA-256); the state transition content, audit-record content, specification content, and predicate content are absent from the ledger entry; an inspector with chain read access observing the on-chain entry cannot reconstruct the transition content from the ledger entry alone
L3 — Bidirectional linkage present after commitment After a successful ledger write, the audit record’s chaincode_commitment.txid field is populated with the ledger transaction identifier; an inspector can traverse from the audit record to the ledger entry and from the ledger entry back to the audit record; a CERTIFY audit record carrying a chaincode_commitment field with a null txid is structurally incomplete
L4 — Hash verification by independent party A party other than the deployment operator, given the on-chain hash and the audit record, recomputes the hash of the audit record and confirms it matches the on-chain value; a mismatch is independently observable without deployment access
L5 — Structural orthogonality of internal and external tamper evidence A conforming ON_CHAIN_ANCHOR deployment maintains both internal hash-chain tamper-evidence (§02a §3a.1) and on-chain external attestation; removing the internal chain while retaining on-chain commitment, or vice versa, is observably non-conforming; the two mechanisms are distinguishable by an inspector: internal evidence is verifiable from the audit chain alone; external evidence requires ledger read access
L6 — DDIL edge-queue causal ordering preserved Under DDIL conditions, queued commitments are submitted to the ledger in the causal order of their verdict issuance; an inspector observing the ledger entries and the reconnection-commitment record confirms that the on-chain sequence matches the audit-chain sequence; a deployment that submits queued commitments in non-causal order is observably non-conforming
L7 — CERTIFY verdict immutability under DDIL A CERTIFY verdict issued under DDIL conditions is not downgraded to REFER or withheld pending ledger reconnection; the verdict is final at issuance; only the external attestation is deferred; an inspector confirms the audit-record verdict timestamp precedes the ledger commitment timestamp by at most the reconnection window
BC1 — Behavioral-condition gate genus invariance A runtime or post-hoc gate for any registered behavioral-condition representation carries the identical structure — bracket declaration, order-type, representation kind, content hash, dual-locus invariance, delta-attestation lifecycle; a behavioral gate implementing this structure under a different condition name is observably this architecture, not a distinct one
MD1 — Behavioral modification detection for externally-hosted models An externally-hosted model’s registration declares a drift-equivalence threshold; a drift finding at or above the threshold produces immediate new-model treatment identical to a detected hash change with no modification record; registration without the declared threshold is refused

← ON_CHAIN_ANCHOR — verification-gated distributed-ledger commitment · Section index