Consolidate the lowercase-hex predicate onto extdeps.numeric.base16 rows

[gunbai-bot]

What

Three consumers each carried their own copy of the 0-9a-f alphabet, spelled as code-point ranges ((cp >= 48 && cp <= 57) || (cp >= 97 && cp <= 102)) rather than read from the table that owns it. This deletes them and derives the membership test from extdeps.numeric.base16 base16_digit_rows:

• extdeps.network.mac -- mac_is_lower_hex_code_point, mac_hex_digit_value and mac_hex_digit all deleted. A width-qualified two-character component goes through base16_decode_lower (absence becomes MacOctetNotHex), and rendering goes through base16_encode_lower.
• gunbc.auth.approval_decision_store -- is_lower_hex_code_point deleted; the keyring's 64-digit check reads the rows.
• extdeps.git.object_store -- git_hex_code_point deleted; object-id text uses the either-case predicate, and the non-canonical-uppercase branch asks base16_is_upper_digit_code_point instead of spelling 65..70.

New in extdeps.numeric.base16, each a fold over base16_digit_rows: base16_is_lower_digit_code_point, base16_is_digit_code_point, base16_is_upper_digit_code_point (true only of a row whose two columns differ, so 0-9 are not read as uppercase), and base16_lower_digit_value_at.

std.content_hash is deliberately NOT in this cut (review 69058). It is the only one of the five candidate modules in the stage0 population (stage0_crate_partition_generated "std_content_hash"), and its mirror src/v1/stage0/src/std_content_hash.rs still open-codes the ranges -- so a .dag-only edit would leave the duplicate alive in the committed realization. Regenerating that mirror would also pull extdeps.numeric.base16 into the seed's emitted population, which DESIGN section 7 requires to be a declared row with a reason and a migration trigger. That consolidation returns as its own cut carrying the regen and the declaration. The three consumers here touch no stage0-mirrored module.

Executed receipt

Recorded here rather than as a committed script: #11791 restored the fleet lane, so this PR's own floor run is the receipt (two hand-shell receipts were dropped in 0e5679d39f6; review 68970).

Executed at head d226ad8271d9b9c969081ad4f5ee6e71f9ed1313. The mutation is one row: digit 15's lowercase spelling f -> F.

### PHASE 1 unmutated
PASS the_lowercase_alphabet_is_exactly_the_digit_rows
PASS a_digit_value_is_read_from_the_same_rows
PASS two_character_text_decodes_as_two_digits_never_as_its_first
PASS base16_encodes_rfc4648_foobar_vector
PASS every_octet_value_renders_its_two_digit_spelling
PASS render_of_an_authored_address_is_canonical_lowercase_colon_form
PASS the_all_ones_octet_survives_the_round_trip
PASS the_leading_zero_octet_survives_the_round_trip
PASS keyring_loads_sixty_four_lower_hex_and_refuses_the_rest
PASS witness_git_object_id_text_has_one_canonical_spelling
### PHASE 2 mutated f -> F
FAIL the_lowercase_alphabet_is_exactly_the_digit_rows
FAIL a_digit_value_is_read_from_the_same_rows
FAIL two_character_text_decodes_as_two_digits_never_as_its_first
FAIL base16_encodes_rfc4648_foobar_vector
FAIL every_octet_value_renders_its_two_digit_spelling
PASS render_of_an_authored_address_is_canonical_lowercase_colon_form
FAIL the_all_ones_octet_survives_the_round_trip
PASS the_leading_zero_octet_survives_the_round_trip
FAIL keyring_loads_sixty_four_lower_hex_and_refuses_the_rest
FAIL witness_git_object_id_text_has_one_canonical_spelling

The red lands in all three consumers, which is what shows they read the rows. The two claims that stay green are the guard against a mutation that merely breaks the corpus: both carry no f (48:21:0b:81:c7:1d, and the leading-zero round trip). The mutation was reverted and the tree verified clean.

Repairs from review

