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
107 changes: 107 additions & 0 deletions dag/test/claim/operation_body_unknown_field_refused_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
module test.claim.operation_body_unknown_field_refused_witness

import std.types { String, Bool, Int }
import v2.std.optional { Present, Absent }
import gunbc.compile_diagnostic_census { CompileDiagnosticCensus, CensusObserved, CensusNotRunnable, CompileDiagnosticCensusRow, census_blocking_rows, census_total_count }
import gunbc.guarantee_probe_corpus { census_blocking_count_for_class }

// THE OPERATION-BODY GENERIC-SWALLOW ARM DISCARDED UNRECOGNIZED FIELDS SILENTLY.
//
// THE CLASS, not one instance of it. gunbc#8593 found that admit_callers written on an operation
// parses, resolves clean, and does nothing -- but admit_callers was never the defect. The v1 seed's
// parse_op_body_entries (src/v1/stage0/src/v1_compiler_parse.rs) had a generic fallback arm: any
// `ident:` at operation-body top level that was not one of the known fields (input, output,
// transport, exit, response, mock_response, idempotent, readonly, hermetic) was parsed as an
// expression AND THEN DISCARDED -- the parsed value was never stored in any accumulator, the loop
// just continued. That is DESIGN §5 silent wrongness at the source boundary: a misspelled
// mock_response, a misspelled transport, any typo at all, is accepted with no diagnostic. The
// scariest instance is exactly the hermetic-mock case -- a typo'd mock_response silently unmocked,
// and a witness believing it replays a recorded result is doing something else while staying green.
//
// THE FIX REFUSES THE ARM ITSELF, not the one name. The generic-swallow branch is deleted; any
// unrecognized identifier at operation-body top level now falls straight to the existing
// "unexpected '{id}' in operation body" parse_error refusal that already guarded the non-colon
// shape. This makes the whole class unwritable in one move and is LESS code than enumerating
// admit_callers as a special case would have been -- a discard deleted, not a name added to a list.
//
// SCOPE, stated per DESIGN 4b so this receipt is not read wider than it is. This is a PARSE-TIME
// refusal on the v1 seed's Rust parser. It closes the "silently discarded field" class at
// operation-body top level. It says nothing about, and does not attempt, operation-grain
// admit_callers ENFORCEMENT (gunbc#8593's own finding) -- that remains a separate, larger,
// unstarted capability (SeedFeatureCompletion under the v1 seed freeze), not something a parse
// refusal can provide. Population measured before landing: zero of the 325 operation declarations
// across dag/ and src/v2/ carried a field outside the known set, so this refusal fires on nothing
// in the live corpus and the class was purely latent, exactly as #8593's admit_callers instance was.
//
// WHY A NONSENSE KEY, NOT admit_callers, IS THE DISCRIMINATING RED HERE. #8593's own file already
// owns admit_callers as its subject and is not this fix's to edit while it is open. More to the
// point, the claim under test here is about the ARM, not about any one field name -- so the red
// uses a field name (bogus_nonsense_field) that names nothing the grammar has ever recognized,
// which is the honest subject for "any unrecognized field is refused" rather than a name that
// happens to also be independently interesting for enforcement reasons.
//
// SHAPE, same reason as #8593: sources compiled as DATA through the guarantee probe corpus, so an
// unadmitted... here, an ill-formed... operation body can be observed without taking this file's
// own resolve down with it -- a parse error in real module source would refuse the whole file.

data operation_valid_body_source: String = "module probe_op_valid_body\nimport std.types { String, Int }\nservice probe.ValidSvc {\n operation Sealed {\n input { arg: String }\n output { exit_code: Int from \"exit_code\" }\n readonly\n transport shell { argv: [\"true\", arg] }\n exit { 0 => Unit nonzero => Unit }\n mock_response { 0 => { exit_code: 0 } \"hermetic\" }\n }\n}\n"

