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
6 changes: 3 additions & 3 deletions dag/gunbc/v1_interpreter_primitive_surface.dag
Original file line number Diff line number Diff line change
Expand Up @@ -184,13 +184,13 @@ fn v1_interpreter_cross_form_spellings() -> List<String> {
distinct_strings(xs: cross)
}

data v1_interpreter_primitive_surface_authority_note: String = "THE V1 INTERPRETER'S PRIMITIVE DISPATCH SURFACE, MADE ENUMERABLE. Before this carrier the surface had no roster anywhere: its only authority was string match arms inside the hand-maintained seed src/v1/stage0/src/v1_interpreter.rs, so 'which primitives does the interpreter provide' was a question no consumer could ask. That is why it was the fifth surface the primitive-identity census could not read, and why v1 deletion could not be sequenced honestly: you cannot show that nothing still needs a capability you cannot enumerate.\n\nTHE SURFACE IS SEVEN DISPATCH SYMBOLS. Measured against the tree rather than assumed: eval_builtin_inner; eval_algebra_method_inner; eval_call, which carries TWO separate mechanisms -- nine guard-predicated v4 std bridge families AND a native fold intercept -- both running BEFORE the free-call dispatch, which is why fold_list and the bridge names never reach the builtin registry; try_v2_std_collection_map_primitive_grounding; try_parse_table_memo_dispatch; a lookup short-circuit inside eval_method_call; and the Filesystem.Read hermetic carve-out in eval_service_call. dispatch_site_count derives that 7 from the rows rather than restating it, so this sentence cannot drift from the roster. AN EARLIER REVISION OF THIS NOTE SAID SIX SITES and modelled eval_call as the fold intercept alone, omitting all twelve bridge spellings; the omission was caught in review, and it is recorded here rather than quietly corrected because it is the precise failure this carrier exists to prevent -- a denominator asserted from the sites someone happened to read.\n\nFIVE OF THE SEVEN SITES ARE NOW DERIVED, NOT TRANSCRIBED. eval_builtin_inner, eval_algebra_method_inner, eval_call's bridge families, eval_call's native intercept, the map grounding and the parse-table memo each expand their dispatch AND their roster row from one macro token list, so an arm without a row and a row without an arm are both unwritable rather than reconciled afterwards (DESIGN.md 5, construction over validation). No live-tree scan of Rust source is involved and none is wanted: a regex interpreting hand-written match arms would leave the denominator in Rust while adding a second thing that can be wrong.\n\nTHE RESIDUE IS CHECKABLE BY GREP, WHICH IS THE POINT. Every primitive dispatch arm in v1_interpreter.rs now carries the token form `arm \"identity\" { \"spelling\" } =>`. What remains in the file as a BARE quoted match arm is exactly 39 lines and none of it is primitive dispatch: 12 in match_pattern (pattern kinds), 5 each in map_shell_outputs, map_file_outputs and dispatch_rest, 3 each in resolve_auth and expectation_from_declared_arg, 2 each in dispatch_file and rest_tls_posture_interp_disposition, and 2 nested INSIDE arm bodies (a tree-name mapping) rather than being arms themselves. Those dispatch on HTTP methods, TLS postures, auth kinds, output channels and pattern kinds -- transport and value vocabulary, not primitive names. So 'is there an unenumerated primitive arm' is answerable by looking for a bare quoted arm outside that named list, which is a far stronger position than the line-count reconciliation an earlier revision relied on.\n\nSERVICE OPERATIONS ARE NOT ARMS, and that is a finding rather than an omission. eval_service_call resolves Service.Op against ctx.service_ops, which is built from the DECLARED .dag corpus, so that population is already enumerable as data and is deliberately outside this roster's denominator. The interpreter contributes exactly one service-name dispatch of its own -- the Filesystem.Read hermetic checkout carve-out -- plus transport realizations, which dispatch on transport and HTTP method values rather than on primitive names. Only the carve-out is a row here.\n\nROWS CARRY THE ARM'S OWN FACTS ONLY. There is deliberately no primitive-identity field, not even an optional one: an arm that joins to no known primitive must remain representable, because that population is exactly what a primitive-identity join needs to discover. A roster whose shape forbade recording an unjoined arm would be complete by construction and useless as a denominator. This carrier answers WHICH ARMS EXIST; which primitive each one realizes belongs to the join.\n\nONE ROW PER (SITE, ARM IDENTITY, SPELLING); ALIASES SHARE AN ARM IDENTITY. length, count and size are one arm under three rows, so they cannot disagree by construction. duplicate_row_keys asserts that triple is unique across the whole surface. A spelling appearing under two different arm identities at the SAME site is unreachable code, because the earlier arm always wins. A spelling appearing at two different SITES is two genuine implementations: lookup is the live specimen, dispatched both by the eval_method_call short-circuit and by the algebra arm the short-circuit shadows."
data v1_interpreter_primitive_surface_authority_note: String = "THE V1 INTERPRETER'S PRIMITIVE DISPATCH SURFACE, MADE ENUMERABLE. Before this carrier the surface had no roster anywhere: its only authority was string match arms inside the hand-maintained seed src/v1/stage0/src/v1_interpreter.rs, so 'which primitives does the interpreter provide' was a question no consumer could ask. That is why it was the fifth surface the primitive-identity census could not read, and why v1 deletion could not be sequenced honestly: you cannot show that nothing still needs a capability you cannot enumerate.\n\nTHE SURFACE IS A CLOSED SET OF DISPATCH SYMBOLS. Measured against the tree rather than assumed: eval_builtin_inner; eval_algebra_method_inner; eval_call, which carries TWO separate mechanisms -- guard-predicated v4 std bridge families AND a native fold intercept -- both running BEFORE the free-call dispatch, which is why fold_list and the bridge names never reach the builtin registry; try_v2_std_collection_map_primitive_grounding; try_parse_table_memo_dispatch; a lookup short-circuit inside eval_method_call; and the Filesystem.Read hermetic carve-out in eval_service_call. dispatch_site_count() derives the site count from the roster rather than restating it in prose. AN EARLIER REVISION UNDERCOUNTED eval_call by modelling it as the fold intercept alone, omitting the bridge spellings; the omission was caught in review, and it is recorded here rather than quietly corrected because it is the precise failure this carrier exists to prevent -- a denominator asserted from the sites someone happened to read.\n\nMOST DISPATCH SITES ARE NOW DERIVED, NOT TRANSCRIBED. eval_builtin_inner, eval_algebra_method_inner, eval_call's bridge families, eval_call's native intercept, the map grounding and the parse-table memo each expand their dispatch AND their roster row from one macro token list, so an arm without a row and a row without an arm are both unwritable rather than reconciled afterwards (DESIGN.md 5, construction over validation). No live-tree scan of Rust source is involved and none is wanted: a regex interpreting hand-written match arms would leave the denominator in Rust while adding a second thing that can be wrong.\n\nTHE RESIDUE IS CHECKABLE BY GREP, WHICH IS THE POINT. Every primitive dispatch arm in v1_interpreter.rs now carries the token form `arm \"identity\" { \"spelling\" } =>`. What remains in the file as a BARE quoted match arm is non-primitive dispatch: pattern kinds, shell/file output channels, auth kinds, TLS postures, HTTP methods, and similar transport and value vocabulary -- not primitive names. So 'is there an unenumerated primitive arm' is answerable by looking for a bare quoted arm outside that named list, which is a far stronger position than a hand-maintained line-count reconciliation.\n\nSERVICE OPERATIONS ARE NOT ARMS, and that is a finding rather than an omission. eval_service_call resolves Service.Op against ctx.service_ops, which is built from the DECLARED .dag corpus, so that population is already enumerable as data and is deliberately outside this roster's denominator. The interpreter contributes exactly one service-name dispatch of its own -- the Filesystem.Read hermetic checkout carve-out -- plus transport realizations, which dispatch on transport and HTTP method values rather than on primitive names. Only the carve-out is a row here.\n\nROWS CARRY THE ARM'S OWN FACTS ONLY. There is deliberately no primitive-identity field, not even an optional one: an arm that joins to no known primitive must remain representable, because that population is exactly what a primitive-identity join needs to discover. A roster whose shape forbade recording an unjoined arm would be complete by construction and useless as a denominator. This carrier answers WHICH ARMS EXIST; which primitive each one realizes belongs to the join.\n\nONE ROW PER (SITE, ARM IDENTITY, SPELLING); ALIASES SHARE AN ARM IDENTITY. length, count and size are one arm under three rows, so they cannot disagree by construction. duplicate_row_keys asserts that triple is unique across the whole surface. A spelling appearing under two different arm identities at the SAME site is unreachable code, because the earlier arm always wins. A spelling appearing at two different SITES is two genuine implementations: lookup is the live specimen, dispatched both by the eval_method_call short-circuit and by the algebra arm the short-circuit shadows."

