Assurance Reference¶

EvidenceStrength¶

Vocabulary¶

Two EvidenceStrength vocabularies coexist. Both are values of class EvidenceStrength(str, Enum) in lola/ssfc_taxonomy.py.

Value	Meaning
`PROVED`	Mathematically complete for the stated scope.
`PROVED-CONDITIONAL`	Holds subject to the listed ASSUME clauses; proved by universal attractor analysis. Recovery analysis only.
`NOT-PROVED`	Analysis cannot establish the property. Not a solver failure; a design finding. Recovery analysis only.
`NOT-REFUTED`	Conservative or over-approximative; no counterexample found but completeness is not guaranteed.
`UNKNOWN`	Solver timeout or encoding gap.
`ASSUMED`	Explicit engineering assumption; not verified.

Scope of recovery-specific values¶

PROVED-CONDITIONAL and NOT-PROVED are emitted only by the recovery analysis (lola/ssfc_recovery.py). The SSFC structural claims produced by check_all() use PROVED and NOT-REFUTED; they do not emit PROVED-CONDITIONAL or NOT-PROVED.

SSFC Structural Claims¶

These claims are produced by check_all() in lola/ssfc_report.py.

Claim ID	What it checks	Evidence strength	Approximation / scope
`C-SAF`	P-invariant: every reachable marking is a valid SSFC marking (no impossible token patterns).	`PROVED`	Complete algebraically.
`C-INT`	Region integrity: every reachable marking respects region membership (each region has exactly one active place).	`PROVED`	Complete over `NetModel`.
`C-DEAD`	No dead states: every leaf state (non-superstate) has at least one outgoing transition.	`PROVED`	Structural; does not check guard satisfiability.
`C-SYNC-DEAD`	No JOIN source orphan: every place in a JOIN's source set is reachable.	`PROVED`	Stated scope only; co-reachability across regions is out of scope.
`C-GUARD-SAT`	Guard satisfiability: every transition guard is satisfiable under the type domain.	`PROVED`	Complete over BitVec domain.
`C-DET`	Guard disjointness: no two outgoing guards from the same state can both be satisfied simultaneously.	`PROVED`	Complete over BitVec domain.
`C-DATA-DEAD`	Data dead transition: at least one transition guard per non-terminal state is satisfiable under all ASSUMEs.	`PROVED`	Complete over BitVec domain.
`C-REACH`	State reachability: a SAT-based BFS finds a path to the state.	`NOT-REFUTED` on PASS (path found is not a complete proof); `PROVED` on WARN (no path found even in the over-approximation confirms true unreachability).	Per-edge-SAT BFS; sound (no false WARN) but incomplete on PASS.
`C-HOME`	Home-state reachability from all marking graph states.	`NOT-REFUTED`	Per-edge-SAT BFS witness.
`C-NO-STUCK-MARKING`	No terminal non-home marking is reachable.	`NOT-REFUTED`	Marking-graph BFS over reachable markings.
`C-INV`	State invariant (`INVARIANT` annotation): an SMT invariant claim at a specific state.	`PROVED` if proved; `NOT-REFUTED` if validated by testing only.	Present only when `ssfc` is passed to `check_all()`.
`C-ASSUME`	ASSUME clause acknowledgement: the SSFC has explicit ASSUME clauses used as premises.	`PROVED` (structural).	Present only when `ssfc` is passed to `check_all()`.
`C-STRUCT-PATH`	Structural liveness path: a guard-ignoring BFS confirms a path from the initial state to a terminal or home state.	`PROVED`	Guards ignored; not a liveness guarantee.
`C-STRUCT-REACH`	Structural reachability per place: every place in the net is reachable from the initial marking (marking-graph BFS).	`PROVED`	Marking graph required.
`C-STRUCT-HOME`	Backward reachability to home markings: every reachable non-terminal marking has a path to a home marking (backward BFS).	`PROVED`	Marking graph required.
`C-REVERSI`	Reversibility to the initial marking: every reachable non-terminal marking can reach the initial marking.	`PROVED` on PASS; `NOT-REFUTED` on WARN.	Backward BFS from each marking to the initial marking; marking graph required.
`C-NO-STUCK-Z3`	No stuck marking under Z3: no reachable marking has all transition guards UNSAT under ASSUMEs.	`PROVED`	Marking-graph + Z3; exact query.
`C-WITHIN-FEASIBLE`	WITHIN annotation: a feasibility witness exists for the timing bound.	`NOT-REFUTED`	Existential feasibility; not a timing guarantee.

Signal Ownership Analysis¶

OwnershipClass¶

Defined in lola/ssfc_ownership.py.

