Skip to content
Closed
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
337 changes: 337 additions & 0 deletions dag/gunbc/emit_copy_qualification.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,337 @@
module gunbc.emit_copy_qualification

import std.types { Bool, List, NonEmptyStr, String }

// WHY THIS MODULE EXISTS, in one sentence: the production Rust emitter decides at every value use
// site whether to copy or to share, and nothing in the corpus could say what a given copy COSTS or
// whether it was NEEDED -- two different questions that a single ".clone() is present" observation
// silently conflates.
//
// The two axes are independent and neither implies the other. A clone that is load-bearing may
// still be free (the receiver was realized Rc<T>, so the copy is a refcount increment). A clone
// that is redundant may still be free for the same reason. And a clone that is redundant on a bare
// aggregate is the one cell that is an actual cost defect. Reading only clone presence collapses a
// 2-axis space onto one bit, and the bit that survives is the one that does not decide anything.
//
// DISJOINT FROM THE CARRIER-COST VOCABULARY, stated because the names are near neighbours and a
// silent fork here would be exactly DESIGN section 3's failure. std.primitives
// CarrierCostSensitivity and v2.std.value_carrier CarrierCost describe the asymptotics of a
// PERSISTENT COLLECTION CARRIER -- the update and lookup work of a hash-array-mapped trie against a
// relaxed-radix-balanced tree. This module describes what one COPY OF ONE VALUE costs once the Rust
// emitter has chosen a realization for it. Different subject, different authority; a FreeMonoid's
// lookup work is not a fact about what cloning a handle to it costs.
//
// SUBJECT, named so this vocabulary is not read as covering more than it does. The production
// source->Rust-emission path is the v1 seed emitter (v1.compiler.emit_rust), which is what
// `gunbc compile --target rust` reaches end to end; the R1 census in
// docs/plans/rc-ownership-wrap-decision-design.md establishes that the v2 wrap_decision_gate is not
// compiled into the binary and was dormant while the measured sites were produced. v2's
// v2.compiler.use_site_verdict UseSiteVerdict is a DIFFERENT path and is not qualified here.

// What one copy costs once the emitter has realized the receiver. Grounded in the realization the
// emitter actually chose, not in the authored type: the same authored type reaches Rc<T> at one
// occurrence and bare at another (the fourteen bare field occurrences R1 measured), so the cost is
// a property of the occurrence's realization and cannot be read off the declaration.
type CopyRealizationCost
= ShareHandleBump { realization: NonEmptyStr }
| DeepAggregateCopy { realization: NonEmptyStr }
| MachineWordCopy { realization: NonEmptyStr }
| CopyRealizationUnobserved

// Whether an emitted copy was needed. CloneEmittedUndecidable is the axis's load-bearing arm and
// not a catch-all: where the receiver is Copy-eligible, rustc performs an implicit bitwise copy
// whether or not the clone is written, so DELETING THE CLONE COMPILES EITHER WAY and the removal
// experiment returns the same answer for a required and a redundant clone. That is a property of
// the experiment, not of the emitter -- the question is genuinely not decidable by that instrument,
// and answering it anyway would be the fabricated plausible output DESIGN section 5 forbids. This
// is the Copy-trap the lambda_capture_clone_required witness names as the reason its own receipt is
// trustworthy rather than vacuous.
//
// CloneMinimalityUnobserved is a different fact with a different remedy: nobody ran the experiment.
// Collapsing it into CloneEmittedRequired would let an unmeasured clone read as defended.
type CloneMinimality
= CloneAbsent
| CloneEmittedRequired { receipt: NonEmptyStr }
| CloneEmittedRedundant { receipt: NonEmptyStr }
| CloneEmittedUndecidable { reason: NonEmptyStr }
| CloneMinimalityUnobserved

// The receiver shapes the derived population ranges over. Closed, and each is chosen because it
// forces a DIFFERENT arm of CopyRealizationCost out of the emitter -- the axis is the realization
// trichotomy, so a shape that could not distinguish two arms would add a row without adding a
// question.
type CopyReceiverShape
= ReceiverAggregateNonCopy
| ReceiverMachineScalar
| ReceiverSharedContainer