data arm_accepted_shape_gap_note: String = "ARITY IS NOT DERIVABLE FROM THIS DISPATCH, and ShapeDerivability is a coproduct rather than an Int so that the gap is representable instead of guessed. Arm bodies reach for positional.first(), positional.as_slice() patterns, and byte-vector coercions, so nothing structural in the arm states how many arguments it accepts. Any number written here would be a hand transcription that rots silently the first time a body changes, which is the decorative-roster failure this carrier exists to avoid. A typed absence is countable; a fabricated arity is not. DISSOLVE-ON: the R1 step where each arm list carries an explicit parameter spec beside each body, at which point arity expands from the same tokens as the spelling and ShapeDerivedFromDispatch becomes the honest answer."

data derived_versus_declared_note: String = "WHICH ROWS ARE REAL BY CONSTRUCTION, AND WHY PROVENANCE SITS ON THE ROW RATHER THAN ON THE FORM. Enumeration provenance is a fact about how a PARTICULAR row was obtained, not about its dispatch form: MethodCall rows are derived from eval_algebra_method_inner's tokens while the MethodCall lookup short-circuit is declared, and NativeSpecial rows are derived while ServiceDispatch is declared. An earlier revision derived provenance from the form, which would have reported the short-circuit row as derived and hidden exactly the staleness the field exists to expose. So ArmEnumeration is a field, DeclaredHere carries the row's OWN dissolution trigger, and v1_interpreter_declared_arm_count counts the frontier rather than describing it.\n\nThe two declared rows are the two sites that are not match arms at all: eval_method_call's lookup short-circuit is an if-guard, and eval_service_call's Filesystem.Read carve-out dispatches on a service name. Each row states what would have to change for it to dissolve, and every_declared_row_names_its_own_dissolution_trigger executes over the rows rather than trusting this prose. Absence from a declared row is NOT evidence that an arm does not exist. The owning roadmap row is v1-interpreter-primitive-roster, and v1-interpreter-quarantine depends on it."
data derived_versus_declared_note: String = "WHICH ROWS ARE REAL BY CONSTRUCTION, AND WHY PROVENANCE SITS ON THE ROW RATHER THAN ON THE FORM. Enumeration provenance is a fact about how a PARTICULAR row was obtained, not about its dispatch form: MethodCall rows are derived from eval_algebra_method_inner's tokens while the MethodCall lookup short-circuit is declared, and NativeSpecial rows are derived while ServiceDispatch is declared. An earlier revision derived provenance from the form, which would have reported the short-circuit row as derived and hidden exactly the staleness the field exists to expose. So ArmEnumeration is a field, DeclaredHere carries the row's OWN dissolution trigger, and v1_interpreter_declared_arm_count counts the frontier rather than describing it.\n\nThe two declared rows are the two sites that are not match arms at all: eval_method_call's lookup short-circuit is an if-guard, and eval_service_call's Filesystem.Read carve-out dispatches on a service name. Each row states what would have to change for it to dissolve via its DeclaredHere dissolve_on field. Absence from a declared row is NOT evidence that an arm does not exist."

