scm: a typed read-command result that names no destination

dag/gunbc/scm/read_command.dag

@@ -0,0 +1,121 @@
+module gunbc.scm.read_command
+
+// WHAT A READ-SIDE SCM COMMAND PRODUCES, WITH NO IDEA WHERE IT IS GOING.
+//
+// Every read verb is the same two steps: load a repository from a path, then ask it a question.
+// Both steps can fail and they fail for different reasons, so this module exists to compose them
+// ONCE rather than have each verb restate the three ways a load can refuse.
+//
+// NOTHING HERE NAMES A DESTINATION. No terminal, no stream, no exit code, no formatting. A caller
+// binds this value to whatever medium it has -- a terminal, an HTTP response, a file, a captured
+// fixture -- and that binding is the realization, kept peripheral exactly as
+// `gunbc.cli_dispatch_surface` keeps it: the surface names no realization, and the dispatch that
+// selects one is itself realization.
+//
+// THIS MODULE CHOOSES NO PHRASING. Wording, layout, ordering, plurals, colour and truncation are
+// the binding's business and none of them appear below. THE CLAIM IS ABOUT WHAT THIS MODULE
+// AUTHORS, NOT ABOUT THE WHOLE TYPE, and an earlier revision of this header stated it at the wrong
+// grain -- "there is no human-readable string in any arm", which is true of the arms declared here
+// and FALSE of `ScmReadResult` as a type, because `ScmReadRepositoryUnavailable` carries a
+// `RepositoryLoadRefusal` whose `RepositoryFileUnreadable` arm carries an `error: String` from the
+// host. That is DESIGN's total-at-the-level-examined class landing in the one sentence that was
+// supposed to be this module's mechanical test. The prose inside that refusal is a real finding
+// against `gunbc.scm.repository_load` and is filed there rather than repaired here.
+//
+import std.types { String }
+import gunbc.scm.repository_load {
+  RepositoryLoaded,
+  RepositoryLoadRefused,
+  RepositoryLoadRefusal,
+  load_repository,
+}
+import gunbc.scm.log { CommitLog, repository_log }
+import gunbc.scm.status { RepositoryStatus, repository_status }
+import gunbc.scm.merge { Proposal }
+
+// THE VERB IS A TYPE ARGUMENT, NOT AN ARM. Selecting a verb from argv is dispatch, and dispatch is
+// realization (DESIGN section 3), so a `ScmReadCommand = Log | Status` coproduct here would pull
+// the CLI's own concern into the value layer. A `ScmReadAnswer = ScmLogAnswer | ScmStatusAnswer`
+// coproduct did exactly that in an earlier revision while a header paragraph denied it: the roster
+// was not removed, it was MOVED FROM THE REQUEST TO THE RESPONSE, one arm per verb. The test that
+// this revision fixed it rather than relocating it again is mechanical -- the coproduct below names
+// no verb at all, and adding a third read verb adds no arm to any type here.
+type ScmReadResult<T>
+  = ScmReadAnswered { path: String, answer: T }
+  | ScmReadRepositoryUnavailable { cause: RepositoryLoadRefusal }
+
+// WHAT THE TYPE ARGUMENT DOES NOT BUY, MEASURED RATHER THAN ASSUMED. The reason for the generic is
+// the paragraph above -- the coproduct names no verb -- and that reason is structural, discharged by
+// the declaration itself. It is NOT a claim that the payload type is enforced here, and the
+// difference was measured rather than reasoned about. Mutation: make `scm_read_status` answer with
+// `repository_log(...)`, so a `CommitLog` sits in a declared `ScmReadResult<RepositoryStatus>`
+// position. Result: the compile produced 0 blocking errors AND no diagnostic of any severity at
+// this module's construction site. The neighbouring advisory about generic formals is real but
+// belongs to other call sites; nothing was reported against these two functions at all.
+//
+// SO THE HONEST RUNG IS mitigatable, NOT structurally guaranteed (DESIGN section 4b). A reader who
+// took the generic for a wall would be doing the rung inflation that section names as worse than
+// sitting low, because an inflated class never ranks for climbing. What the generic ACTUALLY
+// removed is a state the old shape could NAME: under `ScmReadAnswer = ScmLogAnswer | ScmStatusAnswer`
+// a log answer from the status verb was a well-typed value with an arm of its own, and here it has
+// no arm -- which is a real narrowing of what the module can SAY, independent of what the compiler
+// currently CHECKS.
+//
+// THE MECHANISM IS MEASURED, NOT GUESSED, AND THE TRIGGER IS NAMED AT ITS GRAIN. Three probes,
+// serialized, each asserting the source state it ran under: a kernel at a NON-GENERIC record field
+// REFUSES (`type mismatch: expected 'Product(RepositoryStatus)', got 'Primitive(Int)'`); an
+// UNDEFINED NAME at this module's generic `answer` field REFUSES, which proves inference reaches
+// this exact position rather than skipping it; and a kernel at that same generic field ADMITS. So
+// the judgment is REACHED and DECLINES, and it declines because the formal is the type VARIABLE
+// `T`. Declining there is CORRECT in general -- `T` can be instantiated at `Int`, so refusing a
+// kernel at an uninstantiated formal would be wrong. The gap is therefore one level up from the
+// judgment: at this construction the instantiation is fully concrete (`ScmReadResult<RepositoryStatus>`),
+// so `T` is known, and if the argument were substituted before judging, the generic field would
+// refuse for exactly the reason the non-generic one does.
+//
+// NEXT-RUNG TRIGGER: THE TYPE ARGUMENT SUBSTITUTED INTO THE FORMAL BEFORE THE INHABITANCE JUDGMENT
+// RUNS. That is the capability, stated in the words the loss is stated in -- not "a check at
+// generic positions", which is an artifact that could be built while this stayed dead. It is a
+// compiler capability and not a thing this module can construct.
+
+// THE VERDICT IS THE SHAPE. There is no `answered: Bool` and no `verdict:` field, deliberately: a
+// stored verdict is a second representation of something the arms already determine, so a value
+// could be constructed whose flag says answered and whose payload is a refusal, and nothing would
+// refuse it. Here that pair has no spelling. The construction is the one
+// `gunbc.live_deploy.spec` `deployment_step_ownership` uses, whose authority note gives the reason
+// in general form: the classification is DERIVED, never stored, so an inconsistent pair is
+// unwritable -- DESIGN section 5, construction over validation.
+//
+// AND NO `Bool` PROJECTION OVER IT IS EXPORTED. An earlier revision offered
+// `scm_read_produced_answer`, whose only consumers were the two witnesses asserting it returns true
+// and false -- an artifact with no final consumer (DESIGN section 6). `gunbc.scm.checkout` records
+// this exact helper shape being removed twice before, once as `checkout_succeeded` and once from
+// `gunbc.scm.ancestry` under review 56207, for the reason that survives here: consumers match the
+// arms, so a new arm fails to compile at every site rather than being silently absorbed into a
+// false. A binding needing both did-it-answer and did-the-intent-complete derives BOTH from the arm
+// it is in; one Bool cannot express two questions, and a second Bool would be the same mistake
+// twice.
+//
+// AN EMPTY REPOSITORY IS AN ANSWER, NOT A FAILURE. `CommitLog`'s `NoCommitsYet` sits INSIDE
+// ScmReadAnswered: a repository with no commits was read successfully and truthfully has nothing to
+// report. Filing it beside "the document was unparseable" would be the
+// not-applicable-rendered-as-malformed conflation -- opposite owners, opposite repairs, one symbol.
+
+fn scm_read_log(path: String) -> ScmReadResult<CommitLog> {
+  match load_repository(path: path) {
+    RepositoryLoadRefused { cause: cause } => ScmReadRepositoryUnavailable { cause: cause }
+    RepositoryLoaded { path: p, envelope: envelope } =>
+      ScmReadAnswered { path: p, answer: repository_log(envelope: envelope) }
+  }
+}
+
+// STATUS TAKES THE PENDING PROPOSAL AS A PARAMETER rather than reading it from somewhere, because
+// `repository_status` does: what is staged is not a fact the repository document carries, and
+// inventing a source for it here would be this module deciding a question its authority left open.
+fn scm_read_status(path: String, pending: Proposal) -> ScmReadResult<RepositoryStatus> {
+  match load_repository(path: path) {
+    RepositoryLoadRefused { cause: cause } => ScmReadRepositoryUnavailable { cause: cause }
+    RepositoryLoaded { path: p, envelope: envelope } =>
+      ScmReadAnswered { path: p, answer: repository_status(envelope: envelope, pending: pending) }
+  }
+}