data operation_unknown_field_source: String = "module probe_op_unknown_field\nimport std.types { String, Int }\nservice probe.BadSvc {\n operation Sealed {\n input { arg: String }\n output { exit_code: Int from \"exit_code\" }\n readonly\n bogus_nonsense_field: 1\n transport shell { argv: [\"true\", arg] }\n exit { 0 => Unit nonzero => Unit }\n mock_response { 0 => { exit_code: 0 } \"hermetic\" }\n }\n}\n"

data admit_fn_form_source: String = "module probe_admit_fn_form\nimport test.fixture.sole_constructor_sealed.definer { LocalValidated, mint_sealed_local }\nfn unadmitted_caller() -> LocalValidated {\n mint_sealed_local(n: 65)\n}\n"

fn op_census_of(source: String) -> CompileDiagnosticCensus {
compile_dag_diagnostic_census(source)
}

fn census_is_clean(census: CompileDiagnosticCensus) -> Bool {
match census {
CensusObserved { rows: rows } => census_total_count(rows: census_blocking_rows(rows: rows)) == 0
CensusNotRunnable { cause: _ } => false
}
}

// POSITIVE CONTROL 1, GREEN TODAY AND AFTER THE FIX. A legitimate operation body using every known
// top-level field (input, output, readonly, transport, exit, mock_response) compiles with zero
// blocking diagnostics. Without this, a red on the unknown-field source below could equally mean
// the refusal fires correctly OR that this file's operation-form fixture is malformed and would
// have refused regardless of the field under test -- different states, different remedies.
test fn operation_body_with_only_known_fields_compiles_clean() -> Bool {
census_is_clean(op_census_of(source: operation_valid_body_source))
}

// THE FIX, DISCRIMINATING RED BEFORE, GREEN AFTER. Identical operation body, one nonsense field
// added at top level. Before the fix this field was parsed as an expression and silently
// discarded -- census_is_clean would have read true, indistinguishable from the control above.
// After the fix it is a blocking ParseError.
test fn operation_body_unknown_field_is_refused_not_silently_dropped() -> Bool {
match census_blocking_count_for_class(
census: op_census_of(source: operation_unknown_field_source),
wanted: "ParseError"
) {
Present { value: n } => n >= 1
Absent => false
}
}

// POSITIVE CONTROL 2, REGRESSION CONTROL FOR THE UNTOUCHED PATH. fn-attached admit_callers is
// enforced through a single call site (parse_fn_body_from_prefix, src/v1/stage0/src/
// v1_compiler_parse.rs) this fix never touches -- operations never reached that call site in the
// first place, since operations have no admit_callers parse path at all (confirmed: every real
// admit_callers site in dag/ and src/v2/ is fn-attached, and a sealed type's admit_callers rides
// its constructor fn, e.g. extdeps.shell.exec.transport_script_seal -- there is no separate
// sealed-type parse path to exercise). This proves the parser edit did not regress the mechanism
// it sits beside. The subject is the purpose-built fixture test.fixture.sole_constructor_sealed,
// not transport_script_seal directly, for the same measured cost reason #8593 gives: compiling a
// caller of transport_script_seal drags the whole shell/extdeps closure through the census (54.9s,
// ~1GB RSS there); the fixture's LocalValidated is sole_constructor-sealed the same way and costs a
// fraction of that.
test fn fn_attached_admit_callers_still_refuses_unadmitted_caller() -> Bool {
match census_blocking_count_for_class(
census: op_census_of(source: admit_fn_form_source),
wanted: "ConstructorCallAdmissionRefused"
) {
Present { value: n } => n >= 1
Absent => false
}
}
9 changes: 9 additions & 0 deletions src/v1/stage0/src/cli_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41776,6 +41776,15 @@ pub fn run_required_floor(
if let Some(path) = long_home_storage_agreement_path {
write_long_home_storage_agreement_tsv(&path, &outcome.long_home_storage_agreement)?;
}
// Diagnosis-only, never gated on: PREPARE_GRAMMAR_CROSS_CLAIM_MEMO has no eval_call_memo-style
// hit/miss disclosure, so whether it amortizes grammar preparation across claims has been
// unobservable except by inferring it from wall-clock cost after the fact (gunbc#8581's own
// premise). This prints the raw counts so that inference is no longer necessary.
let (cross_claim_hits, cross_claim_misses, cross_claim_stores) =
crate::v1_interpreter::prepare_grammar_cross_claim_memo_counters();
eprintln!(
"[cross-claim-memo] prepare_grammar hits={cross_claim_hits} misses={cross_claim_misses} stores={cross_claim_stores}"
);
Ok(outcome)
}