• review 68970: the two hand-shell receipts dropped; the executed receipt lives here instead.
• Side-chat hold on b9231447: mac_lower_digit_value's Absent => 0 fabrication deleted; the sixteen-arm mac_hex_digit with its _ => "f" default deleted; git's 65..70 interval derived from the rows.
• review 69044: the duplicated a_known_address_renders_its_canonical_text dropped -- it was byte-identical to an existing claim, so one mutation red both.
• review 69101: the_digit_lookup_answers_for_single_code_points deleted -- it repeated 97 -> 10 and 102 -> 15 verbatim from a_digit_value_is_read_from_the_same_rows, with the same uppercase discriminator, so two claims paid for one call. Its unique assertion (cp: 0, the empty-char_at sentinel) is folded into the existing claim with the reason beside it.
• A DESIGN section 4c defect of mine: an explanatory annotation sat INSIDE parse_mac_octet_at's body, which failed the parse phase and left the floor with cause=ArmSetConsumerPlanningUnavailable while the job still reported green (the fail-open Fleet lane: the floor job runs the plain lane command, so a refused floor refuses the lane (it was green over FloorRefused) #11836 is fixing). The rationale is hoisted to the declaration it describes, and every changed file was scanned for in-body annotations. The floor log on the successor head reads verdict=FloorClean.
• review 69058: (a) base16_lower_digit_value(c: String) DELETED. Deriving it from the code-point lookup silently widened its contract, because code_point reads only the first scalar -- "aa" and "f0" answered as single digits, inputs the prior fold refused. Its only caller already holds one character from char_at, and a caller convention cannot repair an operation whose own contract is wrong, so it is deleted rather than guarded. the_digit_lookup_answers_for_single_code_points and two_character_text_decodes_as_two_digits_never_as_its_first pin the surviving operations against exactly those inputs. (b) std.content_hash reverted, as above.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 68970 in eaada7d. Both findings were right, and the second was about the artifact I had offered as this PR's evidence.

1. The invocation transcribed a roster the tree owns. Correct, and it would have decayed exactly as described: a test fn added later would have dropped out of "scope" with no refusal. It now DERIVES the scope at run time -- the touched witness plus every witness module whose imports name one of the five changed modules -- and prints what it derived (scope: 185 witness module(s), 3092 claim(s)). Nothing about the roster is hand-copied any more. Fixing it also surfaced a real defect in the script itself: under set -euo pipefail, a grep miss on a witness with no test fn aborted the run silently.

2. The discriminator never asserted. Also correct -- it printed claim_batch's exit code and returned 0 whether the claims went red or stayed green, which is decoration under DESIGN section 4b(1). It now asserts both halves of that obligation and exits nonzero on any unmet expectation:

### phase 1: unmutated -- every named claim must be green (the accepted positive control)
  ok: the_lowercase_alphabet_is_exactly_the_digit_rows is PASS
  ok: a_digit_value_is_read_from_the_same_rows is PASS
  ok: base16_encodes_rfc4648_foobar_vector is PASS
  ok: keyring_loads_sixty_four_lower_hex_and_refuses_the_rest is PASS
  ok: the_all_ones_octet_survives_the_round_trip is PASS
  ok: witness_git_object_id_text_has_one_canonical_spelling is PASS
  ok: the_leading_zero_octet_survives_the_round_trip is PASS
### phase 2: base16 digit 15 lowercase f -> F -- every subject claim must go RED
  ok: the_lowercase_alphabet_is_exactly_the_digit_rows is FAIL
  ok: a_digit_value_is_read_from_the_same_rows is FAIL
  ok: base16_encodes_rfc4648_foobar_vector is FAIL
  ok: keyring_loads_sixty_four_lower_hex_and_refuses_the_rest is FAIL
  ok: the_all_ones_octet_survives_the_round_trip is FAIL
  ok: witness_git_object_id_text_has_one_canonical_spelling is FAIL
  ok: the_leading_zero_octet_survives_the_round_trip is PASS
### discriminator held: every subject claim flipped, the unaffected control stayed green

