Skip to content
8 changes: 6 additions & 2 deletions dag/extdeps/git/git.dag
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,7 @@ type AdvertisedRef {

data advertised_ref_scan_note: String = "The scan REFUSES on a line it cannot read rather than skipping it, and the located line is carried so the refusal names what it choked on. Dropping unparseable lines is the shape DESIGN 5 calls the absorbing fallback: the answer would still be a well-formed ref list, so a consumer could not tell a complete advertisement from a partial one, and the deficit's frequency would be zero by construction. A partial ref list is exactly the input that makes an exact-head judgment answer `not published` about a branch that is in fact published."

data ls_remote_carries_no_exit_block_note: String = "WHY LsRemoteHeads DECLARES NO `exit` BLOCK WHILE EVERY SIBLING OPERATION DOES, which is the first thing a reader will notice. The `exit` arms are INERT AT RUN TIME - established by reading the seed, not assumed. The shell dispatch in v1_interpreter.rs maps declared output sources (`stdout`, `stderr`, `exit_success`, `exit_code`, `stdout_lines`) onto the process result and returns a record; it never consults the operation's exit arms and never raises on a nonzero exit. The only consumer of exit_props anywhere outside the parser is v1_compiler_emit_rust.rs, which round-trips them back to source so the self-host fixed point holds. So an exit arm is a declaration that is parsed, re-emitted, and never realized.\\n\\nThat makes this operation's OUTPUTS the realized authority for its outcome: a caller learns whether the read succeeded from `success`/`exit_code`/`stderr`, which are values it can match on. Adding an exit block beside them would be a second representation of the same fact where only one of the two executes - and since this operation is new, authoring one knowing it is inert would be minting a fresh declared-but-unrealized instance rather than inheriting an existing one. The corpus-wide inertness of exit blocks is a real finding and a separate correction; it is not fixed by making one operation diverge from a hundred siblings, and it is not made worse by declining to add the hundred-and-first."
data ls_remote_carries_no_exit_block_note: String = "WHY LsRemoteHeads DECLARES NO `exit` BLOCK WHILE EVERY SIBLING OPERATION DOES, which is the first thing a reader will notice. The `exit` arms are INERT AT RUN TIME - established by reading the seed, not assumed. The shell dispatch in v1_interpreter.rs maps declared output sources onto the process result and returns a record; it never consults the operation's exit arms and never raises on a nonzero exit. The only consumer of exit_props anywhere outside the parser is v1_compiler_emit_rust.rs, which round-trips them back to source so the self-host fixed point holds. So an exit arm is a declaration that is parsed, re-emitted, and never realized.\\n\\nThat makes this operation's OUTPUTS the realized authority for its outcome. This operation deliberately omits `success: Bool from exit_success` (PR #7527 census: 148 such blocks in dag/extdeps discard the exit code beside an inert exit table; LsRemoteHeads is the Lane C exemplar fix, leaving 147). Callers read `exit_code` and `exit_code_present` directly; `exit_success` is a projection that belongs in the renderer, not the declaration."

type AdvertisedRefScan
= AdvertisedRefsRead { refs: List<AdvertisedRef> }
Expand Down Expand Up @@ -584,9 +584,13 @@ service git.Core {
input { remote: String }
output {
advertised: List<String> from "stdout_lines"
success: Bool from "exit_success"
exit_code: Int from "exit_code"
stderr: String from "stderr"
stdout: Bytes from "stdout_bytes"
stderr_bytes: Bytes from "stderr_bytes"
exit_code_present: Bool from "exit_code_present"
signaled: Bool from "signaled"
signal: Int from "signal"
}
readonly
transport shell { argv: ["git", "ls-remote", "--heads", "{remote}"] }
Expand Down
257 changes: 257 additions & 0 deletions dag/extdeps/git/ls_remote_advertisement.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,257 @@
module extdeps.git.ls_remote_advertisement

import std.types { String, Int, List, NonEmptyStr, Bytes }
import extdeps.git { advertised_ref_branch_name }
import extdeps.git.object_store {
GitObjectFormat,
GitObjectFormatSha1,
GitObjectId,
GitObjectIdTextRefusal,
GitObjectIdTextDecoded,
GitObjectIdTextRefused,
git_decode_object_id_text,
}

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "git-scm.com/docs/git-ls-remote"
}
}

data ls_remote_advertisement_authority_note: String = "Typed decoder for git ls-remote ref-advertisement output. Strict line framing, validated object ids through git_decode_object_id_text, full ref identity, located malformed-line refusal, duplicate-ref refusal. Branch projection reuses extdeps.git.advertised_ref_branch_name. No cast from arbitrary text to CommitSha or NonEmptyStr — those brands are not construction-enforced in this corpus."

