Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
156 changes: 156 additions & 0 deletions dag/gunbc/scm/log.dag
Original file line number Diff line number Diff line change
@@ -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<CommitLogRow> }

type CommitLogAcc {
index: Int
rows: List<CommitLogRow>
}

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
}
})
}
}
169 changes: 169 additions & 0 deletions dag/test/claim/scm_log_witness_test.dag
Original file line number Diff line number Diff line change
@@ -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<String> {
match log {
NoCommitsYet => []
CommitLogRows { rows: rows } => map(rows, r => r.message)
}
}

fn log_witness_row_references(log: CommitLog) -> List<String> {
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())
)
}
Loading