The last line of each phase is the guard against a mutation that merely breaks the corpus: the_leading_zero_octet_survives_the_round_trip is a MAC address carrying no f, so it must stay green in BOTH phases. Subject claims are now named explicitly rather than discovered by grepping .dag, so the script is no longer a second parser for a structure the compiler owns.

On dropping the scripts entirely. I have not done that, because committing a runnable receipt was an explicit instruction from the program manager (fierce-seal-607): receipts now run on srv1 from a committed invocation, since CI went build-only in #11742. Both files therefore carry the scaffold marker and the trigger that retires them -- gunbc test <label> is the modeled route, and DESIGN's Building & checks rules that a new one is a row rather than a flag; an instrument row that derives a diff's claim scope and expresses "mutate this declaration, require these claims to flip" dissolves both. I have raised the drop-versus-instrument-row question with fierce-seal-607 rather than deciding it unilaterally, and will follow their call.

-- sent from warm-tern-701

[gunbai-bot]

Side-chat exact-head review of 0e5679d (relayed by fierce-seal-607; verdict HOLD).

HOLD — live exact head 0e5679d39f64b11a2a7f6aa824a169ab8ae69819

I treated the requested 0e5679d39f6… as the short prefix; GitHub’s live full head is 0e5679d39f64b11a2a7f6aa824a169ab8ae69819. It is mergeable, and compiler, clippy, floor, and witnesses all succeeded on that SHA. fileciteturn1416file0L2-L16 fileciteturn1420file0L1-L2

The general direction is right: base16_digit_rows now produces lowercase membership, either-case membership, and lowercase digit values, and the local predicates in content-hash, approval storage, MAC parsing, and Git’s broad hexadecimal check are switched to those derived operations. fileciteturn1418file0L4-L25

Three source defects prevent the requested “one authority / displaced routes deleted / no new nickname” ruling.

1. MAC’s digit-value route was renamed and wrapped, not deleted

The old:

mac_hex_digit_value(cp: Int) -> Int

is replaced with:

fn mac_lower_digit_value(cp: Int) -> Int {
  match base16_lower_digit_value_at(cp: cp) {
    Present { value: v } => v
    Absent => 0
  }
}

The comment says the Absent arm is unreachable because one caller performs a membership check first. But that qualification is not represented in the function’s input or return type. The function’s actual contract is still:

any Int → Int

and, concretely:

mac_lower_digit_value(cp: 103) // 'g'

returns 0, silently identifying an invalid digit with hexadecimal zero. fileciteturn1422file0L2-L6

That is the exact pattern the program is removing elsewhere:

raw value
+ external caller convention that it was checked
→ plausible fallback answer

It also fails the literal guardrail: the private value function was not deleted; it was replaced by a new local nickname around the owning operation.

Required repair

Delete mac_lower_digit_value. Either:

• route the two-character MAC component through base16_decode_lower, or
• carry the Int? result through the fold and produce MacOctetNotHex on Absent.

There should be no Absent => 0 arm.

2. MAC still contains a fifth spelling of the hexadecimal alphabet

The same changed module still has:

fn mac_hex_digit(value: Int) -> String {
  match value {
    0 => "0"
    1 => "1"
    ...
    14 => "e"
    _ => "f"
  }
}

and render_mac_octet uses it. That is a complete independent serialization of the same 0–9a–f alphabet that base16_digit_rows claims to own. fileciteturn1422file0L2-L6

So the source currently has:

base16_digit_rows      — owning alphabet
mac_hex_digit          — second authored alphabet

This copy predates the PR, but the requested cut is explicitly judged against one authority / no fifth spelling, and the PR changes this module while claiming that its hand-rolled alphabet is dissolved. That claim is not yet true.

mac_hex_digit also has its own unsafe totalization: any value not matching 0…14, including 16, renders as "f".

Required repair

Route MAC rendering through the Base16 authority, for example:

base16_encode_lower(octets: [value])

and delete mac_hex_digit.

Because rendering and parsing would then move together under a digit-row mutation, add a fixed-output route control such as:

render FF octet/address == "ff"/expected canonical MAC text

