Skip to main content

4. Semantic Bridge Consistency (Viper/Silicon & TLA+/TLC)

1. One Source, Two Verification Lanes​

Sector9 keeps local deductive verification and protocol-level temporal checking tied to the same authored program, but it is important not to describe this as "two proofs" of the same thing.

The lanes have different jobs:

  1. Viper/Silicon lane: Sector9 source is lowered through MVIR into Viper. Silicon checks the generated verification conditions, and Z3 discharges the resulting SMT queries. This lane owns local per-handler correctness: contracts, frames, permissions, actor invariants, and obligations around await boundaries.
  2. TLA+/TLC lane: Protocol roots are translated through a protocol extraction and PIR pipeline into TLA+. TLC model-checks the generated finite or abstract protocol model. This lane owns cross-message scheduling, interleavings around await, failure paths, rollback/commit behavior, and temporal claims such as safety and liveness.

The bridge exists so the TLA+ model does not silently invent a different view of the implementation. If an implementation suspends, touches protocol-visible state, or calls a trusted companion, that fact must either appear in the bridge/PIR surface or fail closed.

2. Current Bridge Architecture​

The current architecture is not "Sector9 source directly to TLA+", and it is also not "both backends branch equally from MVIR." MVIR is Viper-owned. TLA consumes protocol DSL catalogs plus typed semantic facts exported from the Viper/MVIR lane.

The current pipeline is:

  1. src/tla/trans_scan.ml extracts protocol catalogs from *.protocol.sr9 roots: endpoints, roles, properties, and schema/state declarations.
  2. src/pipeline/pipeline.ml and src/viper/tla_semantics.ml build MVIR for protocol-coupled units and export post-Await semantic facts.
  3. src/tla/pir_build.ml merges protocol catalogs with bridge facts into Protocol IR (PIR).
  4. src/tla/pir_passes.ml and src/tla/pir_wf.ml normalize and check PIR.
  5. src/tla/pir_emit_tla.ml emits deterministic .tla and .cfg artifacts.
  6. --verify --tla preflights trusted local companion actors through the normal Viper verifier, then runs TLC on the emitted model.

The shared surfaces are explicit:

  • src/verify_shared/phase_surface.ml is the shared authored phase/root surface. Viper and TLA both consume this so public async/phase interpretation is not duplicated in backend-local heuristics.
  • src/verify_shared/tla_bridge_schema.ml is the typed bridge schema exported by src/viper/tla_semantics.ml and consumed by the TLA PIR builders.
  • src/viper/tla_semantics.ml owns method semantic facts: effect class, await/phase data, read/write paths, call edges, and source anchors.
  • src/tla/trans_* owns protocol DSL extraction. It does not reimplement method effect or await analysis.

This split is the core consistency rule: Viper owns method semantics, TLA owns protocol catalogs and temporal policy, and PIR is the reviewed handoff layer.

3. Fail-Closed Protocol Linkage​

PIR construction is intentionally fail-closed. Protocol-relevant behavior must be mapped, excluded, or rejected.

Build-stage failures include:

  • TLA-PIR-BUILD-004: public protocol-state-touching method without endpoint mapping.
  • TLA-PIR-BUILD-005: unknown state-touch classification for a completeness gate.
  • TLA-PIR-BUILD-006: ambiguous endpoint-to-method identity.
  • TLA-PIR-BUILD-007: unsupported or failed contract lowering.

