diff --git a/dag/gunbc/scm/read_command.dag b/dag/gunbc/scm/read_command.dag new file mode 100644 index 00000000000..05778ed94ac --- /dev/null +++ b/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 + = 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` +// 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`), +// 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 { + 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 { + 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) } + } +} diff --git a/dag/gunbc/scm/repository_load.dag b/dag/gunbc/scm/repository_load.dag index 135298f11ec..ab033c53a41 100644 --- a/dag/gunbc/scm/repository_load.dag +++ b/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 } } } } } diff --git a/dag/test/claim/scm_read_command_witness_test.dag b/dag/test/claim/scm_read_command_witness_test.dag new file mode 100644 index 00000000000..6abcd148fcf --- /dev/null +++ b/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() +} diff --git a/dag/test/claim/scm_repository_load_witness_test.dag b/dag/test/claim/scm_repository_load_witness_test.dag index b29a8485d70..f84355b9f7b 100644 --- a/dag/test/claim/scm_repository_load_witness_test.dag +++ b/dag/test/claim/scm_repository_load_witness_test.dag @@ -20,6 +20,8 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import gunbc.scm.repository_load { RepositoryLoad, RepositoryLoaded, + RepositoryLoadRefused, + RepositoryLoadRefusal, RepositoryFileUnreadable, RepositoryDocumentUnparseable, RepositoryDocumentRefused, @@ -48,14 +50,16 @@ test fn scm_rl_a_well_formed_document_loads() -> Bool { test fn scm_rl_an_absent_file_is_unreadable_not_empty() -> Bool { match load_repository(path: scm_rl_absent_path) { - RepositoryFileUnreadable { path: p, error: _ } => p == scm_rl_absent_path + RepositoryLoadRefused { cause: RepositoryFileUnreadable { path: p, error: _ } } => + p == scm_rl_absent_path _ => false } } test fn scm_rl_a_truncated_document_is_unparseable() -> Bool { match load_repository(path: scm_rl_malformed_document_path) { - RepositoryDocumentUnparseable { path: p, gap: _ } => p == scm_rl_malformed_document_path + RepositoryLoadRefused { cause: RepositoryDocumentUnparseable { path: p, gap: _ } } => + p == scm_rl_malformed_document_path _ => false } } @@ -65,7 +69,7 @@ test fn scm_rl_a_truncated_document_is_unparseable() -> Bool { // bytes are damaged" rather than "this is a repository of a version I do not know". test fn scm_rl_a_parseable_non_repository_is_refused_by_schema() -> Bool { match load_repository(path: scm_rl_unknown_format_path) { - RepositoryDocumentRefused { path: p, cause: c } => + RepositoryLoadRefused { cause: RepositoryDocumentRefused { path: p, cause: c } } => p == scm_rl_unknown_format_path && match c { RepositoryFormatUnrecognized { found: f } => f == "gunbc-scm-repository-v99" diff --git a/src/v2/workflow/floor_route_gap.dag b/src/v2/workflow/floor_route_gap.dag index 1399293fcc5..571a69b5c9a 100644 --- a/src/v2/workflow/floor_route_gap.dag +++ b/src/v2/workflow/floor_route_gap.dag @@ -241,6 +241,12 @@ fn floor_route_gap_chunk_01() -> List { tail: Cons { head: "test.claim.run_verdict_exit_status_witness_test.run_success_verdict_reaches_zero_exit", tail: Cons { + head: "test.claim.scm_read_command_witness.scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer", + tail: Cons { + head: "test.claim.scm_read_command_witness.scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log", + tail: Cons { + head: "test.claim.scm_read_command_witness.scm_read_command_keystone_holds", + tail: Cons { head: "test.claim.scm_repository_load_witness.scm_rl_an_absent_file_is_unreadable_not_empty", tail: Cons { head: "test.claim.scm_repository_load_witness.scm_repository_load_keystone_holds", @@ -287,6 +293,9 @@ fn floor_route_gap_chunk_01() -> List { } } } + } + } + } } fn floor_route_gap_chunk_02() -> List {