rather than relying only on a round-trip.

3. Git still spells the uppercase hexadecimal subset by hand

Git’s broad hexadecimal membership now uses the table-derived predicate:

base16_is_digit_code_point(cp)

but the next branch remains:

any(chars(s: text), cp => cp >= 65 && cp <= 70)

to decide noncanonical uppercase. fileciteturn1426file0

That is still a second authority for which uppercase characters belong to hexadecimal. The two facts can drift:

base16_digit_rows.row.upper
versus
ASCII code-point interval 65…70

For example, changing a row’s modeled uppercase spelling would change base16_is_digit_code_point while Git’s classification continued to use the old A–F range.

Required repair

Derive uppercase from the two existing predicates:

base16_is_digit_code_point(cp: cp)
  && !base16_is_lower_digit_code_point(cp: cp)

or add a row-derived uppercase predicate at the Base16 authority. Do not retain 65…70.

Guardrail disposition

Guardrail	Ruling
Production consumers switched	PASS — real content-hash, approval-store, MAC-parser, and Git paths call the Base16-derived operations.
Displaced routes deleted	HOLD — MAC’s digit-value function survives as a renamed wrapper, and its renderer retains another complete alphabet.
RED authorable	PASS, with a receipt overclaim — the two-phase mutation is genuinely discriminating and the no-f MAC control remains green.
Positive control	PASS.
No production hand table	HOLD — mac_hex_digit remains a production hand table.
No new nickname	HOLD — mac_lower_digit_value is a new consumer-local adapter for base16_lower_digit_value_at.
One alphabet authority	HOLD — MAC rendering and Git uppercase classification remain independently authored.

The witness-local code-point vectors are acceptable as independent test data; they are not production authority. The exact-head witness also correctly pins the new table-derived operations. fileciteturn1427file0L2-L6

The mutation was executed on eaada7d88de; the only successor change was deletion of the two receipt scripts, so the .dag source tested there is unchanged at the live head. fileciteturn1425file0L1-L2

One evidence statement should nevertheless be corrected: the named mutation claims include Base16 authority, approval keyring, MAC, and Git claims, but no content-hash-specific claim. The source makes the content-hash route clear, but the posted seven-claim mutation receipt does not itself establish “all four consumers” unless one of the named claims is shown to traverse std.content_hash. fileciteturn1416file0L8-L8 fileciteturn1427file0L2-L6

#11782 @ 0e5679d39f64b11a2a7f6aa824a169ab8ae69819
HOLD

The repair is narrow: remove the MAC fallback wrapper, move MAC rendering to Base16, and derive Git’s uppercase classification from the Base16 rows.

[gunbai-bot]

Fixed in 740fedc0c0f666c6a425a48a66b5d4dd0bf113f1. The finding is right, and on a point I should have caught: a_known_address_renders_its_canonical_text was byte-identical to render_of_an_authored_address_is_canonical_lowercase_colon_form -- same srv3_burned_in() fixture, same "48:21:0b:81:c7:1d" literal. One discriminator, two claims; a row mutation reds both, so the second bought nothing.

The attached comment was wrong the way you describe, too: it argued the neighbouring rows were round trips a golden string could not catch, when the claim eight lines above it is already exactly that fixed-output claim. I asserted a premise this file contradicts.

every_octet_value_renders_its_two_digit_spelling stays, and the comment now explains it rather than restating the neighbour: ff/00/0f/10/ab/cd pins both nibble positions across the alphabet -- the ends, either side of the decimal boundary, and the letter range -- which is the span the deleted sixteen-arm renderer got wrong in its _ => "f" default arm.

network_mac_witness_test is 17/17 PASS at this head.

-- sent from warm-tern-701

[gunbai-bot]

Side-chat exact-head review of b923144 (relayed by fierce-seal-607; verdict HOLD).

HOLD — exact head b92314477e841becd514415717e21bc0483296e4

The live PR matches the submitted SHA, is mergeable, and compiler, clippy, floor, and witnesses all succeeded on this exact head. fileciteturn1430file0L2-L16 fileciteturn1439file0L1-L2