type GitAdvertisedRef {
object_id: GitObjectId
ref_name: NonEmptyStr
}

type GitAdvertisedRefDecodeOutcome
= GitAdvertisedRefsDecoded { refs: List<GitAdvertisedRef> }
| GitAdvertisedRefLineMalformed { line_index: Int, line: String }
| GitAdvertisedRefObjectIdRefused {
line_index: Int,
line: String,
cause: GitObjectIdTextRefusal,
}
| GitAdvertisedRefDuplicate {
ref_name: String,
first_index: Int,
second_index: Int,
}
| GitAdvertisedRefEmptyBranchProjection {
line_index: Int,
ref_name: String,
}

type GitAdvertisedRefSeen {
ref_name: String
line_index: Int
}

type GitAdvertisedRefFold {
refs: List<GitAdvertisedRef>
index: Int
seen: List<GitAdvertisedRefSeen>
failed: Bool
outcome: GitAdvertisedRefDecodeOutcome
}

type GitAdvertisedRefLineFields {
object_id_text: String
ref_name: String
field_count: Int
}

fn advertised_ref_line_field_step(acc: GitAdvertisedRefLineFields, part: String) -> GitAdvertisedRefLineFields {
if acc.field_count == 0 {
GitAdvertisedRefLineFields {
object_id_text: part,
ref_name: acc.ref_name,
field_count: 1,
}
} else if acc.field_count == 1 {
GitAdvertisedRefLineFields {
object_id_text: acc.object_id_text,
ref_name: part,
field_count: 2,
}
} else {
GitAdvertisedRefLineFields {
object_id_text: acc.object_id_text,
ref_name: acc.ref_name,
field_count: acc.field_count + 1,
}
}
}

type GitAdvertisedRefLineDecodeOutcome
= GitAdvertisedRefLineDecoded { row: GitAdvertisedRef }
| GitAdvertisedRefLineAtMalformed { line_index: Int, line: String }
| GitAdvertisedRefLineAtObjectIdRefused {
line_index: Int,
line: String,
cause: GitObjectIdTextRefusal,
}
| GitAdvertisedRefLineAtEmptyBranchProjection {
line_index: Int,
ref_name: String,
}

fn git_decode_advertised_ref_line(
line: String,
line_index: Int,
format: GitObjectFormat,
) -> GitAdvertisedRefLineDecodeOutcome {
let parts = split(s: line, delimiter: "\t")
let fields = fold(
parts,
init: GitAdvertisedRefLineFields {
object_id_text: "",
ref_name: "",
field_count: 0,
},
f: (acc, part) => advertised_ref_line_field_step(acc: acc, part: part),
)
if fields.field_count != 2 {
GitAdvertisedRefLineAtMalformed { line_index: line_index, line: line }
} else if fields.object_id_text == "" || fields.ref_name == "" {
GitAdvertisedRefLineAtMalformed { line_index: line_index, line: line }
} else if advertised_ref_branch_name(ref_name: fields.ref_name) == "" {
GitAdvertisedRefLineAtEmptyBranchProjection {
line_index: line_index,
ref_name: fields.ref_name,
}
} else {
match git_decode_object_id_text(format: format, text: fields.object_id_text) {
GitObjectIdTextRefused { cause } =>
GitAdvertisedRefLineAtObjectIdRefused {
line_index: line_index,
line: line,
cause: cause,
}
GitObjectIdTextDecoded { oid } =>
GitAdvertisedRefLineDecoded {
row: GitAdvertisedRef {
object_id: oid,
ref_name: fields.ref_name as NonEmptyStr,
},
}
}
}
}

fn git_advertised_ref_first_seen(
seen: List<GitAdvertisedRefSeen>,
ref_name: String,
) -> GitAdvertisedRefSeen? {
filter(seen, row => row.ref_name == ref_name) |> first
}