data shadowed_spelling_semantics_note: String = "WHAT form_has_no_shadowed_spelling ACTUALLY DECIDES. A spelling reached by more than one ARM IDENTITY within one dispatch site is unreachable code, because the earlier arm always wins the match. Alias spellings are deliberately NOT this: they share one arm identity, which is precisely why length, count and size cannot disagree with each other. A spelling appearing at two different SITES is a third thing again and is not a defect at all -- it is two genuine implementations of one name, which v1_interpreter_cross_form_spellings derives and a primitive-identity join must reconcile rather than assume away. Twenty spellings are in that class today; lookup, map_insert and empty_map are the load-bearing specimens. Two shadows are live and both are recorded as exact expectations rather than tolerated: the two inert-lens bridges shadow their eval_builtin_inner namesakes, and method_call_short_circuit.lookup shadows method_call.lookup. Those witnesses assert an exact set, so a NEW shadow reds this file."
data shadowed_spelling_semantics_note: String = "WHAT form_has_no_shadowed_spelling ACTUALLY DECIDES. A spelling reached by more than one ARM IDENTITY within one dispatch site is unreachable code, because the earlier arm always wins the match. Alias spellings are deliberately NOT this: they share one arm identity, which is precisely why length, count and size cannot disagree with each other. A spelling appearing at two different SITES is a third thing again and is not a defect at all -- it is two genuine implementations of one name, which v1_interpreter_cross_form_spellings derives and a primitive-identity join must reconcile rather than assume away. lookup, map_insert and empty_map are load-bearing cross-site specimens. Two shadows are live and both are recorded as exact expectations rather than tolerated: the two inert-lens bridges shadow their eval_builtin_inner namesakes, and method_call_short_circuit.lookup shadows method_call.lookup. Those witnesses assert an exact set, so a NEW shadow reds this file."