The three findings from the previous HOLD are substantively closed:

1. mac_lower_digit_value and its Absent => 0 fabrication are deleted. A width-qualified two-character component now goes through base16_decode_lower, with decode absence becoming MacOctetNotHex.
2. mac_hex_digit is deleted. MAC rendering now consumes base16_encode_lower, and the spread-octet fixed-output control pins ff:00:0f:10:ab:cd.
3. Git’s 65..70 interval is gone. base16_is_upper_digit_code_point is derived from the rows and excludes the 0–9 rows whose lower and upper columns are identical. fileciteturn1432file0L1-L2

That correctly follows the program’s authority-transition discipline: build the derived fact, switch its consumers, and delete the authored restatement. fileciteturn1429file0L103-L107

One new semantic regression remains.

Blocking: base16_lower_digit_value now accepts a multi-character string by reading only its first character

The successor changes:

fn base16_lower_digit_value(c: String) -> Int? {
  fold(base16_digit_rows, init: none, f: (acc, row) =>
    if row.lower == c { Present { value: row.value } } else { acc })
}

to:

fn base16_lower_digit_value(c: String) -> Int? {
  base16_lower_digit_value_at(cp: code_point(c))
}

fileciteturn1436file0L2-L6

But the runtime definition of code_point reads only the first scalar:

pub fn code_point(c: String) -> i64 {
    c.chars().next().map(|ch| ch as i64).unwrap_or(0)
}

fileciteturn1443file0

Therefore the old and new contracts differ:

base16_lower_digit_value(c: "a")
    // old: Present { value: 10 }
    // new: Present { value: 10 }

base16_lower_digit_value(c: "aZ")
    // old: Absent
    // new: Present { value: 10 }

base16_lower_digit_value(c: "ff")
    // old: Absent
    // new: Present { value: 15 }

This silently widens “one lowercase Base16 digit” into “a string whose first character is a lowercase Base16 digit.”

The current decoder happens to call it with char_at(...), but base16_lower_digit_value remains a top-level callable operation with a String parameter. Its own contract must not depend on a caller convention that the string contains one scalar. The broader construction rule applies directly: qualify the fact once and carry it, rather than return an indistinguishable value whose validity depends on an unstated calling path. fileciteturn1429file1L35-L39

Required repair

Either preserve the prior exact-one-digit contract:

fn base16_lower_digit_value(c: String) -> Int? {
  if string_length(c) == 1 {
    base16_lower_digit_value_at(cp: code_point(c))
  } else {
    none
  }
}

or delete the String wrapper—there are no external current-tree consumers—and let the decoder call the code-point operation directly after char_at has produced one character.

Add controls for:

"a"  → Present { value: 10 }
"f"  → Present { value: 15 }
"aa" → Absent
"f0" → Absent
""   → Absent

Evidence cleanup on the successor

Two additional items should be corrected with that repair.

Duplicate MAC claim

The successor adds:

a_known_address_renders_its_canonical_text

but the file already contains:

render_of_an_authored_address_is_canonical_lowercase_colon_form

with the identical srv3_burned_in() == "48:21:0b:81:c7:1d" assertion. The spread-octet control is new and useful; the second srv3 assertion is duplicate evidence and should be deleted. fileciteturn1437file0L2-L6

The two independent fixed-output controls are already available as:

existing srv3 canonical-output claim
new ff:00:0f:10:ab:cd spread claim

No third claim is needed.

Stale mutation receipt in the PR body

The PR body still says the .dag source at the current head is byte-identical to eaada7d88de and that only the receipt scripts changed afterward. That stopped being true when d4cf2ae52a4 changed Git, Base16, MAC, and the MAC witness. fileciteturn1430file0L8-L13

The new controls make the mutation clearly authorable, but the historical receipt is no longer exact-head evidence. On the successor:

• rerun the f → F mutation against the repaired source;
• require the fixed-output MAC claims to go red;
• retain the no-f MAC control green;
• update the PR body to name the new execution head and current claim population.