fn git_advertised_ref_step(
acc: GitAdvertisedRefFold,
line: String,
format: GitObjectFormat,
) -> GitAdvertisedRefFold {
if acc.failed {
acc
} else {
match git_decode_advertised_ref_line(line: line, line_index: acc.index, format: format) {
GitAdvertisedRefLineAtMalformed { line_index, line: bad } =>
GitAdvertisedRefFold {
refs: acc.refs,
index: acc.index + 1,
seen: acc.seen,
failed: true,
outcome: GitAdvertisedRefLineMalformed { line_index: line_index, line: bad },
}
GitAdvertisedRefLineAtObjectIdRefused { line_index, line: bad, cause } =>
GitAdvertisedRefFold {
refs: acc.refs,
index: acc.index + 1,
seen: acc.seen,
failed: true,
outcome: GitAdvertisedRefObjectIdRefused {
line_index: line_index,
line: bad,
cause: cause,
},
}
GitAdvertisedRefLineAtEmptyBranchProjection { line_index, ref_name } =>
GitAdvertisedRefFold {
refs: acc.refs,
index: acc.index + 1,
seen: acc.seen,
failed: true,
outcome: GitAdvertisedRefEmptyBranchProjection {
line_index: line_index,
ref_name: ref_name,
},
}
GitAdvertisedRefLineDecoded { row } =>
match git_advertised_ref_first_seen(seen: acc.seen, ref_name: row.ref_name as String) {
Present { value: prior } =>
GitAdvertisedRefFold {
refs: acc.refs,
index: acc.index + 1,
seen: acc.seen,
failed: true,
outcome: GitAdvertisedRefDuplicate {
ref_name: row.ref_name as String,
first_index: prior.line_index,
second_index: acc.index,
},
}
Absent =>
GitAdvertisedRefFold {
refs: acc.refs |> list_push(row),
index: acc.index + 1,
seen: acc.seen |> list_push(
GitAdvertisedRefSeen {
ref_name: row.ref_name as String,
line_index: acc.index,
},
),
failed: false,
outcome: GitAdvertisedRefsDecoded { refs: [] },
}
}
}
}
}

fn git_decode_advertised_ref_lines(
lines: List<String>,
format: GitObjectFormat,
) -> GitAdvertisedRefDecodeOutcome {
let folded = fold(
lines,
init: GitAdvertisedRefFold {
refs: [],
index: 0,
seen: [],
failed: false,
outcome: GitAdvertisedRefsDecoded { refs: [] },
},
f: (acc, line) => git_advertised_ref_step(acc: acc, line: line, format: format),
)
if folded.failed {
folded.outcome
} else {
GitAdvertisedRefsDecoded { refs: folded.refs }
}
}

fn git_decode_ls_remote_stdout_bytes(
stdout: Bytes,
format: GitObjectFormat,
) -> GitAdvertisedRefDecodeOutcome {
git_decode_ls_remote_stdout(stdout: stdout as String, format: format)
}

fn git_decode_ls_remote_stdout(stdout: String, format: GitObjectFormat) -> GitAdvertisedRefDecodeOutcome {
git_decode_advertised_ref_lines(
lines: filter(split(s: stdout, delimiter: "\n"), line => line != ""),
format: format,
)
}
7 changes: 7 additions & 0 deletions dag/gunbc/ci_layer_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -520,6 +520,12 @@ data witness_exclusion_frontier: List<WitnessExclusionRow> = [
reason: excl_install_media_reason,
dissolve_on: excl_install_media_dissolve
},
WitnessExclusionRow {
pattern: "repository_remote_head_real_execution_witness_test.dag",
classification: BinWitnessWet,
reason: excl_install_media_reason,
dissolve_on: excl_install_media_dissolve
},
WitnessExclusionRow {
pattern: "roadmap_belt_actuate_witness_test.dag",
classification: BinWitnessWet,
Expand Down Expand Up @@ -824,6 +830,7 @@ data bin_witness_wet_entries: List<ScheduleWitnessEntry> = [
bin_wet(entry: "dag/test/claim/srv3_seeded_install_media_real_execution_witness_test.dag", f: "install_media_remaster_ensure_grub_cmdline_inserts_by_real_execution"),
bin_wet(entry: "dag/test/claim/http_client_get_real_execution_witness_test.dag", f: "http_client_get_roundtrip_by_real_execution"),
bin_wet(entry: "dag/test/claim/http_client_get_real_execution_witness_test.dag", f: "http_client_get_missing_target_red_control_by_real_execution"),
bin_wet(entry: "dag/test/claim/repository_remote_head_real_execution_witness_test.dag", f: "repository_remote_head_keystone_holds_by_real_execution"),
bin_wet(entry: "dag/test/claim/host_build_cache_provision_real_execution_witness_test.dag", f: "provision_read_back_failure_not_converged_by_real_execution"),
bin_wet(entry: "dag/test/claim/host_effect_plan_real_execution_witness_test.dag", f: "host_effect_plan_shell_witness_holds_by_real_execution"),
bin_wet(entry: "dag/test/claim/effect_plan_bash_materialize_real_execution_witness_test.dag", f: "effect_plan_bash_two_declared_operations_execute"),
Expand Down
Loading
Loading