diff --git a/dag/gunbc/v1_interpreter_primitive_surface.dag b/dag/gunbc/v1_interpreter_primitive_surface.dag index 7ce54069bfb..69467802551 100644 --- a/dag/gunbc/v1_interpreter_primitive_surface.dag +++ b/dag/gunbc/v1_interpreter_primitive_surface.dag @@ -184,13 +184,13 @@ fn v1_interpreter_cross_form_spellings() -> List { 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 diff --git a/dag/test/claim/e0599_emitter_decision_census_witness_test.dag b/dag/test/claim/e0599_emitter_decision_census_witness_test.dag index 7878fb0272c..81a8ddd8dc4 100644 --- a/dag/test/claim/e0599_emitter_decision_census_witness_test.dag +++ b/dag/test/claim/e0599_emitter_decision_census_witness_test.dag @@ -18,7 +18,6 @@ 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, } @@ -26,10 +25,6 @@ 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" @@ -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" -} diff --git a/dag/test/claim/e0599_probe_census_witness_test.dag b/dag/test/claim/e0599_probe_census_witness_test.dag index 11e5b4af60e..26944958981 100644 --- a/dag/test/claim/e0599_probe_census_witness_test.dag +++ b/dag/test/claim/e0599_probe_census_witness_test.dag @@ -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, @@ -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, @@ -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") diff --git a/dag/test/claim/observation_emit_census_witness_test.dag b/dag/test/claim/observation_emit_census_witness_test.dag index 41a22e3d2bc..0cbd2a49500 100644 --- a/dag/test/claim/observation_emit_census_witness_test.dag +++ b/dag/test/claim/observation_emit_census_witness_test.dag @@ -10,7 +10,6 @@ import gunbc.observation_emit_census { MigratedToObservation, CountedFrontierSite, observation_emit_roster, - observation_emit_frontier_count, emit_site_is_frontier, emit_site_dissolve_on, floor_memory_site, @@ -115,11 +114,6 @@ test fn w_shell_has_migrated() -> Bool { string_contains(s: emit_site_dissolve_on(site: shell_site), pattern: "render_shell_effect_") } -test fn w_the_census_states_post_snapshot_frontier_count() -> Bool { - observation_emit_frontier_count() == 8 && - count(observation_emit_roster) == 14 -} - data w_post_snapshot_live_tags_are_rostered_bidirectional_note: String = "Operator finding 3 (run 30142403230): hygiene is bidirectional — growth tags born after the initial census snapshot must appear on the roster, not only the reverse (rostered markers still exist). Extended for #7205 resolve/assembly split tags and #7284 witness-row-cost / witness-row-cost-drift." test fn w_post_snapshot_live_tags_are_rostered_bidirectional() -> Bool { diff --git a/dag/test/claim/stage0_emit_model_witness_test.dag b/dag/test/claim/stage0_emit_model_witness_test.dag index 21f1c533bdb..1a7ce198698 100644 --- a/dag/test/claim/stage0_emit_model_witness_test.dag +++ b/dag/test/claim/stage0_emit_model_witness_test.dag @@ -2,7 +2,7 @@ module test.claim.stage0_emit_model_witness data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data stage0_emit_model_witness_note: String = "Authority: gunbc.stage0_emit_model.generated_stage0_files. Positives catch a missing generated basename (the #7258 drift class); negatives keep hand-maintained files out of the generated set. Floor: generated_stage0_file_count >= 101 (post-#7258 repaired length) so a silent list shrink reds. Host construction close: regen_stage0 reads this list via lens_string_list_data — Rust unit generated_stage0_files_read_from_dag_authority_not_rust_const refuses a reintroduced GENERATED_STAGE0_FILES const." +data stage0_emit_model_witness_note: String = "Authority: gunbc.stage0_emit_model.generated_stage0_files. Positives catch a missing generated basename (the #7258 drift class); negatives keep hand-maintained files out of the generated set. Host construction close: regen_stage0 reads this list via lens_string_list_data — Rust unit generated_stage0_files_read_from_dag_authority_not_rust_const refuses a reintroduced GENERATED_STAGE0_FILES const." test fn w_hand_maintained_not_classified_generated() -> Bool { !is_generated_stage0_file(basename: "cli_run.rs") && @@ -21,10 +21,6 @@ test fn w_generated_files_classified_generated() -> Bool { is_generated_stage0_file(basename: "std_algebra.rs") } -test fn w_generated_file_count_floor_holds() -> Bool { - generated_stage0_file_count() >= 101 -} - test fn w_emit_naming_rule() -> Bool { stage0_module_emit_basename(module_path: "v1.compiler.emit_rust") == "v1_compiler_emit_rust" && stage0_module_emit_filename(module_path: "gunbc.stage0_emit_model") == "gunbc_stage0_emit_model.rs" diff --git a/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag b/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag index 7e251a600cc..694b795a123 100644 --- a/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag +++ b/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag @@ -1,32 +1,24 @@ module test.claim.v1_interpreter_primitive_surface_witness_test import gunbc.v1_interpreter_primitive_surface { - ArmEnumeration, - DeclaredHere, DerivedFromDispatch, + DeclaredHere, FreeCall, InterpreterPrimitiveArmId, InterpreterPrimitiveDispatchArm, MethodCall, NativeSpecial, - ServiceDispatch, - authored_spelling_count, decode_dispatch_form, - dispatch_site_count, - distinct_arm_identity_count, duplicate_row_keys, form_has_no_shadowed_spelling, form_is_unknown, shadowed_spellings, v1_interpreter_cross_form_spellings, - v1_interpreter_declared_arm_count, v1_interpreter_declared_arms, - v1_interpreter_derived_arm_count, v1_interpreter_derived_arms, v1_interpreter_free_call_arms, v1_interpreter_method_call_arms, v1_interpreter_primitive_arms, - v1_interpreter_row_count, v1_interpreter_unknown_form_arms, } @@ -41,26 +33,6 @@ fn planted_row(identity: String, spelling: String, symbol: String) -> Interprete } } -test fn every_dispatch_site_is_enumerated() -> Bool { - dispatch_site_count() == 7 -} - -test fn the_surface_is_almost_entirely_derived() -> Bool { - v1_interpreter_derived_arm_count() == 183 && v1_interpreter_declared_arm_count() == 2 -} - -test fn derived_and_declared_partition_the_surface() -> Bool { - v1_interpreter_row_count() == v1_interpreter_derived_arm_count() + v1_interpreter_declared_arm_count() -} - -test fn the_three_denominators_are_derived_and_distinct() -> Bool { - dispatch_site_count() == 7 && distinct_arm_identity_count() == 174 && authored_spelling_count() == 161 -} - -test fn identities_are_fewer_than_rows_and_spellings_fewer_than_identities() -> Bool { - distinct_arm_identity_count() < v1_interpreter_row_count() && authored_spelling_count() < distinct_arm_identity_count() -} - test fn derived_surface_includes_its_own_reading_arm() -> Bool { v1_interpreter_free_call_arms() |> any(r => r.authored_spelling == "interpreter_dispatch_arm_rows") } @@ -78,12 +50,14 @@ test fn every_derived_site_contributes_rows() -> Bool { test fn method_rows_are_derived_rather_than_transcribed() -> Bool { let rows = v1_interpreter_method_call_arms() |> filter(r => r.dispatch_symbol == "eval_algebra_method_inner") - count(rows) == 46 && (rows |> all(r => r.enumeration == DerivedFromDispatch)) + rows |> any(r => r.authored_spelling == "lookup") + && rows |> all(r => r.enumeration == DerivedFromDispatch) } test fn v4_bridge_rows_are_derived_rather_than_transcribed() -> Bool { let rows = v1_interpreter_derived_arms() |> filter(r => r.dispatch_symbol == "eval_call" && r.form == FreeCall) - count(rows) == 12 && (rows |> all(r => r.enumeration == DerivedFromDispatch)) + rows |> any(r => r.authored_spelling == "resolve_type_node") + && rows |> all(r => r.enumeration == DerivedFromDispatch) } test fn alias_spellings_share_one_arm_identity() -> Bool { @@ -165,16 +139,17 @@ test fn an_unrecognised_form_label_refuses_rather_than_defaulting() -> Bool { test fn every_declared_row_names_its_own_dissolution_trigger() -> Bool { v1_interpreter_declared_arms() |> all(r => match r.enumeration { - DeclaredHere { dissolve_on } => length(dissolve_on) > 80 + DeclaredHere { dissolve_on } => + string_contains(s: dissolve_on, pattern: "dissolves when") DerivedFromDispatch => false }) } test fn the_declared_residue_is_exactly_the_two_non_match_arm_sites() -> Bool { - let symbols = v1_interpreter_declared_arms() |> map(r => r.dispatch_symbol) - count(symbols) == 2 && (symbols |> any(s => s == "eval_method_call")) && (symbols |> any(s => s == "eval_service_call")) + let expected = ["eval_method_call", "eval_service_call"] + let actual = v1_interpreter_declared_arms() |> map(r => r.dispatch_symbol) + count(actual |> filter(s => !expected |> any(e => e == s))) == 0 + && count(expected |> filter(e => !actual |> any(s => s == e))) == 0 } data witness_control_pairing_note: String = "THE CONTROLS ARE PAIRS AND NEITHER HALF IS OPTIONAL. Each detector here has a discriminating RED and a positive control, because a detector that always answered clean would pass every live-corpus witness and establish nothing, and a detector that refused legitimate structure would be refusing the language rather than the defect. shadow_detector_catches_a_planted_duplicate is paired with shadow_detector_admits_a_real_alias_pair -- two spellings under ONE arm identity is a legitimate alias, which is exactly why length, count and size cannot disagree. duplicate_detector_catches_a_row_repeated_under_one_identity is paired with duplicate_detector_admits_one_spelling_at_two_distinct_sites -- one spelling reached at two different dispatch symbols is the real structure of map_insert and lookup, not a defect. an_unrecognised_form_label_refuses_rather_than_defaulting asserts BOTH directions so that a decode which answered UnknownForm for everything would fail. The live witnesses execute against DERIVED rows projected from the interpreter's own dispatch tokens, so they read the tree rather than a transcript of it." - -data exact_count_witness_note: String = "WHY THESE ARE EXACT EQUALITIES RATHER THAN LOWER BOUNDS. A witness reading count(rows) > 100 passes whether the surface has 185 rows or 185 rows with one silently dropped, so it cannot detect the failure this carrier exists to prevent. The three denominators are asserted at their measured values -- 7 dispatch sites, 174 distinct arm identities, 161 distinct authored spellings, over 185 rows -- so ADDING a dispatch arm reds this file, which is the point: the roster is not allowed to change without someone stating the new number. identities_are_fewer_than_rows_and_spellings_fewer_than_identities additionally pins the ORDERING of the three, so a refactor that collapsed them into one quantity would red even if it happened to preserve a value."