// The use positions the derived population ranges over. Each is chosen for its KNOWN semantic
// answer, which is what makes a differential over the population informative: a direct return needs
// no copy, and a capture by a returned Fn closure provably does (Arm C, rustc E0507, recorded in
// dag/test/claim/lambda_capture_clone_required_witness_test.dag). A duplicated use needs a copy at
// every use but the last.
type CopyUsePosition
= PositionDirectReturn
| PositionReturnedClosureCapture
| PositionDuplicatedArgument

data copy_receiver_shapes_all: List<CopyReceiverShape> = [
ReceiverAggregateNonCopy,
ReceiverMachineScalar,
ReceiverSharedContainer,
]

data copy_use_positions_all: List<CopyUsePosition> = [
PositionDirectReturn,
PositionReturnedClosureCapture,
PositionDuplicatedArgument,
]

// One cell of the derived population. Authored nowhere: cells come from the product below, so a
// shape the axes admit has no way to be left out and no way to be spelled twice.
type CopyQualificationCell {
shape: CopyReceiverShape
position: CopyUsePosition
}

fn copy_cells_for_shape(shape: CopyReceiverShape) -> List<CopyQualificationCell> {
map(copy_use_positions_all, p => CopyQualificationCell { shape: shape, position: p })
}

// THE POPULATION, derived rather than rostered. An exclusion list here would make this a hand
// roster with extra steps; a cell the emitter cannot yet satisfy is a finding below, never a
// removed row.
fn copy_qualification_population() -> List<CopyQualificationCell> {
fold(
copy_receiver_shapes_all,
init: [],
f: (acc, s) => concat(acc, copy_cells_for_shape(shape: s)),
)
}

// THE FOLD TO THE DISPOSITION, replacing three separate coproduct-to-Bool predicates that used to
// answer "does this position require a copy", "is minimality decidable by removal here" and "is
// this receiver a shared handle". Each was a hand-rolled match over a closed coproduct producing a
// bare Bool, none consumed a canonical surface, and -- worse -- they let the two questions be
// answered INDEPENDENTLY, which is how the witness came to assert a required clone on a receiver
// the same model typed undecidable. Folding once onto CloneMinimality makes that contradiction
// unwritable: there is one answer per cell and the undecidable arm is one of its states, not a
// separate flag a caller may ignore.
//
// The oracle is grounded in executed rustc receipts, not in the emitter's output: a direct return
// needs no copy; a capture by a returned Fn closure provably does (Arm C, rustc E0507, recorded in
// dag/test/claim/lambda_capture_clone_required_witness_test.dag); a duplicated argument needs one at
// every use but the last.
//
// THE COPY TRAP IS THE SHAPE ARM, and it is why this is keyed on the cell rather than the position.
// Where the receiver is Copy-eligible, rustc performs an implicit bitwise copy whether or not the
// clone is written, so an EMITTED clone cannot be established as required -- the removal experiment
// returns the same answer for a required and a redundant one. That is a property of the instrument,
// not of the emitter. Note the arm is reached only where a clone is actually emitted: a scalar
// direct return emits none, and CloneAbsent is decidable by direct observation.
fn copy_cell_minimality(cell: CopyQualificationCell) -> CloneMinimality {
match cell.position {
PositionDirectReturn => CloneAbsent
PositionReturnedClosureCapture =>
match cell.shape {
ReceiverMachineScalar =>
CloneEmittedUndecidable {
reason: "Copy-eligible receiver: rustc copies i64 with or without the clone, so removal cannot discriminate required from redundant",
}
ReceiverAggregateNonCopy =>
CloneEmittedRequired {
receipt: "returned Fn closure capture, rustc E0507 on removal (Arm C, lambda_capture_clone_required_witness)",
}
ReceiverSharedContainer =>
CloneEmittedRequired {
receipt: "returned Fn closure capture, rustc E0507 on removal (Arm C, lambda_capture_clone_required_witness)",
}
}
PositionDuplicatedArgument =>
match cell.shape {
ReceiverMachineScalar =>
CloneEmittedUndecidable {
reason: "Copy-eligible receiver: rustc copies i64 with or without the clone, so removal cannot discriminate required from redundant",
}
ReceiverAggregateNonCopy =>
CloneEmittedRequired { receipt: "non-Copy receiver consumed at more than one argument position" }
ReceiverSharedContainer =>
CloneEmittedRequired { receipt: "non-Copy receiver consumed at more than one argument position" }
}
}
}