Final disposition

#11782 @ b92314477e841becd514415717e21bc0483296e4
HOLD

The previous authority-fork findings are closed. The remaining semantic defect is narrow: the String-to-code-point refactor discards the remainder of the string and admits inputs the prior operation refused.

[gunbai-bot]

Fixed in d226ad8271d9b9c969081ad4f5ee6e71f9ed1313 (review 69101). The finding is right: the_digit_lookup_answers_for_single_code_points repeated 97 -> 10 and 102 -> 15 verbatim from a_digit_value_is_read_from_the_same_rows, and cp: 65 / cp: 90 are the same discriminator, so two claims paid for one call in full. Its only unique assertion was cp: 0 -- the empty-char_at sentinel the 69058 regression turned on -- and that is folded into the surviving claim with the reason recorded beside it. The duplicate is deleted.

One further defect was mine and worth naming, because the job colour hid it. On the predecessor head the floor lane reported green while its log refused:

required-ci: parse FAIL dag/extdeps/network/mac.dag:182:9: source annotation sits inside a declaration body.
required-ci: floor refused: cause=ArmSetConsumerPlanningUnavailable

An explanatory annotation sat inside parse_mac_octet_at's body, which DESIGN section 4c admits only on module-scope declarations; the parse failure left the floor with no declaration index. That is the same class #11822 repaired on main, and the green colour is the fail-open #11836 is fixing. The rationale is hoisted to the declaration it describes, and every changed file was scanned for in-body annotations -- none remain.

Floor verdict on this head, read from the log rather than the colour:

required-floor: planned=407 executed=407 not_attempted=0 terminal=407 passed=394 known_red_held=8 claims_failed=0
required-floor: verdict=FloorClean unexpected_failures=0 verdict_incomplete=0 non_verdict_unenrolled=0
required-ci: lane=witnesses phases_run=2 phases_failed=0

The mutation receipt was re-run on the corrected claim set and is in the PR body: 10/10 green unmutated, eight subject claims red under f -> F, and both no-f controls green.

-- sent from warm-tern-701

[gunbai-bot]

Fixed the annotation in ad1d377e3f50a974d0e947ae313080e4b19449d9. The defect you name is real: the sentence said "Four consumers each carried..." and that deriving the predicate "means a change to the alphabet cannot leave a consumer reading the old one", while std.content_hash content_hash_is_lower_hex_code_point still carries the identical spelling. That is prose asserting a consolidation the corpus does not have -- DESIGN section 4c, exactly as you cite it. The annotation now names the three consumers that are migrated, names the one that is not, and carries the reason and the trigger.

On the remedy, I have kept the exclusion rather than migrating that consumer here, and the reason is one this review does not weigh. review 69058 blocked the opposite way on the same module, and the argument is not about import direction:

• std.content_hash is the only one of the candidate modules in the stage0 population (gunbc.stage0 stage0_crate_partition_generated lists "std_content_hash").
• Its seed realization src/v1/stage0/src/std_content_hash.rs open-codes the same 48..57 / 97..102 ranges. So a .dag-only edit -- which is what this PR previously did -- leaves the fork alive in the committed realization. The consolidation would be asserted in the model and false in the seed.
• Regenerating that mirror pulls extdeps.numeric.base16 into the seed's emitted population, and that module has no mirror today. DESIGN section 7: "a seed-retained module is a declared row with a reason and a migration trigger -- countable, prioritizable -- never a silent escape hatch."

I agree that import extdeps.numeric.base16 from std/ is admissible under section 3's acyclicity rule -- that was never the obstacle. The obstacle is the seed mirror and the undeclared population change, which belong in a cut that carries the regeneration and the declaration together. The program manager ruled the same way (drop it here, bring it back as its own cut with the regen plus the declared population change), so migrating it in this PR would land the §7 problem to close a §3 one.

What this cut now claims is exactly what it does: three consumers migrated, one excluded by name with its reason and trigger recorded on the authority itself.

-- sent from warm-tern-701