Expand Down
31 changes: 29 additions & 2 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1437,6 +1437,12 @@ thread_local! {
static PREPARE_GRAMMAR_CROSS_CLAIM_MEMO: RefCell<PrepareGrammarCrossClaimMemo> =
RefCell::new(PrepareGrammarCrossClaimMemo::default());
static CROSS_CLAIM_FN_KEEPALIVE: RefCell<Vec<Rc<Node>>> = RefCell::new(Vec::new());
// Diagnosis-only counters: this memo has no eval_call_memo-style hit/miss disclosure, so its
// amortization behavior is currently unobservable short of instrumenting it. These count
// exactly the three decisions the memo can make — never gate, never change behavior.
static PREPARE_GRAMMAR_CROSS_CLAIM_MEMO_HITS: Cell<u64> = Cell::new(0);
static PREPARE_GRAMMAR_CROSS_CLAIM_MEMO_MISSES: Cell<u64> = Cell::new(0);
static PREPARE_GRAMMAR_CROSS_CLAIM_MEMO_STORES: Cell<u64> = Cell::new(0);
}

pub fn clear_cross_claim_pure_memos() {
Expand All @@ -1445,6 +1451,16 @@ pub fn clear_cross_claim_pure_memos() {
CROSS_CLAIM_FN_KEEPALIVE.with(|k| k.borrow_mut().clear());
}

/// Diagnosis-only: (hits, misses, stores) since process start or the last clear. Never read by
/// any decision path — added to make the memo's amortization behavior observable at all.
pub fn prepare_grammar_cross_claim_memo_counters() -> (u64, u64, u64) {
(
PREPARE_GRAMMAR_CROSS_CLAIM_MEMO_HITS.with(|c| c.get()),
PREPARE_GRAMMAR_CROSS_CLAIM_MEMO_MISSES.with(|c| c.get()),
PREPARE_GRAMMAR_CROSS_CLAIM_MEMO_STORES.with(|c| c.get()),
)
}

fn keep_cross_claim_fn(fn_node: &Rc<Node>) {
CROSS_CLAIM_FN_KEEPALIVE.with(|k| {
let mut keepalive = k.borrow_mut();
Expand Down Expand Up @@ -1482,8 +1498,18 @@ fn try_cross_claim_pure_memo(
_ => return None,
};
let memo_key = (Rc::as_ptr(fn_node) as usize, content_hash);
let portable =
PREPARE_GRAMMAR_CROSS_CLAIM_MEMO.with(|m| m.borrow().map.get(&memo_key).cloned())?;
let found =
PREPARE_GRAMMAR_CROSS_CLAIM_MEMO.with(|m| m.borrow().map.get(&memo_key).cloned());
let portable = match found {
Some(p) => {
PREPARE_GRAMMAR_CROSS_CLAIM_MEMO_HITS.with(|c| c.set(c.get() + 1));
p
}
None => {
PREPARE_GRAMMAR_CROSS_CLAIM_MEMO_MISSES.with(|c| c.set(c.get() + 1));
return None;
}
};
return Some(value_from_portable_ctx(ctx, &portable));
}
None
Expand Down Expand Up @@ -1514,6 +1540,7 @@ fn store_cross_claim_pure_memo(
.map
.insert((Rc::as_ptr(fn_node) as usize, h), portable)
});
PREPARE_GRAMMAR_CROSS_CLAIM_MEMO_STORES.with(|c| c.set(c.get() + 1));
}
}
}
Expand Down
Loading