fn copy_shape_token(shape: CopyReceiverShape) -> String {
match shape {
ReceiverAggregateNonCopy => "aggregate"
ReceiverMachineScalar => "scalar"
ReceiverSharedContainer => "shared"
}
}

fn copy_position_token(position: CopyUsePosition) -> String {
match position {
PositionDirectReturn => "direct"
PositionReturnedClosureCapture => "lambda"
PositionDuplicatedArgument => "dup"
}
}

fn copy_receiver_type_spelling(shape: CopyReceiverShape) -> String {
match shape {
ReceiverAggregateNonCopy => "Widget"
ReceiverMachineScalar => "Int"
ReceiverSharedContainer => "FreeMonoid<Widget>"
}
}

fn copy_fixture_header(shape: CopyReceiverShape) -> String {
match shape {
ReceiverAggregateNonCopy => "\n\ntype Widget {\n tag: String\n}\n\n"
ReceiverMachineScalar => "\n\n"
ReceiverSharedContainer => "\nimport std.algebra { FreeMonoid }\n\ntype Widget {\n tag: String\n}\n\n"
}
}

// The function under emission, one per use position. The anchor name is derived from the same token
// the path is, so a cell cannot assert against a function it did not emit.
fn copy_fixture_body(position: CopyUsePosition, ty: String) -> String {
match position {
PositionDirectReturn =>
"fn cell_direct(w: " + ty + ") -> " + ty + " {\n w\n}\n"
PositionReturnedClosureCapture =>
"fn cell_lambda(w: " + ty + ") -> fn(Int) -> " + ty + " {\n fn(u) { w }\n}\n"
PositionDuplicatedArgument =>
"fn cell_pick(a: " + ty + ", b: " + ty + ") -> " + ty + " {\n a\n}\n\nfn cell_dup(w: " + ty + ") -> " + ty + " {\n cell_pick(w, w)\n}\n"
}
}

fn copy_cell_slug(cell: CopyQualificationCell) -> String {
copy_shape_token(shape: cell.shape) + "_" + copy_position_token(position: cell.position)
}

// THE FIXTURE IS DERIVED FROM THE CELL, which is what makes the population a product rather than a
// roster: there is no place to author a source for a cell the axes do not admit, and no way to omit
// one they do.
fn copy_fixture_source(cell: CopyQualificationCell) -> String {
"module emit_copy_qual." + copy_cell_slug(cell: cell)
+ copy_fixture_header(shape: cell.shape)
+ copy_fixture_body(position: cell.position, ty: copy_receiver_type_spelling(shape: cell.shape))
}

fn copy_fixture_path(cell: CopyQualificationCell) -> String {
"src/emit_copy_qual_" + copy_cell_slug(cell: cell) + ".rs"
}

// A positive structural anchor, always asserted present. Without it a cell whose only assertion is
// an ABSENT .clone() cannot tell a real bare emission from the harness silently emitting nothing --
// compile_dag_rust_emit_check returns false for a refusal and for a missing file alike.
fn copy_fixture_anchor(position: CopyUsePosition) -> String {
match position {
PositionDirectReturn => "fn cell_direct"
PositionReturnedClosureCapture => "fn cell_lambda"
PositionDuplicatedArgument => "fn cell_dup"
}
}

// THE RECEIVER-BOUND REALIZATION SPELLING, and the reason it is spelled with the parameter name
// rather than as a bare "Rc<". Asserting "Rc< occurs somewhere in the emitted file" is a correct
// answer about the WRONG SUBJECT: the returned-closure cell realizes the closure itself as
// Rc<dyn Fn...>, so a bare Rc< probe reports present on a scalar receiver whose parameter is a bare
// i64. That is measured, not hypothetical -- it produced a false shard failure before the
// assertions were bound to the receiver. Every cost-axis assertion below therefore names the
// parameter it is about.
fn copy_receiver_realized_spelling(shape: CopyReceiverShape) -> String {
match shape {
ReceiverAggregateNonCopy => "w: Rc<Widget>"
ReceiverMachineScalar => "w: i64"
ReceiverSharedContainer => "w: Rc<"
}
}

