Documentation
¶
Overview ¶
Package invariants checks that each Implemented ADR's `invariant: <slug>` declaration is backed by a proof `<marker> invariant: <slug>` comment in a configured source file. With `invariants.testGlobs` set, a proof marker backs a slug only in a test file; absent testGlobs it falls back to source-glob scope (ADR-0105). An `unbacked-invariant: <slug>` declaration is a reasoned contract exempt from the proof requirement but carrying a `Verify:` note; a `touches-invariant: <slug>` marker is advisory context, never backing. The comment marker and the files scanned are language-configurable via the project's invariants config; nothing here assumes Go.
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func Check ¶
Check returns the hard Findings and advisory Notes for a project's invariants. No required slugs → nil. cfg disabled → nil. cfg nil or source-less → every required slug is Unchecked. Otherwise, per the ADR-0105 model: a backed slug with no proof marker in backing scope is Unbacked; an unbacked slug with a proof marker in scope is UnbackedHasProof; an unbacked slug whose declaration lacks a `Verify:` note is MissingVerify. Advisory notes cover a marker naming an undeclared slug (dangling) and a bare `touches-invariant:` marker.
func DeclaringADRs ¶ added in v0.18.0
DeclaringADRs returns the slug → declaring-ADR map for adrs: every invariant slug declared (in the Invariants section) by an Implemented ADR, carrying its backing class (backed `invariant:` / unbacked `unbacked-invariant:`) and, for unbacked declarations, the `Verify:` guidance text the bullet carries. Token retirements (ADR-0120) are applied. It refuses two Implemented ADRs declaring the same slug (duplicate) and a retirement of a slug no ADR declares (dangling). Check and ContextFor (ADR-0104 Tier 1) share it.
Types ¶
type Class ¶ added in v0.18.0
type Class string
Class is an invariant's declared backing class (ADR-0105): backed invariants require a proof marker; unbacked ones are reasoned contracts carrying a `Verify:` note.
type Decl ¶ added in v0.18.0
type Decl struct {
ADR string // filename of the declaring ADR
Class Class
Verify string // Verify: guidance text; only meaningful for ClassUnbacked
}
Decl is a declared invariant slug's declaring ADR, its backing class, and - for an unbacked declaration - the `Verify:` guidance text its bullet carries (empty when absent). Check treats an empty Verify on an unbacked declaration as a MissingVerify finding; ContextFor surfaces the text as the site note.
type Finding ¶
Finding is an Implemented-ADR invariant slug whose backing declaration is not satisfied.
type MarkerHit ¶ added in v0.18.0
type MarkerHit struct {
Slug string
Proof bool // surfaced by a proof `invariant:` marker under the query
Touches bool // surfaced by a `touches-invariant:` marker under the query
Notes []string // touches-marker site notes (deduped, sorted, non-empty)
}
MarkerHit is an invariant slug found under a queried path: the marker kind(s) that surfaced it - a proof `invariant:` marker, a `touches-invariant:` marker, or both - and, for touches markers, the deduped, sorted, non-empty site notes. (ADR-0106: both marker kinds count as present under a path.)
func MarkersUnder ¶ added in v0.16.0
MarkersUnder returns the slug-sorted MarkerHits for the invariant markers that lie in a file sitting under one of paths (a queried path P owns file F when F == P or F is prefixed by P+"/"). A file is scanned when it matches an `invariants.sources` glob or a `cfg.TestGlobs` glob (the ADR-0106 union scan), so a proof marker in a test file governing production code queried by its path still surfaces. Both the proof `invariant: <slug>` and the advisory `touches-invariant: <slug>[ note]` markers count as present. paths are slash-separated repo-relative paths. It reads only source files and writes nothing.
type Note ¶ added in v0.18.0
Note is a non-failing advisory from the invariant scan (ADR-0105 item 5): a proof/touches marker naming a slug no Implemented ADR declares, or a bare `touches-invariant:` marker carrying no note. Notes ride the `awf check` `note:` channel; they never feed the failure count.
type Status ¶
type Status string
Status classifies an invariant finding.
const ( Unbacked Status = "unbacked" // declared backed, but no proof marker in backing scope Unchecked Status = "unchecked" // no invariant sources configured (and not disabled) // UnbackedHasProof: an `unbacked-invariant:` declaration for which a proof // marker exists in backing scope (ADR-0105 unbacked-refuses-proof). UnbackedHasProof Status = "unbacked-has-proof" // MissingVerify: an `unbacked-invariant:` declaration lacking a `Verify:` note // (ADR-0105 unbacked-requires-verify-note). MissingVerify Status = "missing-verify" )