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()) + ) +}