invariants

package
v0.18.0 Latest Latest
Warning

This package is not in the latest version of its module.

Go to latest
Published: Jul 20, 2026 License: MIT Imports: 10 Imported by: 0

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

func Check(corpus adr.Corpus, root string, cfg *config.InvariantConfig) ([]Finding, []Note, error)

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

func DeclaringADRs(corpus adr.Corpus) (map[string]Decl, error)

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.

const (
	ClassBacked   Class = "backed"
	ClassUnbacked Class = "unbacked"
)

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

type Finding struct {
	Slug   string
	ADR    string // filename of the declaring ADR
	Status Status
}

Finding is an Implemented-ADR invariant slug whose backing declaration is not satisfied.

func (Finding) Detail

func (f Finding) Detail() string

Detail is a human, language-neutral remedy line for the finding.

func (Finding) Line

func (f Finding) Line() string

Line renders the finding as a single human-readable line (no leading indent/column), shared by `awf check` and `awf invariants`.

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

func MarkersUnder(root string, cfg *config.InvariantConfig, paths []string) ([]MarkerHit, error)

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

type Note struct {
	Slug string
	Text string
}

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.

func (Note) Line added in v0.18.0

func (n Note) Line() string

Line renders the note as a single human-readable line for the `note:` channel.

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"
)

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL