§02c Jupiter — Non-Language Bridge — Interaction-protocol lift to order-typed form
Mars® Spec › §02c Jupiter — Non-Language Bridge › Interaction-protocol lift to order-typed form
← Scope-of-applicability certificates · Section index · Outputs →
9. Interaction-protocol lift to order-typed form
An interaction-protocol target has no accessible internal IR. The §02a §5a witness chain applies to it through the following protocol-lift path.
(i) Protocol-specification lift. The declared interaction-protocol specification is lifted to an order-typed protocol model — a formal representation of the protocol’s permissible exchange sequences and state transitions, typed against the orders of the governing domain model. Each permissible sequence and each state transition is assigned to one or more orders. The protocol model is a first-class artifact subject to the IR identity and versioning requirements of §02a §5a.1: it carries an IR identity, a transformation identity (identifying the lift method and parameters), the type-state distribution over its elements, and a content hash.
(ii) Trace-record lift. Observed interaction traces are lifted to order-typed trace records — each observable external-state transition is assigned to one or more orders. Each trace record carries: the interaction session identity, the observed sequence of external-state transitions, the order assignments for each transition, and a content hash. Where a transition cannot be assigned to any declared order, it is carried as an untyped-pending element (§02a §5a.1) with a disambiguation record.
(iii) Analysis-ready representation. The protocol model and the order-typed trace records together constitute the analysis-ready representation over which IR-level and post-IR battery methods operate. The protocol model takes the role of the IR; the trace records take the role of the input elements. Symbolic execution (§02a §5a.5) operates over the protocol model with the trace records as the concrete instantiation of the symbolic state.
Witness chain for interaction-protocol targets. The §02a §5a.2 witness chain for an interaction-protocol target links through:
[signal links if any] → [protocol-specification lift link] → [trace-record lift link] → [traversal witness link(s)] → [analysis-act links] → [verdict link]Each link carries the minimum required fields of §02a §5a.2. The protocol-specification lift link records: the protocol-specification content hash, the order-typed protocol model’s IR identity and content hash, and the lift transformation identity. The trace-record lift link records: the interaction session identity, the trace-record content hash, the order assignment coverage, and any untyped-pending elements with their disambiguation records. Where governed traversal (§02a §4b) is used during analysis of the protocol model and trace records, traversal witness links are required between the trace-record lift link and the analysis-act links, under the same requirements as §02a §5a.2 and §02b Field 7; a chain that omits traversal witness links where traversal was used is structurally incomplete for this target class. An interaction-protocol witness that omits the protocol-specification lift link or the trace-record lift link does not satisfy the §02a §5a.2 chain requirement for this target class.
Scope and falsifier implications. The order-type coverage of the protocol model and the trace records determines the scope invariant (§02b Field 5) for this target: the verdict holds within the scope of the interaction protocol specification and the observed trace set. Untyped-pending elements from the trace lift that are not disambiguated before analysis produce declared-irreducible entries (§02a §5a.4) and narrow the certified scope accordingly. Any revision to the interaction-protocol specification, or re-execution of the interaction producing a different trace set, invalidates the prior-version witness chain and triggers falsifier condition (d) of §02b §2.7.
← Scope-of-applicability certificates · Section index · Outputs →