// The spelling the receiver must NOT carry -- the other arm of the realization it was measured to
// take. Paired with the one above so every cell asserts a confirmed positive and a refuted negative
// on the cost axis, rather than an absence that a silently-empty emission would also satisfy.
fn copy_receiver_refuted_spelling(shape: CopyReceiverShape) -> String {
match shape {
ReceiverAggregateNonCopy => "w: Widget"
ReceiverMachineScalar => "w: Rc<"
ReceiverSharedContainer => "w: FreeMonoid"
}
}

// THE CLONE EXPECTATION, derived from the cell's disposition so that an undecidable cell asserts
// NOTHING about clone presence in either direction. This is the finding codex/gpt-5.6-sol raised on
// review 57920 and it was correct: the model typed the scalar cells undecidable while the witness
// went on enforcing a present .clone() there, which claims the clone is REQUIRED -- a stronger
// result than the instrument can decide, and exactly the fabricated plausible output DESIGN section
// 5 forbids.
//
// THE SPELLINGS ARE SITE-BOUND, NOT A GLOBAL ".clone()" SUBSTRING, which is the second finding
// (review 57932) and it was correct for the same reason the cost axis needed binding: a bare
// ".clone()" occurring anywhere in the emitted file is satisfied by an unrelated or wrongly placed
// clone, so it cannot establish the "copies exactly where needed" claim the header makes. Each arm
// now names the expression it is about:
//
// direct return -- asserts ".clone()" ABSENT FROM THE WHOLE FILE, which is the strongest
// count statement available: exactly zero copies, not merely none at a
// named site.
// duplicated argument -- asserts the whole call "cell_pick(w.clone(), w)", which pins placement
// AND count together: the copy is on the first argument and the second is
// bare, so a second clone would falsify it.
// closure capture -- asserts the receiver-bound "w.clone()". Placement is bound to the
// receiver; the emitter's closure prelude spelling is not pinned here, so
// this arm bounds WHERE the copy is, not how many times the closure body
// might mention it. Stated rather than claimed as exact.
//
// The undecidable cell is WITHHELD, NOT EXCLUDED. It still runs, still asserts its structural
// anchor, and still asserts both arms of the cost axis; only the one question the instrument cannot
// answer goes unasserted, and undecidable_cells_withhold_clone_assertion in the witness pins which
// cells those are, so a future change cannot widen undecidability to buy a green.
fn copy_cell_clone_site_spelling(cell: CopyQualificationCell) -> String {
match cell.position {
PositionDirectReturn => ".clone()"
PositionReturnedClosureCapture => "w.clone()"
PositionDuplicatedArgument => "cell_pick(w.clone(), w)"
}
}

fn copy_cell_clone_present_expectation(cell: CopyQualificationCell) -> List<String> {
match copy_cell_minimality(cell: cell) {
CloneEmittedRequired { receipt: _ } => [copy_cell_clone_site_spelling(cell: cell)]
CloneAbsent => []
CloneEmittedUndecidable { reason: _ } => []
CloneEmittedRedundant { receipt: _ } => []
CloneMinimalityUnobserved => []
}
}

fn copy_cell_clone_absent_expectation(cell: CopyQualificationCell) -> List<String> {
match copy_cell_minimality(cell: cell) {
CloneAbsent => [copy_cell_clone_site_spelling(cell: cell)]
CloneEmittedRequired { receipt: _ } => []
CloneEmittedUndecidable { reason: _ } => []
CloneEmittedRedundant { receipt: _ } => []
CloneMinimalityUnobserved => []
}
}

// The spellings a cell must contain, derived jointly from the semantic oracle (does this position
// require a copy) and the measured realization (how is this receiver realized). Nothing here is
// authored per cell, so the check compares the emitter to a ground rather than to itself.
fn copy_cell_expected_present(cell: CopyQualificationCell) -> List<String> {
concat(
concat(
[copy_fixture_anchor(position: cell.position)],
copy_cell_clone_present_expectation(cell: cell),
),
[copy_receiver_realized_spelling(shape: cell.shape)],
)
}

fn copy_cell_expected_absent(cell: CopyQualificationCell) -> List<String> {
concat(
copy_cell_clone_absent_expectation(cell: cell),
[copy_receiver_refuted_spelling(shape: cell.shape)],
)
}
Loading
Loading