dag/gunbc/scm/repository_load.dag

@@ -65,12 +65,42 @@ import gunbc.scm.repository_envelope {
   RepositoryDecodeRefusal,
 }
 
-type RepositoryLoad
-  = RepositoryLoaded { path: String, envelope: RepositoryEnvelope }
-  | RepositoryFileUnreadable { path: String, error: String }
+// THE REFUSALS ARE THEIR OWN TYPE SO A CONSUMER CAN CARRY ONE WITHOUT BEING ABLE TO HOLD A SUCCESS.
+// A layer above this -- a command surface, a serving handler -- needs to say "the repository was not
+// available, and here is which of the three owners is responsible". If that layer's arm carried a
+// whole `RepositoryLoad`, its unavailable case could be constructed holding `RepositoryLoaded`, and
+// nothing would refuse it. Splitting the refusals off makes that pair unwritable rather than merely
+// unwise, which is DESIGN section 5's construction-over-validation at the seam where the value
+// travels.
+//
+// IT ALSO MAKES THIS MODULE MATCH ITS NEIGHBOURS. `RepositoryDecodeOutcome`,
+// `RepositoryEncodeOutcome` and `CheckoutOutcome` are all `X | XRefused { cause: XRefusal }`, and a
+// fourth spelling for the same shape in the module that composes with all three would be a second
+// idiom for one concept.
+//
+// EVERY REFUSAL STILL CARRIES ITS PATH, and now it carries it INTO whatever holds it: a refusal that
+// travels to a caller without saying what it was reading is not located, and locating it at the
+// outcome instead would strip the location off exactly when the refusal leaves this module.
+type RepositoryLoadRefusal
+  = RepositoryFileUnreadable { path: String, error: String }
   | RepositoryDocumentUnparseable { path: String, gap: JsonDocumentGap }
   | RepositoryDocumentRefused { path: String, cause: RepositoryDecodeRefusal }
 