type SeedScaffoldDisposition {
scaffold: NonEmptyStr
Expand Down
10 changes: 0 additions & 10 deletions dag/test/claim/e0599_emitter_decision_census_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -18,18 +18,13 @@ import tools.e0599_emitter_decision_census {
e0599_lowering_operation_for,
e0599_lowering_operation_label,
e0599_requirement_cause_label,
e0599_lowering_row_count,
e0599_row_for_operation,
e0599_rollup_cause_labels_blob,
}
import tools.e0599_probe_census { e0599_mechanistic_root_family_labels_blob }

data e0599_emitter_decision_census_witness_note: String = "Witness for tools.e0599_emitter_decision_census: the operation selection and the operation->cause decision that docs/probes/e0599_emitter_decision_census.sh (SCAFFOLD realization) consumes over the real compilation path. Each GREEN pins one measured (method, receiver_expr) shape observed in the P-fn Phase B0 census to the lowering operation and typed cause it must select. The REDs are the load-bearing half: they hold the fail-closed arm open, so a future row that widens the classifier into a catch-all is caught. RED family 1 — an out-of-scope method (as_deref, root family R5) must NOT acquire a cause. RED family 2 — a receiver shape no lowering row names must NOT acquire a cause. RED family 3 (ROUTING, added 2026-07-29 on warm-dove-316 / calm-badger-682 review) — a tuple projection is a structurally distinct emitter shape from a named field access: v1.compiler.emit_rust emit_typed_field_access applies clone_value unconditionally in its TupleFirst, TupleSecond, and anonymous-record projection arms, while its StoredField arm gates clone_value by base_is_owned, so they differ on the ownership axis. These controls perturb the ROUTING rather than the destination: the absorbing-default control below proves the fail-closed arm CAN fire, but only a routing control proves an unclassifiable shape REACHES it. RED family 4 — the three causes must stay distinct, so a collapse of the TargetApi/OwnedDeconstruction/CloneShared split (the whole point of the B0 measurement) reds here."

test fn e0599_b0_declared_lowering_catalog_has_seven_rows() -> Bool {
e0599_lowering_row_count() == 7
}

test fn e0599_b0_freemonoid_empty_test_is_target_api() -> Bool {
e0599_lowering_operation_label(operation: e0599_lowering_operation_for(method: "is_empty", receiver_expr: "__fm")) == "FreeMonoidEmptyTest"
&& e0599_requirement_cause_label(cause: e0599_cause_for(method: "is_empty", receiver_expr: "__fm")) == "TargetApiRequirement"
Expand Down Expand Up @@ -151,8 +146,3 @@ test fn e0599_b0_red_mechanistic_scope_excludes_the_tail_families() -> Bool {
&& !string_contains(s: scope, pattern: "R5AsDerefUnit")
&& !string_contains(s: scope, pattern: "R6Other")
}

test fn e0599_b0_inhabited_operation_count_is_six_not_seven() -> Bool {
e0599_lowering_row_count() == 7
&& e0599_lowering_operation_label(operation: e0599_lowering_operation_for(method: "clone", receiver_expr: "__fm")) == "FreeMonoidCatchallBind"
}
27 changes: 0 additions & 27 deletions dag/test/claim/e0599_probe_census_witness_test.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
module test.claim.e0599_probe_census_witness_test

import std.types { list_length }
import std.error_primitives { Ok, Err }
import tools.e0599_probe_census {
MissingMethod,
Expand All @@ -11,10 +10,7 @@ import tools.e0599_probe_census {
R3ContainerCloneBounds,
R4OptionalCoproductGrounding,
R5AsDerefUnit,
e0599_canonical_seven_module_count,
e0599_canonical_seven_module_log_labels_blob,
e0599_failure_shape_from_log_shape,
e0599_message_pattern_row_count,
e0599_message_pattern_rows_blob,
e0599_root_family_for,
e0599_root_family_label_for_row,
Expand All @@ -23,29 +19,6 @@ import tools.e0599_probe_census {

data e0599_probe_census_witness_note: String = "Witness for tools.e0599_probe_census authority: pattern row census, canonical-seven roster blob, and root-family rollup used by docs/probes/e0599_census_extract.sh (SCAFFOLD realization). Aggregate path refuses unless inputs match e0599_canonical_seven_modules exactly (missing/duplicate/extra). Export boundary refuses unknown failure-shape labels (fail-closed). RED: misclassified GlobalBare or type-parameter clone tuple; drifted shape_str."

test fn e0599_probe_census_pattern_rows_complete() -> Bool {
e0599_message_pattern_row_count() == 5
}

test fn e0599_probe_census_canonical_seven_roster() -> Bool {
e0599_canonical_seven_module_count() == 7
}

test fn e0599_canonical_seven_module_log_labels_blob_line_count() -> Bool {
list_length(items: e0599_canonical_seven_module_log_labels_blob() |> split(delimiter: "\n")) == 7
}

test fn e0599_canonical_seven_module_log_labels_blob_first_is_06_translate() -> Bool {
match e0599_canonical_seven_module_log_labels_blob() |> split(delimiter: "\n") |> first {
Present { value: line } => line == "06_translate"
Absent => false
}
}

test fn e0599_message_pattern_rows_blob_line_count() -> Bool {
list_length(items: e0599_message_pattern_rows_blob() |> split(delimiter: "\n")) == 5
}

test fn e0599_message_pattern_rows_blob_first_row_is_missing_method() -> Bool {
match e0599_message_pattern_rows_blob() |> split(delimiter: "\n") |> first {
Present { value: line } => string_contains(s: line, pattern: "missing_method\t")
Expand Down
Loading
Loading