diff --git a/src/v2/compiler/reference_conservation.dag b/src/v2/compiler/reference_conservation.dag index ef8b6c822f8..c96c063833d 100644 --- a/src/v2/compiler/reference_conservation.dag +++ b/src/v2/compiler/reference_conservation.dag @@ -120,6 +120,21 @@ fn reference_conservation_holds(report: ReferenceConservationReport) -> Bool { length(xs: report.dropped) == 0 && length(xs: report.unmeasured) == 0 } +// ACCEPTED IS A SEPARATE FACT FROM CONSERVED, AND A CONTROL THAT MEANS "THIS MODULE LOWERS" MUST ASK +// BOTH. reference_conservation_holds admits refused atoms (a located refusal accounts for what it +// covers), so on its own it cannot tell a module that lowered and kept every reference from one that +// normalization REFUSED -- the refusal stands in for restored acceptance. A module is accepted when +// nothing in it was refused and it conserved a nonzero population (a report that measured nothing +// has not been accepted, only not rejected). Every control whose subject is "lowered, and ..." reads +// these, not their parts, so no claim re-spells what acceptance is. +fn reference_conservation_accepted(report: ReferenceConservationReport) -> Bool { + (report.refused == 0) && (report.conserved > 0) +} + +fn reference_conservation_admitted(report: ReferenceConservationReport) -> Bool { + reference_conservation_holds(report: report) && reference_conservation_accepted(report: report) +} + // ---- the parse-side population ----------------------------------------------------------------- // `items` counts the top-level items entered so far; `item_names` records each item's declaring diff --git a/src/v2/compiler/reference_conservation_admission.dag b/src/v2/compiler/reference_conservation_admission.dag index 3a2574ea49e..8124244e0eb 100644 --- a/src/v2/compiler/reference_conservation_admission.dag +++ b/src/v2/compiler/reference_conservation_admission.dag @@ -68,8 +68,9 @@ import extdeps.communication.medium { Lossless, Medium } // The shapes lowering is known to lose THAT A FIXTURE NEEDS TO EXCUSE, each pinned by its own // discriminating claim in v2.test.claim.namespace_xl0.reference_conservation. Closed on purpose: a // new shape is a new pinned claim first, then a row here, and a row enters only with the fixture -// that consumes it (the block-later-statement and if-arm-argument drops are pinned there too, and -// no admitted fixture's source contains them yet). +// that consumes it (gunbc#12221 changed both shapes that were pinned there without a row here: the +// if-arm argument is now conserved, and a block's later statement now REFUSES located, so both are +// restated in that module -- as a conserved control and as a refused-not-accepted control). type KnownDropShape = NamedArgumentLabel | WhereRefinementPredicate diff --git a/src/v2/test/claim/namespace_xl0/reference_conservation_test.dag b/src/v2/test/claim/namespace_xl0/reference_conservation_test.dag index 5ca263bef00..ae199550982 100644 --- a/src/v2/test/claim/namespace_xl0/reference_conservation_test.dag +++ b/src/v2/test/claim/namespace_xl0/reference_conservation_test.dag @@ -5,6 +5,8 @@ import v2.compiler.reference_conservation { ReferenceConservationReport, ReferenceConservationSubject, dag_declared_token_classes, + reference_conservation_accepted, + reference_conservation_admitted, reference_conservation_holds, reference_conservation_of_subject, reference_conservation_subject_of_read @@ -20,8 +22,9 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import v2.std.logic { Bool } import v2.std.node { Symbol } import v2.std.text { String } -import v2.std.integer { Int } +import v2.std.integer { Int, integer_int_to_decimal_string } import extdeps.communication.medium { Lossless, Medium } +import std.process { ProcessExit, exit_failure } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -99,7 +102,7 @@ fn clean_control_report() -> ReferenceConservationReport { } test fn the_clean_control_conserves_every_authored_atom_holds() -> Bool { - reference_conservation_holds(report: clean_control_report()) + reference_conservation_admitted(report: clean_control_report()) } // The three numbers are separate and together account for the whole population: a check that @@ -119,8 +122,18 @@ test fn the_clean_control_routes_the_test_marker_to_its_channel_holds() -> Bool clean_control_report().test_marker_channel == 1 } -// ---- drop 1: the second statement of a block --------------------------------------------------- +// ---- former drop 1: the second statement of a block (now a located refusal, gunbc#12221) ------- +// MEASURED BOTH WAYS, AND THE SECOND WAY WAS HIDDEN. Before gunbc#12221 this body lowered and its +// second statement reached no reference site: one DroppedReference. #12221 made a statement followed +// by another REFUSE, located, so this module is no longer accepted. The old claim +// (the_block_second_statement_is_reported_dropped_holds) kept passing because +// reference_conservation_holds admits refused atoms: the refusal stood in for the drop. With +// reference_conservation_accepted asked, it went red (seed-interpreted at 1204ef3922, fierce-gull-556). +// Restated as what is true now: the module is refused, and neither accepted nor admitted. This is also +// the shared mutation for every "lowered, and ..." control in this file: on a refusing report the +// predicates they all ask are false, so each of them would be red. When a block's later statements +// lower, this reds and is restated as a conserved control. data block_second_statement_source: String = "module v2.test.reference_conservation_block\n\nfn rc_block() -> Int { 1 \n 2 }\n" fn block_second_statement_subject() -> ReferenceConservationSubject { @@ -131,15 +144,32 @@ fn block_second_statement_report() -> ReferenceConservationReport { conservation_report_of(subject: block_second_statement_subject()) } -test fn the_block_second_statement_is_reported_dropped_holds() -> Bool { - report_drop_count(report: block_second_statement_report(), wanted: ^dag_token_int_literal) == 1 +test fn a_block_with_a_second_statement_is_refused_not_accepted_holds() -> Bool { + let r = block_second_statement_report() + (r.refused > 0) + && !reference_conservation_accepted(report: r) + && !reference_conservation_admitted(report: r) } -// ---- drop 2: a call argument inside an if-arm -------------------------------------------------- +// A REPORT, NOT A CLAIM: the block fixture's four numbers through the process exit, so a run shows +// how the report counts a refused body. +fn block_second_statement_numbers() -> ProcessExit { + let r = block_second_statement_report() + exit_failure(reason: "authored=" + integer_int_to_decimal_string(value: r.authored) + " conserved=" + integer_int_to_decimal_string(value: r.conserved) + " locus_erased=" + integer_int_to_decimal_string(value: r.locus_erased) + " refused=" + integer_int_to_decimal_string(value: r.refused) + " dropped=" + integer_int_to_decimal_string(value: length(xs: r.dropped))) +} + +// ---- former drop 2: a call argument inside an if-arm (repaired by #12221) --------------------- -// The argument's spelling is used NOWHERE else in its declaration, so the declaration-scoped pool -// cannot account for it and the red names exactly it. -data if_arm_call_argument_source: String = "module v2.test.reference_conservation_if_arm\n\nimport v2.std.logic { Bool }\n\nfn rc_callee(probe: Bool) -> Bool { probe }\n\ndata rc_arm_arg: Bool = true\n\nfn rc_if_arm(c: Bool) -> Bool { if c { rc_callee(probe: rc_arm_arg) } else { c } }\n" +// MEASURED BOTH WAYS. Before gunbc#12221 the if-arm's call argument `rc_arm_arg` reached no reference +// site and this check reported it as exactly one DroppedReference. After #12221 (if-arms lower +// through the statement authority) the argument keeps its occurrence, and the pinned-drop claim went +// red on origin/main 53828ae4b2 (fierce-gull-556, seed-interpreted). Restated, not deleted (DESIGN +// section 4b(4)): it is now the permanent regression control that the if-arm argument is conserved. +// The argument is POSITIONAL on purpose: a named argument's label is its own, separately rostered +// drop (a_named_argument_label_is_reported_dropped_holds below), which would red this control for a +// reason that is not the if-arm. The argument's spelling is used NOWHERE else in its declaration, so +// the declaration-scoped pool cannot account for it: a regression drops it and names exactly it. +data if_arm_call_argument_source: String = "module v2.test.reference_conservation_if_arm\n\nimport v2.std.logic { Bool }\n\nfn rc_callee(probe: Bool) -> Bool { probe }\n\ndata rc_arm_arg: Bool = true\n\nfn rc_if_arm(c: Bool) -> Bool { if c { rc_callee(rc_arm_arg) } else { c } }\n" fn if_arm_call_argument_subject() -> ReferenceConservationSubject { conservation_subject(id_tail: "if_arm_call_argument", source: if_arm_call_argument_source) @@ -149,8 +179,9 @@ fn if_arm_call_argument_report() -> ReferenceConservationReport { conservation_report_of(subject: if_arm_call_argument_subject()) } -test fn the_if_arm_call_argument_is_reported_dropped_holds() -> Bool { - report_drop_count(report: if_arm_call_argument_report(), wanted: ^rc_arm_arg) == 1 +test fn the_if_arm_call_argument_is_conserved_holds() -> Bool { + let r = if_arm_call_argument_report() + reference_conservation_admitted(report: r) && report_drop_count(report: r, wanted: ^rc_arm_arg) == 0 } // ---- former drop 3: a later operand of an operator chain (repaired by #12145) ------------------ @@ -171,7 +202,7 @@ fn infix_right_operand_report() -> ReferenceConservationReport { test fn the_infix_right_operand_is_conserved_holds() -> Bool { let r = infix_right_operand_report() - reference_conservation_holds(report: r) && report_drop_count(report: r, wanted: ^rc_rhs) == 0 + reference_conservation_admitted(report: r) && report_drop_count(report: r, wanted: ^rc_rhs) == 0 } // ---- a measured drop outside the brief: the named-argument label ------------------------------ @@ -192,7 +223,7 @@ fn named_argument_label_report() -> ReferenceConservationReport { test fn a_named_argument_label_is_reported_dropped_holds() -> Bool { let r = named_argument_label_report() - report_drop_count(report: r, wanted: ^rc_label) == 1 && length(xs: r.dropped) == 1 + reference_conservation_accepted(report: r) && report_drop_count(report: r, wanted: ^rc_label) == 1 && length(xs: r.dropped) == 1 } // ---- a list-literal call argument: conserved (was a module-wide refusal) --------------------- @@ -218,8 +249,7 @@ fn list_literal_argument_report() -> ReferenceConservationReport { test fn a_list_literal_call_argument_conserves_every_element_holds() -> Bool { let r = list_literal_argument_report() - reference_conservation_holds(report: r) - && r.refused == 0 + reference_conservation_admitted(report: r) && report_drop_count(report: r, wanted: ^rc_elsewhere) == 0 && report_drop_count(report: r, wanted: ^rc_list_second) == 0 && report_drop_count(report: r, wanted: ^rc_list_callee) == 0 @@ -227,12 +257,19 @@ test fn a_list_literal_call_argument_conserves_every_element_holds() -> Bool { // ---- the multiset control: a repeated spelling, one copy dropped ------------------------------- -// `rc_rep` is spelled three times in one declaration: as the parameter binder (rebuilt into an -// edge label, so LocusErased against the pool's one label), as the first block statement (its -// occurrence survives), and as the second block statement (dropped). The pool holds one copy and -// the binder consumes it, so exactly ONE DroppedReference remains -- neither zero (a pool that -// failed to consume) nor two (a pool that was never read). -data repeated_spelling_source: String = "module v2.test.reference_conservation_repeat\n\nimport v2.std.logic { Bool }\n\nfn rc_repeat(rc_rep: Bool) -> Bool { rc_rep \n rc_rep }\n" +// `rc_rep` is spelled three times in the declaration `rc_repeat`: as its parameter binder (rebuilt +// into an edge label, so LocusErased against the pool's one label), as the named argument's LABEL at +// the call (dropped: a call lowers its arguments positionally -- the rostered NamedArgumentLabel +// shape), and as the argument's VALUE (its occurrence survives). The pool is declaration-scoped and +// holds one copy, which the binder consumes, so exactly ONE DroppedReference remains -- neither zero +// (a pool that failed to consume) nor two (a pool that was never read). `rc_callee`'s own `rc_rep` +// binder and body use sit in a different declaration and cannot feed this pool. +// RE-PINNED after gunbc#12221: the previous fixture dropped its repeated copy as the second of two +// block statements (`{ rc_rep \n rc_rep }`), and #12221 made a statement followed by another refuse +// located, so it no longer dropped one copy (red on origin/main 53828ae4b2). The multiset property is +// the subject, not the statement shape, so the fixture now drops through the one shape still +// rostered as a known drop. +data repeated_spelling_source: String = "module v2.test.reference_conservation_repeat\n\nimport v2.std.logic { Bool }\n\nfn rc_callee(rc_rep: Bool) -> Bool { rc_rep }\n\nfn rc_repeat(rc_rep: Bool) -> Bool { rc_callee(rc_rep: rc_rep) }\n" fn repeated_spelling_subject() -> ReferenceConservationSubject { conservation_subject(id_tail: "repeated_spelling", source: repeated_spelling_source) @@ -244,7 +281,7 @@ fn repeated_spelling_report() -> ReferenceConservationReport { test fn a_repeated_spelling_with_one_copy_dropped_is_exactly_one_row_holds() -> Bool { let r = repeated_spelling_report() - report_drop_count(report: r, wanted: ^rc_rep) == 1 && length(xs: r.dropped) == 1 + reference_conservation_accepted(report: r) && report_drop_count(report: r, wanted: ^rc_rep) == 1 && length(xs: r.dropped) == 1 } // ---- a measured drop found by admission: the where-refinement predicate ----------------------- @@ -262,7 +299,7 @@ fn where_refinement_predicate_subject() -> ReferenceConservationSubject { test fn the_where_refinement_predicate_is_reported_dropped_holds() -> Bool { let r = conservation_report_of(subject: where_refinement_predicate_subject()) - report_drop_count(report: r, wanted: ^rc_pred) == 1 && length(xs: r.dropped) == 1 + reference_conservation_accepted(report: r) && report_drop_count(report: r, wanted: ^rc_pred) == 1 && length(xs: r.dropped) == 1 } // ---- measured drops found by admission: a later match arm, a statement-let binder ------------- @@ -274,7 +311,8 @@ test fn the_where_refinement_predicate_is_reported_dropped_holds() -> Bool { data match_later_arm_source: String = "module v2.test.reference_conservation_match\n\ntype RcT = RcA | RcB | RcC\n\ndata rc_first: Int = 1\n\ndata rc_second: Int = 2\n\ndata rc_third: Int = 3\n\nfn rc_match(t: RcT) -> Int {\n match t {\n RcA => rc_first\n RcB => rc_second\n RcC => rc_third\n }\n}\n" test fn the_third_match_arm_is_reported_dropped_holds() -> Bool { - report_drops_identity(report: conservation_report_of(subject: match_later_arm_subject()), wanted: ^rc_third) + let r = conservation_report_of(subject: match_later_arm_subject()) + reference_conservation_accepted(report: r) && report_drops_identity(report: r, wanted: ^rc_third) } // Found the same way through v2.test.claim.body_lowering.statement_let_bind: a statement-form let's @@ -284,7 +322,7 @@ data statement_let_binder_source: String = "module v2.test.reference_conservatio test fn a_statement_let_binder_is_reported_dropped_holds() -> Bool { let r = conservation_report_of(subject: statement_let_binder_subject()) - report_drop_count(report: r, wanted: ^rc_bound) == 1 && length(xs: r.dropped) == 1 + reference_conservation_accepted(report: r) && report_drop_count(report: r, wanted: ^rc_bound) == 1 && length(xs: r.dropped) == 1 } fn match_later_arm_subject() -> ReferenceConservationSubject { @@ -309,7 +347,7 @@ fn anonymous_slots_subject() -> ReferenceConservationSubject { test fn two_anonymous_parameter_slots_are_conserved_by_minted_identity_holds() -> Bool { let r = conservation_report_of(subject: anonymous_slots_subject()) - reference_conservation_holds(report: r) + reference_conservation_admitted(report: r) && report_drop_count(report: r, wanted: symbol_intern_lexeme(lexeme: "_")) == 0 && r.authored > 0 }