The authored protocol surface provides the escape hatches, but they remain explicit:

  • endpoint(...) maps public shared/query methods into the modeled protocol action catalog.
  • ProtocolSchema.callBinding(...) disambiguates same-handle trusted call sites.
  • ProtocolSchema.endpointMode(role, action, #callee_only) keeps a trusted callee action available only as a bound call target.
  • ProtocolSchema.surfaceExclude(...) narrows the public state-touching surface for a modeled root, while still requiring excluded state-touching methods to be declared deliberately.
  • ProtocolSchema.stateBinding(...) and ProtocolSchema.stateBindingFrom(...) bind actor state roots into protocol state projections. Raw State declarations are not automatically promoted into role-bound projections.

This is the key production-grade property of the bridge: scoping is reviewable and fail-closed, not hidden in emitter heuristics.

4. Phase Segmentation and Await Semantics​

await is a semantic boundary. The Viper lane checks local obligations around those boundaries; the TLA lane models what can happen between them.

The current bridge exports real phases plus coarse await_boundaries summaries. PIR keeps one method-level action id for property scopes, but TLA emission can emit phase-backed transitions such as Action_<method>_PhaseN under that method action.

The public authored phase-contract surface is deliberately narrow today:

  • phase blocks must be top-level, straight-line, statement-only, unit-typed, and await-free internally;
  • explicit single await separators are supported;
  • carried separator bindings can be referenced in later phase contracts;
  • result is restricted to phase ensures, and on non-unit methods it belongs to the final phase with an explicit pure return tail;
  • calls, arbitrary body locals, unsupported projections, await*, and unresolved suspending helper shapes fail closed in the public phase-contract slice.

This keeps the emitted temporal model honest while the system evolves toward richer CFG/PC-level segmentation.

5. Contract-Faithful TLA Emission​

The TLA emitter renders normalized PIR; it should not invent action semantics.

When contracts lower successfully into PIR:

  • requires clauses become action guards.
  • lowered ensures clauses become transition constraints.
  • reads and modifies paths drive frame information.
  • untouched modeled projections receive UNCHANGED constraints.
  • emitted action comments retain method and contract trace metadata.

TLC is therefore checking the interplay of the generated protocol transition relation, the authored protocol properties, and the assumptions that PIR records. A TLC counterexample means the protocol model, local contracts, trusted assumptions, or mapping choices are insufficient for the property being checked.

6. Current Limits​

This bridge reduces model/code drift, but it is not a full implementation-to-TLA equivalence proof.

Current important limits:

  • TLA+/TLC model-checks a finite or abstract model; it does not prove arbitrary unbounded properties by itself.
  • Some may-write behavior is still represented by typed path-local update skeletons, with fallback abstraction when no modeled touched projection can be derived.
  • Public method/phase compatibility checks are conservative coverage checks, not full logical implication solving.
  • Some Viper-specific constructs, such as permissions and triggers, do not have backend-neutral TLA meanings.
  • The public phase-contract surface intentionally rejects complex control flow around phase boundaries until the model has a richer public segmentation story.
  • Trusted and abstract/bodyless surfaces remain explicit assumptions, not facts proven by TLA.

These limits are part of the trust story. The page should describe them directly rather than implying that the bridge automatically proves all protocol behavior from implementation code.

7. Regression and Audit Lanes​

The bridge is guarded by deterministic tests and drift checks rather than by documentation alone.

Relevant lanes include:

  • src/viper/tla_semantics_test.ml for bridge schema, await, phase, and call-edge extraction behavior.
  • src/tla/*_test.ml for PIR build, well-formedness, pass, and emission behavior.
  • ./test-tla.sh for manifest-driven TLA guard checks.
  • ./scripts/run-generated-obligation-crosscheck.sh
  • ./scripts/run-lowering-crosscheck.sh
  • ./scripts/run-tla-emission-crosscheck.sh
  • ./scripts/run-verifier-doc-audit.sh

8. Summary​

The semantic bridge is the handoff between local Viper/Silicon deductive verification and TLA+/TLC protocol model checking. Its current correctness story is grounded in shared authored phase extraction, typed Viper-to-TLA bridge facts, explicit protocol mappings, PIR well-formedness gates, deterministic emission, and fail-closed diagnostics.

That is the maintainable claim: one authored program, two verification lanes, and a typed fail-closed bridge that makes protocol-relevant drift visible instead of silently trusting a hand-written model.