Class	Meaning
`SINGLE_WRITER`	Exactly one `WriteSite` writes to this signal.
`EXCLUSIVE_MULTI_WRITER`	Multiple `WriteSite`s exist; all pairs are proved mutually exclusive (cannot be active in the same scan). Mutual exclusion is formally proved; safe to use.
`COMPATIBLE_MULTI_WRITER`	Some co-activatable `WriteSite` pairs exist, but all such pairs are proved to write the same value. No conflict.
`CONFLICTING`	At least one co-activatable pair of `WriteSite`s writes different or unknown values. Design finding: the signal has a write conflict.
`UNKNOWN`	Co-activation could not be determined (mutual exclusion neither proved nor disproved). Does not imply conflict.

Epistemics¶

CONFLICTING requires: co-activatable = True AND compatible = False.
Co-activatable but value-unknown → UNKNOWN, not CONFLICTING.
EXCLUSIVE_MULTI_WRITER is architecturally safe: the mutual exclusion proof covers all scan-cycle configurations.

API¶

analyze_ownership(ssfc, net, mg) → OwnershipReport

Method	Returns	Meaning
`OwnershipReport.conflict_free()`	`bool`	`True` if no `CONFLICTING` signals.
`OwnershipReport.analysis_complete()`	`bool`	`True` if no `UNKNOWN` signals.
`OwnershipReport.is_clean()`	`bool`	`conflict_free()` AND no policy violations.
`OwnershipReport.conflicts()`	`List[SignalOwnership]`	All `CONFLICTING` signals.
`OwnershipReport.unknowns()`	`List[SignalOwnership]`	All `UNKNOWN` signals.

Transitive Component Effects¶

When an SSFC has WIRING blocks that reference State.X (state activity marker), LoLa traces the chain:

state activation → wiring → child_instance.input → (child FB) → child_instance.output → parent output

Each such chain is a ComponentEffect. They appear in OwnershipReport.component_effects.

Policy Gates¶

Configured in project TOML under [ssfc_assurance].

Key	Default	Effect
`allow_exclusive_multi_writer`	`true`	Permit `EXCLUSIVE_MULTI_WRITER` signals.
`allow_compatible_multi_writer`	`true`	Permit `COMPATIBLE_MULTI_WRITER` signals.
`allow_unknown`	`true`	Permit `UNKNOWN` signals.
`allow_conflict`	`false`	Permit `CONFLICTING` signals. Enabling is unusual.

Recovery and Progress Analysis¶

Claim Levels¶

Produced by analyze_recovery(source_state, home_state, ssfc, net, mg) in lola/ssfc_recovery.py.

Level	Quantifier	What is proved	Approximation
`STRUCTURAL`	∃	A path from source to home exists in the marking graph, ignoring all guards.	Guards not checked; over-approximation.
`POSSIBLE`	∃	A path exists where every transition guard is satisfiable under ASSUMEs (SAT).	Per-edge SAT; guard satisfiability checked independently per transition, not as a coherent multi-scan trace.
`GUARANTEED`	∀	Every admissible execution from source eventually reaches home. Proved by universal attractor over `PossibleSucc(M)`.	Requires ASSUME clauses for non-tautological guards; result may be `PROVED-CONDITIONAL`.
`BOUNDED`	∀	Every admissible execution reaches home within N scans. N = max attractor rank over source markings.	Same as `GUARANTEED`; additionally, each scan fires exactly one transition (no-stall guaranteed by attractor membership condition).

Definitions¶

PossibleSucc(M) = {M′ | SAT(guard(t) ∧ assumes) for some transition t: M→M′}. All markings reachable from M in one scan under some admissible input.

no_stall(M) = UNSAT(assumes ∧ ¬g₁ ∧ … ∧ ¬gₙ) where g₁…gₙ are outgoing guards. The system cannot idle in M indefinitely.

Universal attractor:

Attr₀ = home_marks
Attr_{k+1} = Attr_k ∪ {M | no_stall(M) ∧ PossibleSucc(M) ≠ ∅ ∧ PossibleSucc(M) ⊆ Attr_k}

Attractor rank:

B(home) = 0
B(M)    = 1 + max_{M′ ∈ PossibleSucc(M)} B(M′),  for M ∈ Attr \ home_marks
BOUNDED = max_{M ∈ source ∩ Attr} B(M)

EvidenceStrength for Recovery Claims¶

Strength	Condition
`PROVED`	Claim holds without any ASSUME clauses.
`PROVED-CONDITIONAL`	Claim holds given the listed ASSUME clauses (`assumptions_used` is non-empty).
`NOT-PROVED`	Claim does not hold: the analysis found a reachable marking outside the attractor, or a stall-possible marking. Design finding; not a solver failure.

RecoveryClaim Fields¶

RecoveryClaim has four RecoveryEvidence sub-results:

Field	Type	Description
`.structural`	`RecoveryEvidence`	Result for the `STRUCTURAL` level.
`.possible`	`RecoveryEvidence`	Result for the `POSSIBLE` level.
`.guaranteed`	`RecoveryEvidence`	Result for the `GUARANTEED` level.
`.bounded`	`RecoveryEvidence`	Result for the `BOUNDED` level.

