Documentation
¶
Overview ¶
Package propdoc derives the Status column of PROPERTIES.md from that document's own refutation register, so that one fact has one source.
PROPERTIES.md states propositions in section 3 and refutations in section 4. Status is a function of the two — see DeriveStatus — and the function is written down here rather than applied by hand. Maintaining status beside the register is what this package exists to prevent: two sources of truth for one fact drift apart, and the drift is invisible because both sources look authoritative. Discharging one of a proposition's two counterexamples used to leave its Status cell untouched, which made a real movement unreportable.
The authored inputs are the Basis cell (one or more scoped bases, each with its citation) and the register rows. Everything in the Status column is output.
A Basis cell claiming several scopes reduces to the **weakest** of them, not the strongest — see Reduce. A proposition quantifying over several execution routes is rarely covered equally on all of them, and reporting the best-covered route's strength as the proposition's overstates silently (#135).
Index ¶
- Constants
- Variables
- func DeriveStatus(b Basis, live, total int) string
- func Kind(status string) string
- type Basis
- type BasisKind
- type Citation
- type CitationDefect
- type CitationStats
- type Coverage
- type DischargeDefect
- type Doc
- func (d *Doc) CheckCitations(fetch LineFetcher) CitationStats
- func (d *Doc) Citations() []Citation
- func (d *Doc) DischargeDefects() []DischargeDefect
- func (d *Doc) Distribution() map[string]int
- func (d *Doc) Drifts() []Drift
- func (d *Doc) Propositions() []*Proposition
- func (d *Doc) Register() []Refutation
- func (d *Doc) Render() []byte
- func (d *Doc) Statuses() map[string]string
- func (d *Doc) Unknown() []string
- type Drift
- type LineFetcher
- type Proposition
- type Reduction
- type Refutation
- type ScopedBasis
- type Subject
Constants ¶
const ( // TierNone means no evidence is cited for the proposition. TierNone = "none" // TierWithdrawn means the proposition has been superseded and is no longer // measured; the citation names what replaced it. TierWithdrawn = "withdrawn" // TierIncomparable is the reduction of a multi-scope Basis cell whose scopes // do not share a Subject, so no meet exists. It is not a tier an author may // write: parseBasis derives it, and Reduce's Set names the bases it stands for. TierIncomparable = "incomparable" )
Tier values accepted in a proposition's Basis cell, in addition to the seven bases defined in section 2 of the document — see Bases, and note that a basis is a (Coverage, Subject) pair rather than a rung on a ladder.
const ( DischargedYes = "Yes" DischargedNo = "No" DischargedPartially = "Partially" )
Discharge values accepted in a register row's Discharged cell.
Variables ¶
var ( // ErrDischargeNoBasis is returned when a Yes cell names no basis, so the // reader cannot tell whether the evidence meets rule 11's floor. ErrDischargeNoBasis = errors.New("propdoc: a Discharged: Yes cell must name the basis of its evidence") // ErrDischargeNoCitation is returned when a Yes cell cites no artifact — // the case "Yes — closed completed" is, where the only thing offered is a // fact about the tracker. ErrDischargeNoCitation = errors.New("propdoc: a Discharged: Yes cell must cite the evidence, not the closure") )
Rejection reasons for a Discharged: Yes cell, exported so a test can assert which check fired rather than that some check did. A rejection from the wrong reason is not evidence for the right one.
var ( // ErrBasisScopeUnnamed is returned when a multi-scope cell leaves an entry's // bound unnamed. A set of bases over unnamed scopes says nothing: the pair // says *how* a domain was covered and only the bound says *which* domain // (§2.1 rules 2 and 10). ErrBasisScopeUnnamed = errors.New("propdoc: every entry of a multi-scope Basis cell must name its scope with @") // ErrBasisScopeRepeated is returned when two entries name the same scope. // Two bases for one scope puts the choice between them back on the reader, // and the strongest-wins reading is the one this grammar exists to remove. ErrBasisScopeRepeated = errors.New("propdoc: two entries of a Basis cell name the same scope; merge them") // ErrBasisScopeUncited is returned when an entry of a multi-scope cell cites // nothing. A basis with no citation is not a basis, per section 3, and // per-scope bases mean per-scope evidence. ErrBasisScopeUncited = errors.New("propdoc: every entry of a multi-scope Basis cell must cite its evidence") // ErrBasisNotWeakestFirst is returned when a multi-scope cell does not lead // with the entry it reduces to. The reduction is not written in the cell — it // is derived — so the only thing a reader's eye lands on is the first entry, // and a cell leading with its strongest scope reproduces the overstatement // even though every derived number is right. ErrBasisNotWeakestFirst = errors.New("propdoc: a multi-scope Basis cell must lead with the scope it reduces to") // ErrBasisWithdrawnScoped is returned when withdrawn appears as one entry of // a multi-scope cell. Withdrawal is a fact about the whole proposition — it // is no longer measured — so it cannot be true of one scope and not another. ErrBasisWithdrawnScoped = errors.New("propdoc: withdrawn describes a whole proposition and cannot be one scope of a Basis cell") // ErrBasisScopeUnterminated is returned when an entry opens a scope with @ and // never closes it with an em dash, so the citation cannot be told from the // bound. ErrBasisScopeUnterminated = errors.New("propdoc: a Basis entry opening a scope with @ must close it with an em dash before its citation") )
Rejection reasons for a multi-scope Basis cell, exported for the same reason as the discharge sentinels above: a test asserts which authoring mistake was caught, not merely that one was.
All but ErrBasisScopeUnterminated apply only to a cell claiming more than one scope, that one being a malformed entry wherever it appears. A single-entry cell naming no scope parses exactly as it did before per-scope bases existed, which is why the twelve such cells in the document needed no edit (#135).
Functions ¶
func DeriveStatus ¶
DeriveStatus returns the status a proposition must carry, given its authored basis and its register rows: live is the number of rows not discharged, total the number of rows naming it at all.
The definition, in the order the tests apply it:
- A withdrawn proposition is not measured.
- Any live refutation makes it REFUTED, whatever else is cited for it. This is proof-standard rule 5: a refutation outranks any tier. The count is reported when there is more than one row, so that discharging one of several counterexamples is visible in this column rather than only in prose.
- Otherwise the authored tier decides, and a tier with no citation is not a tier.
Where the Basis cell claims more than one scope, the tier that decides is the **meet** over those scopes and the rendered status says how many scopes it is the weakest of, so that a number derived from unevenly covered routes cannot be read as a claim about the whole domain (#135). Where the scopes do not share a Subject there is no meet, and the status names the set instead of picking from it.
The function is total: every input yields a status, so no proposition can be left without one.
Types ¶
type Basis ¶
type Basis struct {
// Tier is the canonical spelling of one of the seven bases — a legacy name
// E0 through E3, or pair notation such as "exhaustive/implementation" for a
// pair that has none — or TierNone, TierWithdrawn or TierIncomparable. Pair
// decodes it.
Tier string
// Citation is whatever the Basis cell says after the tier, or for a
// multi-scope cell every entry's citation joined with "; ". For
// TierWithdrawn it names the replacement propositions.
Citation string
// Scoped holds the cell's entries when it names any scope at all, in cell
// order. Nil for a Basis built by hand and for a single-entry cell that names
// no scope, whose Tier and Citation are the whole claim.
//
// len(Scoped) > 1 is what makes Tier a reduction rather than a transcription,
// and DeriveStatus says so in the status it renders.
Scoped []ScopedBasis
}
Basis is the authored half of a proposition's status: what the cell claims, and the citation carrying the claim.
Where the cell claims one basis, Tier is it. Where the cell claims a basis per scope, Tier is what those scopes **reduce** to — the meet, per Reduce — and Scoped holds the entries the reduction was taken over. Reading Tier therefore cannot overstate, which reading "the strongest claimed" did (#135). "Strongest" was never a total order either: section 2 states the ranking convention and the pairs it ranks that the evidence does not.
type BasisKind ¶
type BasisKind struct {
Coverage Coverage
Subject Subject
// Legacy is the E0-E3 name for this pair, or empty where the pair has none.
// Three of the seven have no legacy name, which is the defect that the
// one-dimensional ladder had and this pair does not: the strongest of the
// three, exhaustive/implementation, had to be filed below a model check.
Legacy string
}
BasisKind is one of the seven bases section 2 defines: a coverage, the subject it applies to, and the legacy E-name if that pair has one.
func Bases ¶
func Bases() []BasisKind
Bases returns the seven bases, in the order section 2 tabulates them. It is a function rather than a package variable both because this package has no globals and because a caller cannot then mutate the registry the parser reads.
The count is 1 + 3*2 rather than 4*2: CoverageAsserted takes no subject, since "asserted about the implementation" and "asserted about a model" distinguish nothing measurable when nothing was executed.
func (BasisKind) Canonical ¶
Canonical returns the spelling a Basis cell normalises to: the legacy name where one exists, so that the Status column reads the same whichever spelling the author used, and the pair notation otherwise.
func (BasisKind) Rank ¶
Rank returns the position of a basis's coverage in the coverage order: asserted 0, chosen 1, sampled 2, exhaustive 3.
This is the ordering on Coverage alone, which section 2 states is total and means it. It is *not* the seven-basis sorting convention, which ranks pairs the evidence does not — Reduce refuses to compare two bases differing in Subject rather than consulting a rank for them.
type Citation ¶
type Citation struct {
LineIdx int // 0-based line index in the document
Path string // the path exactly as written
Spans [][2]int // cited line spans; "a-b" → {a,b} (inclusive), "a" → {a,a}
Symbols []string // trailing identifiers, e.g. a test name
LineSHAs []string // commit-like hex tokens on the same document line
Raw string
}
Citation is a `path:line[s] [symbol...]` reference found in the document.
func (Citation) Resolvable ¶
Resolvable reports whether the file can be located without a search — i.e. the path carries a directory. A basename-only citation (`agent.go:299`) is not resolvable here, and a bare `:299` (no path) is not matched at all; the caller counts those as the notation gap rather than checking them.
type CitationDefect ¶
CitationDefect is a resolvable citation that does not resolve.
type CitationStats ¶
type CitationStats struct {
Checked int
NotResolvable int
Defects []CitationDefect
}
CitationStats summarises a citation check: the count of citations examined, the count skipped as not machine-resolvable (the notation gap), and the defects found among the resolvable ones.
type Coverage ¶
type Coverage string
Coverage is how much of a declared domain a proposition's evidence reached. Coverage is totally ordered — asserted, chosen, sampled, exhaustive — which is why "chosen or stronger" is a well-formed phrase about coverage alone.
const ( // CoverageAsserted means nothing was executed: the property is stated in // documentation or follows from the structure of the code. CoverageAsserted Coverage = "asserted" // CoverageChosen means example tests exercised the property on inputs the // author picked, and the site the property is about ran. CoverageChosen Coverage = "chosen" // CoverageSampled means a generated run drew inputs from a declared domain. CoverageSampled Coverage = "sampled" // CoverageExhaustive means every member of a declared bounded domain ran. CoverageExhaustive Coverage = "exhaustive" )
The four coverage values defined in section 2 of the document.
type DischargeDefect ¶
type DischargeDefect struct {
// Line is the 1-indexed line of the register row.
Line int
// Tracking is the row's Tracking cell, so the reader can go to the artifact.
Tracking string
// Cell is the Discharged cell as written.
Cell string
// Err wraps ErrDischargeNoBasis or ErrDischargeNoCitation, so a caller can
// tell which of rule 11's two demands the row fails.
Err error
}
DischargeDefect describes a register row marked Discharged: Yes whose cell does not meet section 2.1 rule 11.
type Doc ¶
type Doc struct {
// contains filtered or unexported fields
}
Doc is a parsed PROPERTIES.md.
func Parse ¶
Parse reads a PROPERTIES.md and returns its propositions and register. Malformed rows are errors rather than skipped rows: a row this package cannot read is a row whose status nothing would check.
func (*Doc) CheckCitations ¶
func (d *Doc) CheckCitations(fetch LineFetcher) CitationStats
CheckCitations resolves every citation against fetch. A resolvable citation is a defect if its path does not resolve, any cited line is past end of file, or (when the citation names symbols) none of those symbols appears on any cited line. A citation that fails against the working tree is retried against each commit token on its document line before being reported, so a citation pinned to a past commit — the record of a discharged refutation — resolves against the code as it was and is not a defect. Non-resolvable citations are counted, not checked: normalising them is the notation half of the work (#105).
func (*Doc) DischargeDefects ¶
func (d *Doc) DischargeDefects() []DischargeDefect
DischargeDefects returns every register row marked Discharged: Yes that names no basis or cites no artifact, in document order — the "closed completed" case rule 11 was written against, and the near misses either side of it.
This is a report rather than a parse error, and the distinction is the whole design. Rule 11 is a policy about what a row may claim, not a statement about whether the row can be read; making a violation a parse failure would mean a document with one unjustified discharge could not be read *at all* — not by propgen, which is the tool that would regenerate its Status column, and not by a test constructing a hypothetical register to prove some other check can fail. Unknown has the same shape for the same reason. The enforcement lives where it belongs, in a CI test asserting this slice is empty, so a rule-11 violation fails the build with a message naming the row rather than aborting every reader of the document.
The predicate is checkDischargeCitation, whose doc comment states what it cannot see.
func (*Doc) Distribution ¶
Distribution returns the number of propositions carrying each derived status, with the count stripped from REFUTED so that "REFUTED (1 of 2 live)" and "REFUTED" are tallied together. The document quotes this distribution, and a quoted number that nothing derives is a number that drifts.
func (*Doc) Drifts ¶
Drifts returns every proposition whose Status cell is not what the register implies, in document order.
func (*Doc) Propositions ¶
func (d *Doc) Propositions() []*Proposition
Propositions returns the parsed section 3 rows in document order.
func (*Doc) Register ¶
func (d *Doc) Register() []Refutation
Register returns the parsed section 4 rows in document order.
func (*Doc) Render ¶
Render returns the document with every Status cell set to its derived value. Nothing else is altered: cells are rejoined as they were parsed, so a document with no drift renders byte-identically to its input.
type Drift ¶
type Drift struct {
// ID is the proposition identifier.
ID string
// Line is the 1-indexed line of the proposition's row.
Line int
// Written is the status in the file; Derived is what the register implies.
Written, Derived string
}
Drift describes one proposition whose written status disagrees with the status derived from the register.
type LineFetcher ¶
LineFetcher returns the lines of path at commit sha (empty sha = working tree) and whether it could be read. cmd/propgen supplies one backed by the working tree and `git show`; tests supply a fake.
type Proposition ¶
type Proposition struct {
// ID is the proposition identifier, such as R1, I1' or T5.
ID string
// Verdict is the result of attacking the proposition's text.
Verdict string
// Basis is the authored evidence claim.
Basis Basis
// Written is the Status cell as it appears in the file.
Written string
// contains filtered or unexported fields
}
Proposition is one row of a section 3 group table.
type Reduction ¶
type Reduction struct {
// Meet is the greatest lower bound of the covered scopes' bases. Valid only
// when Comparable; the zero BasisKind otherwise.
Meet BasisKind
// Set is every distinct basis the cell claims, in the order section 2
// tabulates them. Always populated, and it is the whole of the answer when
// Comparable is false.
Set []BasisKind
// Comparable reports whether a meet exists — that is, whether every covered
// scope whose evidence executed something shares a Subject with every other.
Comparable bool
// Scopes is the union of the declared bounds, in cell order. It is part of the
// claim, not decoration: the reduction is a floor over *these* scopes and says
// nothing about a part of the domain no entry names (§2.1 rule 2 and rule 10).
Scopes []string
}
Reduction is what a Basis cell's entries reduce to: the honest floor over the scopes the cell covers.
The reduction is a **meet** (greatest lower bound), not a max. A max over unevenly covered scopes reports the best-covered scope's strength as the proposition's, which overstates silently and is what #135 was filed about. A meet reports the weakest, which is the most that holds everywhere the cell claims to cover.
But a meet needs an order, and the seven bases do not have one: Coverage is totally ordered and Subject is not (§2.1 rule 1). So the meet exists only where all covered scopes share a Subject, and where they do not there is no single answer to report — hence Set, and hence Comparable.
func Reduce ¶
func Reduce(entries []ScopedBasis) (Reduction, bool)
Reduce returns what a set of scoped bases reduces to, and whether any entry named a basis at all.
asserted is the bottom of the coverage order and is treated as comparable with every other basis, because the incomparability of Subject arises from *what was executed* and asserted executed nothing: there is no model-versus-implementation disagreement to have. Note what this does and does not claim. It is a floor on **coverage**. It is not a claim that a `model` result outranks asserted in usefulness — section 2's ranking note says it does not, and this function does not consult that ranking.
TierNone short-circuits the whole reduction: a scope declared uncovered means nothing is established over the union, however well covered the other scopes are. That is the mechanism by which a cell can state the bound honestly instead of leaving an uncovered route to be inferred from prose.
type Refutation ¶
type Refutation struct {
// Props are the proposition IDs the counterexample breaks.
Props []string
// Capability is the adversary capability used, or H1 for none.
Capability string
// Tracking names the artifact tracking the discharge.
Tracking string
// Discharged is DischargedYes, DischargedNo or DischargedPartially.
Discharged string
// contains filtered or unexported fields
}
Refutation is one row of the section 4 register.
func (Refutation) Live ¶
func (r Refutation) Live() bool
Live reports whether the refutation is still standing. Partially discharged counts as live: a counterexample half-answered still refutes.
type ScopedBasis ¶
type ScopedBasis struct {
// Tier is the canonical spelling of one of the seven bases, or TierNone for a
// scope declared uncovered.
Tier string
// Scope is the declared bound: which part of the proposition's domain this
// entry covers. Empty only for a single-entry cell, whose scope is whatever
// the proposition's own text quantifies over.
Scope string
// Citation is the evidence for this scope.
Citation string
}
ScopedBasis is one entry of a Basis cell: a basis, the part of the proposition's domain that basis covers, and the citation carrying it.
A proposition quantifying over several execution routes is not covered equally on all of them, and one basis for the whole cell cannot say so — which is the defect this type exists to remove (#135).
type Subject ¶
type Subject string
Subject is what a proposition's evidence was about. Subject is not an ordering: a model result does not become an implementation result, with or without a faithfulness argument (section 2.1 rule 1). The pair of a coverage and a subject is therefore not totally ordered, which is the whole reason Basis records a pair rather than a rung.
const ( // SubjectNone is the subject of CoverageAsserted, which has none: where // nothing was executed there is no artifact the evidence was about. SubjectNone Subject = "" // SubjectModel means the evidence executed an abstraction of the code. SubjectModel Subject = "model" // SubjectImplementation means the evidence executed the code that ships. SubjectImplementation Subject = "implementation" )
The subject values defined in section 2 of the document.
Source Files