+// DERIVED, NEVER STORED. There is no `loaded: Bool` field anywhere in this module: the arm IS the
+// answer, so a value whose flag disagrees with its shape has no spelling. Same construction as
+// `gunbc.live_deploy.spec` `deployment_step_ownership`, whose authority note states the rule -- an
+// inconsistent ownership/payload pair is unwritable because ownership is projected, not recorded.
+//
+// AND NO PROJECTION OVER THE REFUSAL EITHER. Every refusal carries `path`, so a
+// `refusal -> String` accessor is authorable and was authored here and removed: with no consumer it
+// is DESIGN section 6 residue, and with one it is worse -- a fourth refusal arm would be absorbed by
+// the projection instead of failing to compile at each site that must decide about it. This exact
+// shape has now been removed three times (`checkout_succeeded`, `gunbc.scm.ancestry` under review
+// 56207, and here). Consumers match the arms.
+type RepositoryLoad
+  = RepositoryLoaded { path: String, envelope: RepositoryEnvelope }
+  | RepositoryLoadRefused { cause: RepositoryLoadRefusal }
+
 // THE ONLY HOST EFFECT IN THE READ PATH, AND IT IS FOLDED BEFORE IT IS READ. The scalar transport
 // observation -- content, success, error together -- is handed to `filesystem_read_outcome` rather
 // than projected field by field, so the arms below never see a content/success/error combination
