From a5207f31fefc9d6a13c15dc631c7cc3e8f98eb2b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 26 Aug 2026 03:11:20 +0000 Subject: [PATCH] scm: the log verb, and the finding that it cannot claim recency Log answers one question -- which commits this envelope carries -- as typed rows rather than text. Nothing here chooses a separator or a column order: a decision justifiable only by how output would LOOK cannot be derived from the envelope, and rendering belongs with the process-output boundary. THREE FIELDS A USER WOULD EXPECT ARE ABSENT FROM THE MODEL, reported rather than synthesised. A RepositoryCommit is { root, message } and nothing else: no AUTHOR, no TIMESTAMP, and no PARENT. There is no ancestry relation anywhere in gunbc.scm, so a repository's history is a SEQUENCE and not a graph -- every operation git states in terms of ancestry (merge-base, ahead/behind, "commits since X") has no referent here. Each would have to be invented to appear. THE ORDERING FINDING, which is stronger than the tiebreak that was anticipated. Rows come back in REFERENCE order, which is a stated basis: references ARE indices into the commit list, and the corpus already witnesses that reversing two commits changes the repository's root signature. But NOTHING IN THE MODEL ESTABLISHES THAT A LATER INDEX IS A NEWER COMMIT -- there is no commit-authoring verb, every RepositoryCommit constructed anywhere in this repository today is constructed by a witness, and no commit carries a timestamp or parent to recover an order from. Presenting rows newest-first would manufacture chronology out of position, which is the same fabrication as inventing the timestamp, one step less obvious. This is NOT a partial basis awaiting a tiebreak; the basis for recency is absent, and it becomes derivable the moment a commit verb defines it. THE REFERENCE IS DERIVED FROM POSITION, NOT BY LOOKING THE ROOT UP, and the witness for that is the one that earns its place. commit_reference_of searches by identity and answers the FIRST match, while the envelope's header states two commits may share a root and differ only in message -- they name the same program, "the point of content addressing and not a collision". Under an identity lookup both rows advertise the first row's reference and the second commit is unreachable through the identifier its own row carries. An empty history is its own state, not an empty row list: the two readings have different remedies, and DESIGN rules that collapse the empty-observation narrow, strictly worse than the widen it mirrors. Made structural, so no empty CommitLogRows value exists to confuse with NoCommitsYet. A commit naming a root the store does not hold is marked, derived from the envelope encoder's own RepositoryCommitRootNotInStore refusal -- the same reasoning behind status's CheckedOutCommitMissing arm. Receipts, by execution: six witnesses PASS. Three mutations, each turning its own witness FALSE. The sharpest: deriving the reference by identity lookup leaves the ORDINARY reference witness GREEN and is caught only by the duplicate-root one -- so that witness detects a defect the obvious test cannot see, which is why it exists. Parse sweep clean. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/scm/log.dag | 156 ++++++++++++++++++++++ dag/test/claim/scm_log_witness_test.dag | 169 ++++++++++++++++++++++++ 2 files changed, 325 insertions(+) create mode 100644 dag/gunbc/scm/log.dag create mode 100644 dag/test/claim/scm_log_witness_test.dag diff --git a/dag/gunbc/scm/log.dag b/dag/gunbc/scm/log.dag new file mode 100644 index 00000000000..3657357158e --- /dev/null +++ b/dag/gunbc/scm/log.dag @@ -0,0 +1,156 @@ +module gunbc.scm.log + +// THE LOG VERB: which commits this envelope carries. +// +// It answers exactly that one question. It is not a formatting engine: the result is a sequence of +// typed rows, and turning rows into text is a rendering concern that belongs with the process-output +// boundary. Nothing here chooses a separator, a column order or a width, because a decision that can +// only be justified by how the output would LOOK cannot be derived from the envelope, and this +// module is built entirely from what the envelope carries. +// +// WHAT THE ENVELOPE CARRIES, EXHAUSTIVELY: a RepositoryCommit is { root: ObjectId, message: String } +// and nothing else. So a log row can name the commit, name the program it points at, and carry the +// message. THREE FIELDS A USER WOULD EXPECT ARE ABSENT FROM THE MODEL, and their absence is reported +// here rather than synthesised: +// +// AUTHOR -- no commit in this layer records who made it. +// TIMESTAMP -- no commit records when. +// PARENT -- there is NO ancestry relation at all. RepositoryCommit has no parent field and +// nothing else in gunbc.scm names one, so a repository's history is a SEQUENCE and +// not a graph. Every operation git states in terms of ancestry -- merge-base, +// ahead/behind, "the commits since X" -- has no referent here. +// +// Each would have to be invented to appear in a row, and inventing them is the fabricated-plausible- +// output failure DESIGN section 5 forbids at a user-facing boundary. + +import std.types { Bool, Int, List, String } +import gunbc.scm.object_store { ObjectId, ObjectStore, store_contains } +import gunbc.scm.repository_envelope { RepositoryEnvelope, RepositoryCommit } +import gunbc.scm.commit_closure_json_v2 { position_reference } + +// WHETHER THIS COMMIT'S PROGRAM IS ACTUALLY HELD, which is decidable here and therefore reported. +// The envelope's own encoder refuses on RepositoryCommitRootNotInStore, so "this commit names a root +// the store does not contain" is a state the model already knows how to recognise. Listing such a +// commit without saying so would present a row that cannot be checked out as though it were +// ordinary -- the same reasoning that gives gunbc.scm.status its CheckedOutCommitMissing arm, and +// the same refusal it is derived from. +type LoggedCommitStanding + = LoggedCommitRootHeld + | LoggedCommitRootMissingFromStore + +// THE REFERENCE IS THE COMMIT'S IMAGE-LOCAL POSITION, spelled by the SAME authority the encoder uses +// (commit_closure_json_v2 `position_reference`). It is not a second naming scheme invented for +// display: it is the identifier a reader can hand back to any operation that takes a commit +// reference, which is what makes a log row actionable rather than decorative. +// +// IT IS DERIVED FROM POSITION DURING THE WALK, NOT BY LOOKING THE ROOT UP. `commit_reference_of` +// searches by identity and answers the FIRST match, and the envelope's own header states that two +// commits may share a root and differ only in message -- they "name the SAME program, which is the +// point of content addressing and not a collision". So an identity lookup would give both rows the +// first row's reference, and the second commit would be unreachable through the very identifier its +// row advertises. +type CommitLogRow { + reference: String + root: ObjectId + message: String + standing: LoggedCommitStanding +} + +// AN EMPTY HISTORY IS ITS OWN STATE, NOT AN EMPTY LIST. +// +// A consumer handed `[]` has to decide what it means, and the two available readings have different +// remedies: "this repository has no commits yet" is the ordinary state of a fresh repository +// (repository_envelope's header: `init` produces no commits and no root, and neither is an error), +// while "the log produced nothing" is the shape a failed or unperformed observation takes. DESIGN +// names that collapse the empty-observation narrow and rules it strictly worse than the widen it +// mirrors, because a widen is merely expensive and a narrow is silently uncovered. +// +// Making the distinction structural means no consumer can accidentally treat one as the other: +// there is no empty CommitLogRows value to confuse with NoCommitsYet, because the fresh-repository +// case has its own constructor and never produces a row list at all. +type CommitLog + = NoCommitsYet + | CommitLogRows { rows: List } + +type CommitLogAcc { + index: Int + rows: List +} + +fn logged_commit_standing(store: ObjectStore, root: ObjectId) -> LoggedCommitStanding { + if store_contains(store: store, identity: root) { + LoggedCommitRootHeld + } else { + LoggedCommitRootMissingFromStore + } +} + +fn commit_log_step(store: ObjectStore, acc: CommitLogAcc, commit: RepositoryCommit) -> CommitLogAcc { + CommitLogAcc { + index: acc.index + 1, + rows: concat( + acc.rows, + [ + CommitLogRow { + reference: position_reference(n: acc.index), + root: commit.root, + message: commit.message, + standing: logged_commit_standing(store: store, root: commit.root), + }, + ], + ), + } +} + +// ROWS COME BACK IN REFERENCE ORDER, AND THAT IS A STATED BASIS RATHER THAN AN ARTEFACT. +// +// The envelope's commit list order is load-bearing: references ARE indices into it +// (repository_envelope `commit_reference_of`), and the corpus already witnesses that reversing two +// commits changes the repository's root signature. So the order is a fact about the image, preserved +// by the codec, and reporting rows in it means a row's position and its reference agree. +// +// WHAT THIS DELIBERATELY DOES NOT CLAIM IS RECENCY, and the reason is a finding rather than a +// preference: NOTHING IN THE MODEL ESTABLISHES THAT A LATER INDEX IS A NEWER COMMIT. There is no +// commit-authoring verb -- every RepositoryCommit constructed anywhere in this repository today is +// constructed by a witness -- so no producer defines what appending means, and no commit carries a +// timestamp or a parent to recover an order from. Presenting these rows newest-first would therefore +// manufacture chronology out of position, which is the same fabrication as inventing the timestamp +// itself, one step less obvious. +// +// This is not a tiebreak waiting to be chosen. A tiebreak presumes an ordering basis that is merely +// partial; here the basis for recency is ABSENT. It becomes derivable the moment a commit verb +// exists to define it, and at that point this function gains a stated recency order rather than a +// reinterpretation of position. +fn repository_log(envelope: RepositoryEnvelope) -> CommitLog { + if count(envelope.commits) == 0 { + NoCommitsYet + } else { + match fold( + envelope.commits, + init: CommitLogAcc { index: 0, rows: [] }, + f: fn(acc, c) { commit_log_step(store: envelope.store, acc: acc, commit: c) }, + ) { + CommitLogAcc { index: _, rows: rows } => CommitLogRows { rows: rows } + } + } +} + +// Whether every logged commit names a program this repository actually holds. A consumer deciding +// whether the image is usable wants this without walking the rows itself, and it is a FACT rather +// than a rendering, so it belongs beside the log rather than in whatever eventually prints it. +fn commit_log_is_fully_held(log: CommitLog) -> Bool { + match log { + NoCommitsYet => true + CommitLogRows { rows: rows } => + fold(rows, init: true, f: fn(held, r) { + if held { + match r.standing { + LoggedCommitRootHeld => true + LoggedCommitRootMissingFromStore => false + } + } else { + false + } + }) + } +} diff --git a/dag/test/claim/scm_log_witness_test.dag b/dag/test/claim/scm_log_witness_test.dag new file mode 100644 index 00000000000..046f90cf683 --- /dev/null +++ b/dag/test/claim/scm_log_witness_test.dag @@ -0,0 +1,169 @@ +module test.claim.scm_log_witness + +import std.types { Bool, String, List } +import v2.std.node { Node, Symbol, TypeNode, Atom, node_synthetic } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.scm.object_store { + ObjectStore, + ObjectId, + empty_store, + store_node, + Stored, + LocatorCollision, +} +import gunbc.scm.repository_envelope { RepositoryEnvelope, RepositoryCommit } +import gunbc.scm.log { + repository_log, + commit_log_is_fully_held, + CommitLog, + NoCommitsYet, + CommitLogRows, + CommitLogRow, + LoggedCommitRootHeld, + LoggedCommitRootMissingFromStore, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// Names qualified: top-level definitions are corpus-wide and the resolver silently selects among +// duplicates (#8707), a hazard this layer's other witness files already document hitting. +fn log_witness_atom(name: Symbol) -> Node { + node_synthetic(kind: TypeNode { connective: Atom { identity: name } }, children: []) +} + +type LogWitnessStored { + store: ObjectStore + identity: ObjectId +} + +fn log_witness_store_one(store: ObjectStore, name: Symbol) -> LogWitnessStored { + match store_node(store: store, n: log_witness_atom(name: name)) { + Stored { store: next, identity: identity } => + LogWitnessStored { store: next, identity: identity } + LocatorCollision { identity: identity, existing: _, incoming: _ } => + LogWitnessStored { store: store, identity: identity } + } +} + +fn log_witness_two_commit_repository() -> RepositoryEnvelope { + let a = log_witness_store_one(store: empty_store(), name: ^a) + let b = log_witness_store_one(store: a.store, name: ^b) + RepositoryEnvelope { + store: b.store, + commits: [ + RepositoryCommit { root: a.identity, message: "first" }, + RepositoryCommit { root: b.identity, message: "second" }, + ], + checked_out: none, + } +} + +// A commit whose root was never stored. The envelope's encoder refuses on +// RepositoryCommitRootNotInStore, so this is a state the model already recognises. +fn log_witness_repository_with_unheld_root() -> RepositoryEnvelope { + let a = log_witness_store_one(store: empty_store(), name: ^a) + let orphan = log_witness_store_one(store: empty_store(), name: ^never_stored) + RepositoryEnvelope { + store: a.store, + commits: [ + RepositoryCommit { root: a.identity, message: "held" }, + RepositoryCommit { root: orphan.identity, message: "not held" }, + ], + checked_out: none, + } +} + +fn log_witness_row_messages(log: CommitLog) -> List { + match log { + NoCommitsYet => [] + CommitLogRows { rows: rows } => map(rows, r => r.message) + } +} + +fn log_witness_row_references(log: CommitLog) -> List { + match log { + NoCommitsYet => [] + CommitLogRows { rows: rows } => map(rows, r => r.reference) + } +} + +// AN EMPTY HISTORY IS ITS OWN STATE, asserted as NoCommitsYet rather than as "no rows". Written as a +// row-count claim this would also be satisfied by CommitLogRows { rows: [] } -- the exact collapse +// the type exists to make unrepresentable, and the empty-observation narrow DESIGN rules strictly +// worse than a widen because a narrow is silently uncovered rather than merely expensive. +test fn a_fresh_repository_logs_no_commits_yet_rather_than_no_rows() -> Bool { + match repository_log(envelope: RepositoryEnvelope { + store: empty_store(), + commits: [], + checked_out: none, + }) { + NoCommitsYet => true + CommitLogRows { rows: _ } => false + } +} + +// THE POSITIVE CONTROL FOR THE ABOVE, and without it answering NoCommitsYet for everything would +// pass: a repository that HAS commits must produce rows carrying their messages. +test fn a_repository_with_commits_logs_a_row_per_commit() -> Bool { + log_witness_row_messages(log: repository_log(envelope: log_witness_two_commit_repository())) + == ["first", "second"] +} + +// ROWS COME BACK IN REFERENCE ORDER, AND ROW POSITION AGREES WITH THE REFERENCE IT ADVERTISES. This +// is the claim that makes a row actionable: the reference is the identifier a reader hands back to +// an operation that takes one, so a row whose reference did not match its position would send that +// reader to a different commit. +test fn row_references_are_positional_and_agree_with_row_order() -> Bool { + log_witness_row_references(log: repository_log(envelope: log_witness_two_commit_repository())) + == ["0", "1"] +} + +// THE DUPLICATE-ROOT CASE, WHICH IS WHY THE REFERENCE IS DERIVED FROM POSITION RATHER THAN BY +// LOOKING THE ROOT UP. repository_envelope's header states that two commits may share a root and +// differ only in message -- they name the same program, "which is the point of content addressing +// and not a collision". An identity lookup answers the FIRST match, so both rows would advertise the +// first row's reference and the second commit would be unreachable through the identifier its own +// row carries. +test fn two_commits_sharing_a_root_still_get_distinct_references() -> Bool { + let a = log_witness_store_one(store: empty_store(), name: ^shared) + let repo = RepositoryEnvelope { + store: a.store, + commits: [ + RepositoryCommit { root: a.identity, message: "relabelled once" }, + RepositoryCommit { root: a.identity, message: "relabelled twice" }, + ], + checked_out: none, + } + log_witness_row_references(log: repository_log(envelope: repo)) == ["0", "1"] + && log_witness_row_messages(log: repository_log(envelope: repo)) + == ["relabelled once", "relabelled twice"] +} + +// A COMMIT NAMING A ROOT THE STORE DOES NOT HOLD IS MARKED, not listed as ordinary. Listing it +// silently would present a row that cannot be checked out as though it were fine -- the same +// reasoning that gives status its CheckedOutCommitMissing arm. +test fn a_commit_whose_root_is_not_held_is_marked_rather_than_listed_as_ordinary() -> Bool { + match repository_log(envelope: log_witness_repository_with_unheld_root()) { + NoCommitsYet => false + CommitLogRows { rows: rows } => + map(rows, r => match r.standing { + LoggedCommitRootHeld => "held" + LoggedCommitRootMissingFromStore => "missing" + }) == ["held", "missing"] + } +} + +// THE ROLL-UP, WITH ITS DISCRIMINATOR. A fully-held repository and a fresh one both answer true, and +// a repository with one unheld root answers false -- so the predicate distinguishes the state it +// names rather than tracking whether any rows exist. +test fn fully_held_distinguishes_an_unheld_root_from_a_healthy_or_empty_log() -> Bool { + commit_log_is_fully_held(log: repository_log(envelope: log_witness_two_commit_repository())) + && commit_log_is_fully_held(log: repository_log(envelope: RepositoryEnvelope { + store: empty_store(), + commits: [], + checked_out: none, + })) + && !commit_log_is_fully_held( + log: repository_log(envelope: log_witness_repository_with_unheld_root()) + ) +}