Skip to content
Crucible logo Crucible

state/verify/symbolic

import "github.com/stablekernel/crucible/state/verify/symbolic"

Package symbolic reasons about a machine’s guards structurally — without executing them — over the kernel’s Core GuardNode tree. It answers whether a guard is satisfiable (can ever hold) and whether two guards are disjoint (can never both hold), and scans a machine for competing transitions whose guards overlap (candidate nondeterminism).

It is a bounded, pure-Go analyzer, not an SMT solver: it normalizes a guard to disjunctive normal form and checks each conjunctive clause for a per-field contradiction — numeric fields as intervals, discrete (string/bool/enum) fields as value sets. It is deliberately conservative: a Rich or named-leaf guard, a cross-field comparison, or a duration/time field it cannot model is treated as an unconstrained unknown, so it never reports a contradiction or a disjointness it cannot prove. This makes Contradiction and Disjoint sound (no false positives): a true verdict is always correct, while an unprovable case is reported as satisfiable / not-disjoint.

It consumes only the kernel’s own GuardNode and ContextSchema, so it adds no dependency and stays in the stdlib-only state module.

Index

Section titled “Index”

func Contradiction

Section titled “func Contradiction”
func Contradiction[S comparable](g state.GuardNode[S], schema state.ContextSchema) bool

Contradiction reports whether the guard is provably unsatisfiable — no context can make it true, so a transition it gates is dead. It is sound: it never reports a contradiction it cannot prove (an opaque, Rich, or cross-field guard yields false).

func Disjoint

Section titled “func Disjoint”
func Disjoint[S comparable](a, b state.GuardNode[S], schema state.ContextSchema) bool

Disjoint reports whether a and b are provably mutually exclusive — no context can satisfy both at once, so two transitions guarded by them can never both be enabled. It is the satisfiability of their conjunction, and is sound: it returns true only when the conjunction is provably unsatisfiable, so guards it cannot fully analyze are reported as not-disjoint (the safe answer for nondeterminism detection). It is the basis for finding competing transitions whose guards overlap.

func Satisfiable

Section titled “func Satisfiable”
func Satisfiable[S comparable](g state.GuardNode[S], schema state.ContextSchema) bool

Satisfiable reports whether the guard can ever hold. It is conservative: it returns false only when the guard is provably unsatisfiable (a contradiction over the analyzable Core constraints), and true otherwise — including guards it cannot analyze. So a false result is a proof of unsatisfiability; a true result may be “satisfiable” or merely “not provably unsatisfiable.”

type Overlap

Section titled “type Overlap”

Overlap reports two competing transitions — the same source state firing on the same event — whose guards are not provably disjoint, so both can be enabled at once: a candidate nondeterminism the analyzer could not rule out.

type Overlap[S comparable, E comparable] struct {
    // From is the shared source state, On the shared event.
    From S
    On   E
    // ToA and ToB are the two competing transitions' targets.
    ToA S
    ToB S
}

func Overlaps

Section titled “func Overlaps”
func Overlaps[S comparable, E comparable, C any](m *state.Machine[S, E, C]) ([]Overlap[S, E], error)

Overlaps scans a machine for competing transitions (same source, same event) whose guards are not provably disjoint. It is conservative: a pair is reported unless the analyzer can PROVE the guards mutually exclusive, so transitions guarded only by opaque guards (named Go-func or Rich) — or unguarded — are reported as potential overlaps. An empty result means every same-source/same-event pair is provably disjoint, i.e. the machine is provably deterministic on its guarded choices over the analyzable Core guards.

Generated by gomarkdoc