@@ -86,17 +116,18 @@ type RepositoryLoad
 fn load_repository(path: String) -> RepositoryLoad {
   let read = Filesystem.Read(path: path)
   match filesystem_read_outcome(content: read.content, success: read.success, error: read.error) {
-    FilesystemReadRefused { error: e } => RepositoryFileUnreadable { path: path, error: e }
+    FilesystemReadRefused { error: e } =>
+      RepositoryLoadRefused { cause: RepositoryFileUnreadable { path: path, error: e } }
     FilesystemReadSucceeded { content: content } =>
       match parse_json_document(s: content) {
         JsonDocumentUnreadable { gap: gap } =>
-          RepositoryDocumentUnparseable { path: path, gap: gap }
+          RepositoryLoadRefused { cause: RepositoryDocumentUnparseable { path: path, gap: gap } }
         JsonDocumentParsed { value: v } =>
           match decode_repository(v: v) {
             RepositoryDecoded { envelope: envelope } =>
               RepositoryLoaded { path: path, envelope: envelope }
             RepositoryDecodeRefused { cause: cause } =>
-              RepositoryDocumentRefused { path: path, cause: cause }
+              RepositoryLoadRefused { cause: RepositoryDocumentRefused { path: path, cause: cause } }
           }
       }
   }

dag/test/claim/scm_read_command_witness_test.dag

@@ -0,0 +1,118 @@
+module test.claim.scm_read_command_witness
+
+// THE READ-COMMAND COMPOSITION, AND THE ONE DISTINCTION IT EXISTS TO HOLD.
+//
+// `scm_read_log` and `scm_read_status` each do two things that fail for different reasons, and the
+// claim that matters is that they stay apart at the seam where a binding will read them: a
+// repository that could not be loaded is NOT an answer, and a repository with nothing in it IS one.
+//
+// THE CENTRAL CLAIM IS scm_rc_an_empty_repository_is_an_answer_not_a_failure. It is the one that
+// would go red if someone ever decided an empty log was a degenerate failure -- the
+// not-applicable-rendered-as-malformed conflation, which has opposite owners and opposite repairs
+// on each side. Every other claim here supports it.
+//
+// NOTHING IN THIS FILE ASSERTS A RENDERING, deliberately. There is no expected string anywhere: this
+// layer produces facts and a binding decides how they read, so a claim about wording here would be
+// this file inventing the channel the module refuses to name. The one string compared below is a
+// format tag THIS FILE'S OWN FIXTURE AUTHORS, which is a controlled input rather than phrasing.
+//
+// EVERY NAME HERE WAS RE-READ AGAINST ITS BODY, because two claims in this lane were found asserting
+// more in the name than the body checked -- a disagreement no lens and no green run can see, since a
+// lens reads the body and a run reads the result and neither reads the name as a claim. Two claims
+// were repaired in opposite directions: the same-cause claim's NAME came down to what its body can
+// honestly check, and the schema-refusal claim's BODY came up to what its name always said.
+
+import std.types { Bool, String }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import gunbc.scm.authoring { empty_proposal }
+import gunbc.scm.log { NoCommitsYet }
+import gunbc.scm.repository_envelope { RepositoryFormatUnrecognized }
+import gunbc.scm.repository_load {
+  RepositoryFileUnreadable,
+  RepositoryDocumentRefused,
+}
+import gunbc.scm.read_command {
+  ScmReadAnswered,
+  ScmReadRepositoryUnavailable,
+  scm_read_log,
+  scm_read_status,
+}
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+data scm_rc_empty_repository_path: String = "dag/test/fixture/scm_repository_load/empty_repository.json"
+data scm_rc_unknown_format_path: String = "dag/test/fixture/scm_repository_load/unknown_format.json"
+data scm_rc_absent_path: String = "dag/test/fixture/scm_repository_load/this_file_is_never_created.json"
+
+// THE FORMAT TAG THE FIXTURE AUTHORS. Compared below so the schema claim proves the cause reached
+// the command layer INTACT rather than merely that some refusal did. This is a controlled fixture
+// value, not host prose: it is authored two files away in this same repository, so a claim pinned to
+// it cannot rot when a libc message changes.
+data scm_rc_unknown_format_tag: String = "gunbc-scm-repository-v99"
+
+// THE CENTRAL CLAIM. A repository that holds no commits was read successfully and truthfully has
+// nothing to report, so it must land in the ANSWERED arm carrying NoCommitsYet -- never beside a
+// load refusal. The two have opposite remedies: nothing to do, versus fix your repository.
+test fn scm_rc_an_empty_repository_is_an_answer_not_a_failure() -> Bool {
+  match scm_read_log(path: scm_rc_empty_repository_path) {
+    ScmReadAnswered { path: p, answer: NoCommitsYet } => p == scm_rc_empty_repository_path
+    _ => false
+  }
+}
+
+test fn scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer() -> Bool {
+  match scm_read_log(path: scm_rc_absent_path) {
+    ScmReadRepositoryUnavailable { cause: RepositoryFileUnreadable { path: p, error: _ } } =>
+      p == scm_rc_absent_path
+    _ => false
+  }
+}
+
+// THE LOAD REFUSAL REACHES THE COMMAND LAYER INTACT, carrying the schema's own cause rather than a
+// flattened "something went wrong". A binding that wants to distinguish a damaged document from a
+// missing one can, because nothing here collapsed them. The body descends to the FORMAT TAG: an
+// earlier revision bound `cause: _` and so proved only that some schema refusal arrived, which is
+// exactly the claim the name does not make.
+test fn scm_rc_a_schema_refusal_survives_composition_with_its_cause() -> Bool {
+  match scm_read_log(path: scm_rc_unknown_format_path) {
+    ScmReadRepositoryUnavailable {
+      cause: RepositoryDocumentRefused {
+        path: p,
+        cause: RepositoryFormatUnrecognized { found: found },
+      },
+    } => p == scm_rc_unknown_format_path && found == scm_rc_unknown_format_tag
+    _ => false
+  }
+}
+
+// BOTH VERBS REFUSE IN THE SAME ARM ON THE SAME PATH, which is what this body can honestly check and
+// now all its name claims. It does NOT establish that the two causes are equal: the arm carries a
+// host `error` string, and comparing that would pin a merge-blocking claim to a libc message, which
+// is a worse defect than the imprecision it would remove. So the name states arm and path, and the
+// error field is bound and ignored VISIBLY rather than silently.
+test fn scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log() -> Bool {
+  match scm_read_log(path: scm_rc_absent_path) {
+    ScmReadRepositoryUnavailable { cause: RepositoryFileUnreadable { path: lp, error: _ } } =>
+      match scm_read_status(path: scm_rc_absent_path, pending: empty_proposal()) {
+        ScmReadRepositoryUnavailable { cause: RepositoryFileUnreadable { path: sp, error: _ } } =>
+          lp == sp && lp == scm_rc_absent_path
+        _ => false
+      }
+    _ => false
+  }
+}
+
+test fn scm_rc_status_answers_on_a_loadable_repository() -> Bool {
+  match scm_read_status(path: scm_rc_empty_repository_path, pending: empty_proposal()) {
+    ScmReadAnswered { path: p, answer: _ } => p == scm_rc_empty_repository_path
+    _ => false
+  }
+}
+
+test fn scm_read_command_keystone_holds() -> Bool {
+  scm_rc_an_empty_repository_is_an_answer_not_a_failure() &&
+    scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer() &&
+    scm_rc_a_schema_refusal_survives_composition_with_its_cause() &&
+    scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log() &&
+    scm_rc_status_answers_on_a_loadable_repository()
+}