RecoveryEvidence Fields¶

Field	Type	Description
`.strength`	`EvidenceStrength`	Classification of this level's result.
`.assumptions_used`	`List[str]`	Load-bearing ASSUME labels: those whose removal causes `GUARANTEED` to fail (deletion test). May be smaller than the full ASSUME list.
`.bound_scans`	`Optional[int]`	For `BOUNDED`: the worst-case scan count. `None` otherwise.
`.reason`	`str`	Human-readable explanation of the result.

GuidedSynthesisWarrant¶

A GuidedSynthesisWarrant records that a combinational FUNCTION_BLOCK's RULE-defined outputs were proved correct by a bounded model checker (Kani or CBMC), not by the LoLa internal Z3 synthesiser.

Module: lola.guided_synthesis\ Concept: Guided synthesis and EXTERN — same warrant, different source\ How-to: Guided synthesis workflow

Fields¶

Field	Type	Description
`block`	`str`	Name of the `FUNCTION_BLOCK` the warrant covers.
`declaration_sha256`	`str`	SHA-256 of the canonical block contract (inputs, outputs, ASSUME, RULE, synthesis targets). Stable across formatting changes; changes on any contract change.
`semantic_contract_sha256`	`str`	SHA-256 of the canonical expanded AST definitions behind semantic predicates. Stable across locations/formatting and changed by semantic implementation changes.
`candidate_abi`	`str`	ABI version of the accepted candidate, e.g. `"lola-gs-rust-combinational-v2"`.
`candidate_body_sha256`	`str`	SHA-256 of the accepted candidate body text.
`proof_backend`	`str`	Proof tool: `"kani"` or `"cbmc"`.
`proof_source_sha256`	`str`	SHA-256 of the proof harness source that was run.
`rules`	`tuple[str, ...]`	Human-readable RULE texts from the block's contract.
`target`	`str`	Code-generation target: `"rust"` or `"st"`.
`digest`	`str`	SHA-256 of all fields above (excluding `digest` itself).

Factory function¶

from lola.guided_synthesis import make_guided_synthesis_warrant

warrant = make_guided_synthesis_warrant(acceptance_json)

acceptance_json must be a dict with schema: 3, produced by acceptance_receipt() and written to acceptance.json by lola guided accept.

Raises GuidedSynthesisError if the schema is unknown or required keys are missing.

Digest function¶

from lola.guided_synthesis import guided_synthesis_warrant_digest

digest = guided_synthesis_warrant_digest(warrant)

Returns the SHA-256 of the canonical warrant payload (all fields except digest). Used for content-addressing and tamper detection.

Using with `compile_source`¶

from lola import compiler
from lola.guided_synthesis import make_guided_synthesis_warrant
import json

warrant = make_guided_synthesis_warrant(json.loads(acceptance_path.read_text()))

comp = compiler.compile_source(
    source,
    guided_synthesis_warrants={"PumpBank": warrant},
)

Parameter: guided_synthesis_warrants: dict[str, GuidedSynthesisWarrant] | None

When provided, the compiler checks each block whose name appears as a key. If the block has synthesis targets and the warrant's declaration_sha256 matches the current source contract, CEGIS synthesis is skipped and the warrant discharges the RULE proof obligations.

Errors raised by compile_source:

Error	Cause
`ValueError: must be a GuidedSynthesisWarrant`	Dict value is not a `GuidedSynthesisWarrant` instance.
`ValueError: declaration_sha256 does not match`	Source contract changed after acceptance; re-run `lola guided accept`.
`ValueError: could not compute declaration digest`	Source could not be re-parsed for digest comparison.

In `program.assurance`¶

After successful compilation with a warrant, the warrant is stored in:

program.assurance.guided_synthesis_warrants  # dict[str, GuidedSynthesisWarrant]

Keyed by block name. Included in the G2.8 assurance seal.

Acceptance receipt format (`schema: 3`)¶

The acceptance receipt written by lola guided accept has this structure:

{
  "schema": 3,
  "block": "PumpBank",
  "target": "rust",
  "request_version": 1,
  "candidate_abi": "lola-gs-rust-combinational-v2",
  "declaration_sha256": "<64 hex chars>",
  "semantic_contract_sha256": "<64 hex chars>",
  "source_sha256": "<64 hex chars>",
  "candidate_body_sha256": "<64 hex chars>",
  "proof_backend": "kani",
  "proof_source_sha256": "<64 hex chars>",
  "rules": ["COUNT(i IN 0..2 : run[i]) = demand", "..."]
}

source_sha256 is the SHA-256 of the source text at acceptance time (for traceability). declaration_sha256 is the stable contract identity (used for cache and warrant binding). It includes semantic_contract_sha256, which binds the compiler-owned expanded meaning of semantic predicates rather than only their human-readable spelling.