Skip to content
153 changes: 123 additions & 30 deletions dag/extdeps/git/worktree_enumeration.dag
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,20 @@ fn git_worktree_first_fault(attributes: GitWorktreeAttributes, reason: String) -
// admitted. The reason is git's prose for a human and carries no decidable fact this
// decoder consumes, so it is deliberately not retained -- keeping it would invent a
// second authority for a string git may reword at any release.
// EVERY SINGLETON ATTRIBUTE REFUSES ITS OWN REPETITION, all six of them, and the history of this
// function is why that is stated as a closed set rather than left to be read off the arms.
//
// HEAD refused a repeat from the start. `branch` was then given the same guard, and the four BOOLEAN
// attributes were left setting their field to true unconditionally -- so two `detached` records, or
// two `bare`, decoded into a SUCCESSFUL observation. The defect was invisible for the reason
// repetition defects usually are: setting a flag twice is idempotent, so nothing downstream looks
// wrong. It is the WIRE that was malformed, and a decoder that quietly normalizes malformed input is
// not lenient, it is answering a question nobody asked.
//
// THE ASYMMETRY WAS THE TELL, and it was introduced by a diff that stated the invariant while
// applying it to two arms of six. An unknown attribute refused loudly; a KNOWN attribute in an
// impossible arrangement was accepted quietly. When adding a seventh attribute, the guard is part of
// the arm, not a follow-up.
fn git_worktree_attribute_step(
attributes: GitWorktreeAttributes,
attribute: String,
Expand Down Expand Up @@ -111,59 +125,95 @@ fn git_worktree_attribute_step(
}
} else {
if starts_with(s: attribute, prefix: "branch ") {
GitWorktreeAttributes {
head: attributes.head,
branch: Present { value: substring(s: attribute, start: 7, end: length(attribute)) },
detached: attributes.detached,
bare: attributes.bare,
locked: attributes.locked,
prunable: attributes.prunable,
fault: attributes.fault,
match attributes.branch {
Present { value: _ } =>
git_worktree_first_fault(
attributes: attributes,
reason: "entry carries more than one branch",
)
Absent =>
GitWorktreeAttributes {
head: attributes.head,
branch: Present { value: substring(s: attribute, start: 7, end: length(attribute)) },
detached: attributes.detached,
bare: attributes.bare,
locked: attributes.locked,
prunable: attributes.prunable,
fault: attributes.fault,
}
}
} else {
if attribute == "detached" {
GitWorktreeAttributes {
head: attributes.head,
branch: attributes.branch,
detached: true,
bare: attributes.bare,
locked: attributes.locked,
prunable: attributes.prunable,
fault: attributes.fault,
}
} else {
if attribute == "bare" {
if attributes.detached {
git_worktree_first_fault(
attributes: attributes,
reason: "entry carries more than one detached",
)
} else {
GitWorktreeAttributes {
head: attributes.head,
branch: attributes.branch,
detached: attributes.detached,
bare: true,
detached: true,
bare: attributes.bare,
locked: attributes.locked,
prunable: attributes.prunable,
fault: attributes.fault,
}
} else {
if attribute == "locked" || starts_with(s: attribute, prefix: "locked ") {
}
} else {
if attribute == "bare" {
if attributes.bare {
git_worktree_first_fault(
attributes: attributes,
reason: "entry carries more than one bare",
)
} else {
GitWorktreeAttributes {
head: attributes.head,
branch: attributes.branch,
detached: attributes.detached,
bare: attributes.bare,
locked: true,
bare: true,
locked: attributes.locked,
prunable: attributes.prunable,
fault: attributes.fault,
}
} else {
if attribute == "prunable" || starts_with(s: attribute, prefix: "prunable ") {
}
} else {
if attribute == "locked" || starts_with(s: attribute, prefix: "locked ") {
if attributes.locked {
git_worktree_first_fault(
attributes: attributes,
reason: "entry carries more than one locked",
)
} else {
GitWorktreeAttributes {
head: attributes.head,
branch: attributes.branch,
detached: attributes.detached,
bare: attributes.bare,
locked: attributes.locked,
prunable: true,
locked: true,
prunable: attributes.prunable,
fault: attributes.fault,
}
}
} else {
if attribute == "prunable" || starts_with(s: attribute, prefix: "prunable ") {
if attributes.prunable {
git_worktree_first_fault(
attributes: attributes,
reason: "entry carries more than one prunable",
)
} else {
GitWorktreeAttributes {
head: attributes.head,
branch: attributes.branch,
detached: attributes.detached,
bare: attributes.bare,
locked: attributes.locked,
prunable: true,
fault: attributes.fault,
}
}
} else {
git_worktree_first_fault(
attributes: attributes,
Expand Down Expand Up @@ -394,6 +444,47 @@ fn git_worktree_scan_step(state: GitWorktreeScanState, record: String) -> GitWor
// folding the payload first would render "git refused" and "git answered" identically -- the
// execution-provenance conflation DESIGN records, where an unreached read must not inhabit the same
// carrier as a read that happened.
// EXIT ZERO WITH NO ENTRIES IS MALFORMED, NOT AN EMPTY SET, and until this refusal existed the
// decoder returned it as a SUCCESSFUL observation of zero worktrees. Git's porcelain contract lists
// the main worktree first and then the linked ones; every repository has a main worktree, a bare one
// included. So there is no repository for which git answers zero, and a zero-entry success is a
// truncated or redirected stream wearing the shape of an answer.
//
// WHY IT MATTERED MORE THAN A MISSING SET ELEMENT: a consumer comparing worktree rosters before and
// after an operation finds nothing missing from an empty before-set, so EVERY preservation check
// over it passes vacuously. The invalid observation does not produce a wrong worktree, it produces
// an unconditional yes from whatever asks about worktrees -- which is the empty-observation narrow,
// bottom-as-answer read as bottom-as-ignorance, arriving through the decoder rather than through the
// consumer.
//
// NEXT RUNG, DECLARED RATHER THAN CLAIMED. This is a REFUSAL (mechanically preventable): the invalid
// state is still representable and a check rejects it. The structural form is to split the observed
// arm into `primary: GitWorktreeIdentity` beside `linked: List<GitWorktreeIdentity>`, which makes a
// zero-worktree success unwritable rather than rejected, and additionally lets a consumer derive the
// primary from git's own roster instead of accepting a caller-supplied path. That change alters the
// type this module's consumers destructure, so it lands with the rebase that puts the convergence
// consumer on top of this module rather than in a diff that would break it across two open branches.
fn git_worktree_reject_empty_success(
observation: GitWorktreeSetObservation,
) -> GitWorktreeSetObservation {
match observation {
GitWorktreeSetReadRefused { exit_code: c, stderr: e } =>
GitWorktreeSetReadRefused { exit_code: c, stderr: e }
GitWorktreeSetUndecodable { entry_index: i, raw_entry: r, reason: n } =>
GitWorktreeSetUndecodable { entry_index: i, raw_entry: r, reason: n }
GitWorktreeSetObserved { worktrees: ws } =>
if count(ws) == 0 {
GitWorktreeSetUndecodable {
entry_index: 0,
raw_entry: "",
reason: "git exited zero and listed no worktree; every repository has a main worktree, so an empty successful enumeration is a truncated or redirected stream rather than an empty set",
}
} else {
GitWorktreeSetObserved { worktrees: ws }
}
}
}

fn git_worktree_set_observation_of(
raw: String,
exit_code: Int,
Expand All @@ -418,7 +509,9 @@ fn git_worktree_set_observation_of(
reason: "final entry is not terminated: the stream ends mid-entry",
}
} else {
git_worktree_set_observation_in_order(observation: scanned.observation)
git_worktree_set_observation_in_order(
observation: git_worktree_reject_empty_success(observation: scanned.observation),
)
}
}
}
107 changes: 107 additions & 0 deletions dag/test/claim/git_worktree_set_decoder_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -219,3 +219,110 @@ test fn nonzero_exit_refuses_the_read_and_preserves_its_cause() -> Bool {
GitWorktreeSetUndecodable { entry_index: _, raw_entry: _, reason: _ } => false
}
}

// EXIT ZERO WITH NOTHING ON STDOUT IS NOT AN EMPTY SET. Before this refusal the decoder answered
// GitWorktreeSetObserved with zero worktrees, which is not a repository git can describe -- the
// porcelain contract lists the main worktree first, and every repository has one.
//
// THE CONSEQUENCE IS WHY IT IS A REFUSAL RATHER THAN A CURIOSITY: a consumer joining worktree
// rosters before and after an operation finds nothing missing from an empty before-set, so every
// preservation check over that observation passes VACUOUSLY. The bad observation does not yield a
// wrong worktree, it yields an unconditional yes from anything that asks.
test fn an_empty_successful_enumeration_refuses_rather_than_reading_as_no_worktrees() -> Bool {
is_undecodable(observation: git_worktree_set_observation_of(raw: "", exit_code: 0, stderr: ""))
}

// THE POSITIVE CONTROL FOR IT, so the arm above cannot be satisfied by a decoder that refuses every
// successful read. A single well-formed primary entry still decodes.
test fn a_single_entry_is_not_caught_by_the_empty_success_refusal() -> Bool {
let raw = entry(attributes: [
concat("worktree ", "/opt/gunbc/gunbc"),
concat("HEAD ", "1111111111111111111111111111111111111111"),
"branch refs/heads/main",
])
count(observed_worktrees(observation: git_worktree_set_observation_of(raw: raw, exit_code: 0, stderr: ""))) == 1
}

// A REPEATED KNOWN ATTRIBUTE IS AS MALFORMED AS AN UNKNOWN ONE, and `branch` was the arm that did
// not say so: a second `branch` record silently OVERWROTE the first, so an entry naming two branches
// decoded successfully as whichever one git happened to emit last. HEAD already refused this; branch
// inherited the guard only now. The asymmetry is the tell -- an unknown attribute refused loudly
// while a known attribute in an impossible arrangement was accepted quietly.
test fn an_entry_carrying_two_branches_refuses() -> Bool {
let raw = entry(attributes: [
concat("worktree ", "/opt/gunbc/gunbc"),
concat("HEAD ", "1111111111111111111111111111111111111111"),
"branch refs/heads/main",
"branch refs/heads/other",
])
is_undecodable(observation: git_worktree_set_observation_of(raw: raw, exit_code: 0, stderr: ""))
}

// THE FOUR BOOLEAN SINGLETONS, EACH WITH ITS OWN POSITIVE CONTROL -- and the controls are the
// substance of these rows rather than politeness. A first cut of these witnesses built every fixture
// as worktree + HEAD + the doubled attribute, and three of the four then refused FOR THE WRONG
// REASON: `bare` with a HEAD is already refused by the bare-carries-no-head rule, and `locked` or
// `prunable` alone describe no checkout at all, so the entry failed the exactly-one-of check before
// duplication was ever consulted. All four went green while testing almost nothing.
//
// So each fixture below is a VALID entry that duplication alone spoils, and each is paired with the
// same entry carrying ONE occurrence, which must decode. A duplicate arm whose single-occurrence
// twin also refuses is not evidence about duplication.
test fn an_entry_carrying_two_detached_attributes_refuses() -> Bool {
let dup = entry(attributes: [
concat("worktree ", "/opt/gunbc/gunbc"),
concat("HEAD ", "1111111111111111111111111111111111111111"),
"detached",
"detached",
])
let one = entry(attributes: [
concat("worktree ", "/opt/gunbc/gunbc"),
concat("HEAD ", "1111111111111111111111111111111111111111"),
"detached",
])
is_undecodable(observation: git_worktree_set_observation_of(raw: dup, exit_code: 0, stderr: ""))
&& count(observed_worktrees(observation: git_worktree_set_observation_of(raw: one, exit_code: 0, stderr: ""))) == 1
}

test fn an_entry_carrying_two_bare_attributes_refuses() -> Bool {
let dup = entry(attributes: [concat("worktree ", "/opt/gunbc/bare"), "bare", "bare"])
let one = entry(attributes: [concat("worktree ", "/opt/gunbc/bare"), "bare"])
is_undecodable(observation: git_worktree_set_observation_of(raw: dup, exit_code: 0, stderr: ""))
&& count(observed_worktrees(observation: git_worktree_set_observation_of(raw: one, exit_code: 0, stderr: ""))) == 1
}

test fn an_entry_carrying_two_locked_attributes_refuses() -> Bool {
let dup = entry(attributes: [
concat("worktree ", "/opt/gunbc/gunbc"),
concat("HEAD ", "1111111111111111111111111111111111111111"),
"branch refs/heads/main",
"locked",
"locked",
])
let one = entry(attributes: [
concat("worktree ", "/opt/gunbc/gunbc"),
concat("HEAD ", "1111111111111111111111111111111111111111"),
"branch refs/heads/main",
"locked",
])
is_undecodable(observation: git_worktree_set_observation_of(raw: dup, exit_code: 0, stderr: ""))
&& count(observed_worktrees(observation: git_worktree_set_observation_of(raw: one, exit_code: 0, stderr: ""))) == 1
}

test fn an_entry_carrying_two_prunable_attributes_refuses() -> Bool {
let dup = entry(attributes: [
concat("worktree ", "/opt/gunbc/gunbc"),
concat("HEAD ", "1111111111111111111111111111111111111111"),
"branch refs/heads/main",
"prunable",
"prunable",
])
let one = entry(attributes: [
concat("worktree ", "/opt/gunbc/gunbc"),
concat("HEAD ", "1111111111111111111111111111111111111111"),
"branch refs/heads/main",
"prunable",
])
is_undecodable(observation: git_worktree_set_observation_of(raw: dup, exit_code: 0, stderr: ""))
&& count(observed_worktrees(observation: git_worktree_set_observation_of(raw: one, exit_code: 0, stderr: ""))) == 1
}
Loading