diff --git a/dag/gunbc/recurring_failure_mode/refinement_predicate_enforced_only_where_the_value_is_a_literal.dag b/dag/gunbc/recurring_failure_mode/refinement_predicate_enforced_only_where_the_value_is_a_literal.dag new file mode 100644 index 00000000000..bd56629686a --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/refinement_predicate_enforced_only_where_the_value_is_a_literal.dag @@ -0,0 +1,21 @@ +module gunbc.recurring_failure_mode.refinement_predicate_enforced_only_where_the_value_is_a_literal + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data refinement_predicate_enforced_only_where_the_value_is_a_literal: RecurringFailureMode = RecurringFailureMode { + identity: "refinement_predicate_enforced_only_where_the_value_is_a_literal" as NonEmptyStr, + receipts: [ + "SUBJECT: a value that violates the predicate of a `where`-refined type, at a position declared to hold that type. std.types declares NonEmptyStr = String where non_empty, and PathSegment, GlobSegment, LogicalTime and a dozen branded ids as NonEmptyStr where brand(...). THE WALL IS A PROPERTY OF THE SPELLING AT THE SITE, NOT OF THE REFINEMENT: enforcement lives in v1.compiler.infer where_refinement_mismatch_diags, reached from infer_expr through with_expected_where_refinement_diags at every position that threads an expected type -- but where_refinement_diags_for_predicate DECIDES ONLY WHEN THE VALUE IS A LITERAL. Every non-deciding arm emits WhereRefinementUnenforced, and all six of its reasons are advisory by policy (v1.std.core is_where_refinement_unenforced_advisory_reason -> SeverityNonError / GateAdvisoryTypecheck). So the refinement is a comment everywhere a value is not written out at the seam. This is the floor obligation that values inhabit declared types (DESIGN 4b, the floor first), broken for every non-literal value rather than for one argument shape -- which is what separates it from its neighbour refined_alias_argument_exempt_from_declared_type_inhabitance, a class about the FORMAL being a record.", + "CENSUS, MEASURED BY EXECUTION ACROSS THREE ROUTES ON ONE BINARY, 2026-09-14, main 74627165a69. R1 INTERPRETATION, `gunbc run`: a blank element in a List reaching a List parameter, and `\"../../etc\" as PathSegment`, both run to exit 0 with no refusal (the gunbc-private#124 trigger, reproduced). R2 THE FIXTURE HARNESS, compile_dag_diagnostic_census, which its own carrier note scopes to the v1 pipeline to the RUST RENDER TARGET on a synthetic single module. R3 EMISSION, `gunbc compile --target rust|python|go`: exits 0, and the refinement is ERASED -- emitted Rust is `pub fn take(xs: Rc>)` and `fn hostile_segment(raw: String) -> NonEmptyStr { raw.clone() }`, NonEmptyStr a bare String alias, PathSegment not surviving as a distinct name, no constructor and no check; python and go the same. The NonEmptyVec/NonEmptyBTreeSet wrappers that DO validate are for non-empty COLLECTIONS and never touch `String where non_empty`. THE POSITIVE CONTROL HOLDS AND IS WHAT MAKES THE ZEROS OBSERVATIONS: on R2 a blank LITERAL refuses with a blocking TypeMismatch at all seven literal seams -- data binding, cast, function return, let, record field, list literal, call argument.", + "WHAT ADMITS, on R2, each measured as a differential against a control identical but for the hostile term. ADVISORY-ONLY (one WhereRefinementUnenforced, nothing blocking): call argument through a String parameter, with or without a cast; function return; let binding; record field; match payload; Map value; an element cast inside a list literal. SILENT -- zero blocking AND zero advisory, no diagnostic of any severity: (a) A LIST ELEMENT THROUGH A FUNCTION-PARAMETER BOUNDARY, the #124 shape, whether or not an `as` cast is written; (b) AN ALIAS-MEDIATED POSITION. (b) is the sharpest cell and was not predicted: `data v: PathSegment = \"\" as PathSegment` REFUSES, and the identical construction through a one-line local alias, `type Seg = PathSegment` then `data v: Seg = \"\" as Seg`, is admitted in silence. One alias line defeats the only wall this class has. THE ALIAS HOLE IS WIDER THAN THE CAST FORM, first measured by fierce-moth-238 and re-run by this lane on the same R2 route: `type Seg = NonEmptyStr` then `fn f() -> Seg { \"\" }` is silent while the direct `fn f() -> NonEmptyStr { \"\" }` refuses, so the plain alias edge drops the predicate with no cast, brand or data binding; a List let returned as List, or fed to a List parameter, is silent too. The same lane reports, by execution on R1 and not re-run here, that the interpreter carries no predicate arm: blank, .. and a/b elements and an LF-bearing String cast as PathSegment reach their consumers with zero diagnostics, beside an interpreter positive control where take(xs: [\"\"]) refuses at resolve.", + "THE PATHSEGMENT HALF IS WORSE AND IT IS NOT A SEAM PROBLEM. `brand` is on the compiler's DEFERRED predicate list (v1.compiler.infer where_refinement_is_deferred_predicate), so PathSegment contributes NO decidable predicate of its own and inherits only `non_empty` transitively. The law std.types path_segment_safety_note calls 'the law, held once' lives in path_segment_is_safe, an ordinary runtime fn that NO SEAM CONSULTS. Measured on R2: of the characters that note names -- `.` `..` `/` `\\` CR LF NUL -- ZERO are refused at any seam, on any route, in any spelling, INCLUDING as a bare literal, which is the one place every other predicate in this corpus does refuse. `\"..\" as PathSegment` and `\"a/b\" as PathSegment` compile clean. The blank is the sole refusal and only because non_empty reached it. GlobSegment is identical.", + "BRAND FORGERY, the consequence that ranks. gunbc.merge_admission_subject WalkAttemptId and gunbc.fleet_known_hosts_anchor FleetSshAttemptIdentity are both `PathSegment where brand(...)`, and both modules state in their own prose that their validating fn is 'the only constructor' and 'REFUSES rather than sanitizing'. BOTH STATEMENTS ARE TRUE ABOUT THE FUNCTIONS AND FALSE ABOUT THE TYPES: a refined alias has no constructor to seal, so sole-constructor admission never applies to it. Measured: a foreign module writing `\"../../etc\" as WalkAttemptId` or `\"a/b\" as FleetSshAttemptIdentity` -- carrying exactly the characters those functions exist to refuse, into ids that are concatenated into /.gunbc/merge-admission// and into the known-hosts anchor path -- adds ZERO blocking diagnostics.", + "PRODUCTION CONSUMERS, INCLUDING A CORRECTION TO THIS LANE'S FIRST READING, which claimed PathSegment had exactly two producers, the branded walk_attempt_id and fleet_ssh_attempt_identity, both calling path_segment_is_safe. That counted brands and missed the unbranded carrier: std.types FilePathParts has `segments: List`, and extdeps.rust.cargo cargo_target_source_path and rust_module_candidate_paths build it from a bare caller String (`concat(name, \".rs\")`, and `[\"src\", stem, \"mod.rs\"]`) at the admitted list-element seam with no path_segment_is_safe, so a stem of \"..\" yields src/../mod.rs with no refusal. Found by the parallel census lane fierce-moth-238 and confirmed by grep: both fns' ONLY caller is test.claim.cargo_target_path_witness_test, so it is a third, unguarded producer and NOT a live production hazard. The FilePathParts renderers that join on / (v2.extdeps.languages.bash_orch_if bash_relative_parts_text / bash_absolute_parts_text, extdeps.linux.proc_self_cgroup proc_self_cgroup_mount_root_text) receive only literal segments in production (v2.workflow.ci_floor_peak_emit). GlobSegment has ZERO consumers. extdeps.uri_path PathSegmentTokensResult / MalformedPathSegment are a different name, not this type.", + "ENROLLED FORM: three probes under dag/test/probe/ -- refinement_seam_admission_probe, path_segment_predicate_admission_probe, branded_path_segment_forgery_probe -- each a module that RESOLVES TODAY, which is the finding. test.claim.refinement_seam_enforcement_witness reads each off the tree and hands it to compile_dag_diagnostic_census paired with a control that is the same module with every hostile term made safe, so the shared closure cancels and the delta is the hostile term alone; the carrier's own rule forbids reading a total over an importing fixture. It asserts the literal wall at delta 1 FIRST -- without that the zeros would be indistinguishable from a harness that cannot refuse, which DESIGN 4b calls a permanently-green decoration -- then asserts the admissions at delta 0. Those zero assertions are the tripwires: each goes red the day its seam starts refusing, and the probe is then rewritten to expect the refusal rather than retiring (DESIGN 4b(4)).", + "RUNG FOUND AT AND CURRENT RUNG: silent wrongness, OUTSIDE the ladder, and that is the MINIMUM across all three in-scope routes, which is the rung (DESIGN 4b(1)). Citing the literal wall would be inflation twice over: it is mechanically preventable at best, and the alias receipt shows it defeated by one line. CEILING: structurally guaranteed (3), not impossible (4). non_empty and path_segment_is_safe are total decidable functions of a fully-modeled String, and the compiler already computes the first -- decidable_where_string_predicate_holds runs non_empty today -- so the judgment is not the missing piece; what is missing is that it is attempted only for literals, and that brand carries no predicate to a value's provenance. (4) is out of reach while these are refined ALIASES, because an alias has no constructor to seal, which is why the ceiling stops at (3) rather than at unwritability.", + "NEXT-RUNG TRIGGER, capability grain: the refinement judgment decides a value's predicate from its PROVENANCE rather than from its spelling at the seam -- a value whose origin does not establish the predicate is refused at a refined position, at every seam that threads an expected type, with alias-mediated and list-element positions judged exactly as the direct spelling is. Sufficient for flipping every zero-delta assertion in test.claim.refinement_seam_enforcement_witness to expect refusals. NOT satisfied by: widening the literal arm to more literal shapes; promoting WhereRefinementUnenforced from advisory to blocking, which refuses correct code rather than judging it; or adding a predicate to brand() alone, which leaves every non-branded refinement where it is. A SEPARATE AND SMALLER TRIGGER CLOSES THE FORGERY HALF ALONE, and it is worth naming because it does not touch a load-bearing stage: each branded path-segment id becomes a sealed sole_constructor record whose only mint runs path_segment_is_safe, at which point the two prose 'only constructor' claims become walls. That closes forgery for those brands and closes nothing else.", + "WHERE THE FIX LIVES, FLAGGED AND NOT STARTED per the census lane's brief: v1.compiler.infer (where_refinement_diags_for_predicate, where_refinement_mismatch_diags) and the disposition policy in v1.std.core -- the v1 seed's inference stage, which DESIGN names as load-bearing, and which is semantics-frozen under gunbc.v1_maintenance_standing so a change there must pass its PURPOSE admission test. READ, NOT MEASURED, and labelled as a code reading rather than a receipt: src/v2/compiler/04_infer.dag carries no where-refinement predicate judgment of any kind, so on the v2 route the wall is not weak but ABSENT, and the question for the fix lane is whether it is BUILT there rather than repaired in the seed. Probing the v2 route by execution is the first step of that lane, not a claim this row makes.", + ], + evidence: [], +} diff --git a/dag/test/claim/refinement_seam_enforcement_witness_test.dag b/dag/test/claim/refinement_seam_enforcement_witness_test.dag new file mode 100644 index 00000000000..55544b683f5 --- /dev/null +++ b/dag/test/claim/refinement_seam_enforcement_witness_test.dag @@ -0,0 +1,189 @@ +module test.claim.refinement_seam_enforcement_witness + +import std.types { String, Bool, Int, List } +import extdeps.filesystem.filesystem_io +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, CompileDiagnosticCensusRow, CensusObserved, CensusNotRunnable, +} + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// WHAT THIS WITNESS ESTABLISHES. The refinement predicates std.types declares are enforced ONLY +// where the value at the seam is a literal, and the branded PathSegment law is enforced nowhere at +// all. The three probes under dag/test/probe/ are the census fixtures; this file is what makes +// them evidence rather than decoration (DESIGN 4b: the RED must be authorable, and then it must be +// executed). +// +// THE READING IS A DIFFERENTIAL, NEVER A TOTAL. gunbc.compile_diagnostic_census states the rule on +// its own carrier: CensusObserved carries every diagnostic the whole compile produced, imported +// closure included, so a total over an importing fixture is not a fact about the fixture. The two +// exact forms it names are a count scoped to class AND subject, and a differential between two +// censuses whose sources differ on ONE axis, where the shared closure cancels. Every assertion +// below is the second form: each probe is paired with a control that is the same module with the +// hostile term replaced by a safe one, so the delta is the blocking diagnostics the hostile term +// alone caused. +// +// THE POSITIVE CONTROL IS ASSERTED FIRST AND IT IS LOAD-BEARING. A blank literal at a refined +// position DOES refuse, blocking, with delta exactly 1. Without that assertion every zero below +// would be indistinguishable from a harness that cannot refuse anything -- which is the shape +// DESIGN 4b calls a permanently-green decoration. It also fixes the axis: the wall the zeros are +// measured against is real and is one term away. +// +// THE ROUTE THIS MEASURES, named rather than assumed (DESIGN 4b(1): a class's rung is the minimum +// across its in-scope paths, and citing the strongest is inflation). compile_dag_diagnostic_census +// measures the v1 pipeline to the RUST RENDER TARGET on a synthetic single module, per its own +// carrier note. The interpretation route and the python/go emission routes were measured by the +// filing lane and are recorded on the gunbc.recurring_failure_mode row; this witness does not +// assert them, because it cannot reach them. + +data probe_dir: String = "dag/test/probe/" + +fn probe_source(name: String) -> String { + filesystem_read(path: probe_dir + name + ".dag").content +} + +fn census_of(source: String) -> CompileDiagnosticCensus { + compile_dag_diagnostic_census(source) +} + +fn blocking_total(c: CompileDiagnosticCensus) -> Int { + match c { + CensusNotRunnable { cause: _ } => -1 + CensusObserved { rows: rows } => + rows |> filter(r => r.blocking) |> fold(init: 0, f: (acc, r) => acc + r.count) + } +} + +fn census_ran(c: CompileDiagnosticCensus) -> Bool { + match c { + CensusNotRunnable { cause: _ } => false + CensusObserved { rows: _ } => true + } +} + +// The blocking diagnostics the hostile term alone caused. Both censuses run, or the delta is +// refused as -1000 rather than reported as a number: could-not-measure must never read as the +// subject passing (DESIGN 5, the absorbing fallback). +fn blocking_delta(hostile: String, safe: String) -> Int { + let h = census_of(source: hostile) + let s = census_of(source: safe) + if census_ran(c: h) && census_ran(c: s) { + blocking_total(c: h) - blocking_total(c: s) + } else { + -1000 + } +} + +data seam_hdr: String = "module probe_refinement_seam\nimport std.types { String, Bool, Int, List, NonEmptyStr, PathSegment }\n" + +// THE POSITIVE CONTROL. A blank literal cast to a refined alias refuses, blocking; the same cast +// of a non-blank literal does not. Delta exactly 1. +test fn a_blank_literal_at_a_refined_position_refuses() -> Bool { + blocking_delta( + hostile: seam_hdr + "fn f() -> NonEmptyStr { \"\" as NonEmptyStr }\n", + safe: seam_hdr + "fn f() -> NonEmptyStr { \"ok\" as NonEmptyStr }\n" + ) == 1 +} + +// The same wall at the seam positions that DO hold it, so the zeros below are located rather than +// general: record field, list literal, call argument, function return, let binding. +test fn a_blank_literal_refuses_at_the_record_list_argument_return_and_let_seams() -> Bool { + blocking_delta( + hostile: seam_hdr + "type R { s: NonEmptyStr }\nfn f() -> R { R { s: \"\" } }\n", + safe: seam_hdr + "type R { s: NonEmptyStr }\nfn f() -> R { R { s: \"ok\" } }\n" + ) == 1 + && blocking_delta( + hostile: seam_hdr + "data v: List = [\"\"]\n", + safe: seam_hdr + "data v: List = [\"ok\"]\n" + ) == 1 + && blocking_delta( + hostile: seam_hdr + "fn take(s: NonEmptyStr) -> Int { 1 }\nfn f() -> Int { take(s: \"\") }\n", + safe: seam_hdr + "fn take(s: NonEmptyStr) -> Int { 1 }\nfn f() -> Int { take(s: \"ok\") }\n" + ) == 1 + && blocking_delta( + hostile: seam_hdr + "fn f() -> NonEmptyStr { \"\" }\n", + safe: seam_hdr + "fn f() -> NonEmptyStr { \"ok\" }\n" + ) == 1 + && blocking_delta( + hostile: seam_hdr + "fn f() -> NonEmptyStr { let v: NonEmptyStr = \"\"\n v }\n", + safe: seam_hdr + "fn f() -> NonEmptyStr { let v: NonEmptyStr = \"ok\"\n v }\n" + ) == 1 +} + +// EXPECTING-RED HOLE. The whole seam probe -- the #124 list-element shape, the alias-mediated +// blank literal, and the two non-literal seams -- adds NOT ONE blocking diagnostic over a control +// that is the identical module with every hostile term made safe. This assertion is the tripwire: +// it goes red the day any of those seams starts refusing, and the probe is then rewritten to +// expect the refusal. +data seam_probe_control: String = "module probe_refinement_seam_control\nimport std.types { String, Int, List, NonEmptyStr, PathSegment }\nfn blanks() -> List { [\"a\", \"b\"] }\nfn take_nonempty_list(xs: List) -> Int { count(xs) }\nfn blank_reaches_a_nonempty_list() -> Int { take_nonempty_list(xs: blanks()) }\ntype Seg = PathSegment\ndata blank_through_an_alias: Seg = \"ok\" as Seg\nfn take_nonempty(s: NonEmptyStr) -> Int { 1 }\nfn any_string_reaches_a_nonempty_parameter(raw: String) -> Int { take_nonempty(s: raw) }\nfn any_string_becomes_a_nonempty_return(raw: String) -> NonEmptyStr { raw as NonEmptyStr }\n" + +test fn every_non_literal_seam_and_the_alias_mediated_literal_still_admit_a_blank() -> Bool { + blocking_delta( + hostile: probe_source(name: "refinement_seam_admission_probe"), + safe: seam_probe_control + ) == 0 +} + +// EXPECTING-RED HOLE, and the sharper half of it stated on its own: one local alias line defeats +// the literal wall the positive control above establishes. The pair differs only in whether the +// cast names PathSegment directly or through `type Seg = PathSegment`. +test fn an_alias_defeats_the_literal_wall_that_the_direct_spelling_holds() -> Bool { + blocking_delta( + hostile: seam_hdr + "data v: PathSegment = \"\" as PathSegment\n", + safe: seam_hdr + "data v: PathSegment = \"ok\" as PathSegment\n" + ) == 1 + && blocking_delta( + hostile: seam_hdr + "type Seg = PathSegment\ndata v: Seg = \"\" as Seg\n", + safe: seam_hdr + "type Seg = PathSegment\ndata v: Seg = \"ok\" as Seg\n" + ) == 0 +} + +// EXPECTING-RED HOLE, measured first by the parallel census lane fierce-moth-238 and re-run by this +// lane before enrolling. The alias edge drops the predicate with no cast, no brand and no data +// binding: a blank returned through `type Seg = NonEmptyStr` is silent where the direct return +// (asserted at delta 1 above) refuses. Two more #124-shaped cells with no parameter-literal +// involved: a List let returned as List, and the same let fed to a +// List parameter. +test fn the_alias_edge_and_let_bound_lists_admit_a_blank_without_any_cast() -> Bool { + blocking_delta( + hostile: seam_hdr + "type Seg = NonEmptyStr\nfn f() -> Seg { \"\" }\n", + safe: seam_hdr + "type Seg = NonEmptyStr\nfn f() -> Seg { \"ok\" }\n" + ) == 0 + && blocking_delta( + hostile: seam_hdr + "fn f() -> List {\nlet raw: List = [\"\"]\nraw\n}\n", + safe: seam_hdr + "fn f() -> List {\nlet raw: List = [\"ok\"]\nraw\n}\n" + ) == 0 + && blocking_delta( + hostile: seam_hdr + "fn take(xs: List) -> Int { 0 }\nfn g() -> Int {\nlet raw: List = [\"\"]\ntake(xs: raw)\n}\n", + safe: seam_hdr + "fn take(xs: List) -> Int { 0 }\nfn g() -> Int {\nlet raw: List = [\"ok\"]\ntake(xs: raw)\n}\n" + ) == 0 +} + +// EXPECTING-RED HOLE. Every character std.types path_segment_safety_note names as the law -- +// `..`, `/`, `\`, LF, NUL -- is admitted as a BARE LITERAL at the position the brand declares, +// which is the one place every other predicate in this corpus refuses. `brand` is on the deferred +// list, so PathSegment carries no decidable predicate; the law lives in a runtime fn no seam +// consults. +data path_segment_probe_control: String = "module probe_path_segment_control\nimport std.types { String, PathSegment, GlobSegment }\ndata navigates_out_of_its_parent: PathSegment = \"ok\" as PathSegment\ndata introduces_a_level: PathSegment = \"ok\" as PathSegment\ndata introduces_a_level_backslash: PathSegment = \"ok\" as PathSegment\ndata terminates_a_line_oriented_record: PathSegment = \"ok\" as PathSegment\ndata terminates_at_the_syscall_boundary: PathSegment = \"ok\" as PathSegment\ndata a_glob_segment_navigates_too: GlobSegment = \"ok\" as GlobSegment\nfn any_string_becomes_a_segment(raw: String) -> PathSegment { raw as PathSegment }\n" + +test fn no_path_segment_safety_character_is_refused_at_any_seam() -> Bool { + blocking_delta( + hostile: probe_source(name: "path_segment_predicate_admission_probe"), + safe: path_segment_probe_control + ) == 0 +} + +// EXPECTING-RED HOLE, and the consequence that ranks. Two production modules declare in prose that +// their validating fn is the only constructor of a branded PathSegment that becomes a directory +// name. A foreign module mints both with a cast carrying the exact `..` and `/` those functions +// exist to refuse, and adds no blocking diagnostic. The control imports the SAME two production +// modules, so their whole closure cancels and the delta is the forgery alone. +data forgery_probe_control: String = "module probe_forgery_control\nimport std.types { String }\nimport gunbc.merge_admission_subject { WalkAttemptId }\nimport gunbc.fleet_known_hosts_anchor { FleetSshAttemptIdentity }\ndata forged_attempt_id_escapes_its_directory: WalkAttemptId = \"ok\" as WalkAttemptId\ndata forged_ssh_identity_introduces_a_level: FleetSshAttemptIdentity = \"ok\" as FleetSshAttemptIdentity\nfn any_string_becomes_an_attempt_id(raw: String) -> WalkAttemptId { raw as WalkAttemptId }\n" + +test fn a_branded_path_segment_can_be_forged_from_any_module() -> Bool { + blocking_delta( + hostile: probe_source(name: "branded_path_segment_forgery_probe"), + safe: forgery_probe_control + ) == 0 +} diff --git a/dag/test/probe/branded_path_segment_forgery_probe.dag b/dag/test/probe/branded_path_segment_forgery_probe.dag new file mode 100644 index 00000000000..15e55f1c788 --- /dev/null +++ b/dag/test/probe/branded_path_segment_forgery_probe.dag @@ -0,0 +1,32 @@ +module test.probe.branded_path_segment_forgery_probe + +// THIS MODULE RESOLVES TODAY, AND THAT IS THE FINDING -- an EXPECTING-RED hole. +// +// Two production modules brand a PathSegment into an identity that becomes a DIRECTORY NAME, and +// both say in their own prose that their validating fn is the only way in: +// +// gunbc.merge_admission_subject -- "Both producers ... go through walk_attempt_id, the only +// constructor, and refuse rather than sanitizing." +// The id is concatenated into +// /.gunbc/merge-admission//. +// gunbc.fleet_known_hosts_anchor -- "fleet_ssh_attempt_identity is the only constructor and +// REFUSES rather than sanitizing". +// +// Both statements are TRUE ABOUT THE FUNCTIONS AND FALSE ABOUT THE TYPES. Each identity is +// `PathSegment where brand(...)` -- a refined alias, which has no constructor to seal, so +// sole-constructor admission never applies. Any module may mint one with a cast, and this one +// does: the casts below carry exactly the `..` and `/` that path_segment_is_safe exists to refuse, +// and they compile with zero blocking diagnostics. +// +// This is the consequence that ranks: the two runtime checks are real and are the only thing +// standing, and nothing in the type stops a third branded id from being written without one. + +import std.types { String } +import gunbc.merge_admission_subject { WalkAttemptId } +import gunbc.fleet_known_hosts_anchor { FleetSshAttemptIdentity } + +data forged_attempt_id_escapes_its_directory: WalkAttemptId = "../../etc" as WalkAttemptId + +data forged_ssh_identity_introduces_a_level: FleetSshAttemptIdentity = "a/b" as FleetSshAttemptIdentity + +fn any_string_becomes_an_attempt_id(raw: String) -> WalkAttemptId { raw as WalkAttemptId } diff --git a/dag/test/probe/path_segment_predicate_admission_probe.dag b/dag/test/probe/path_segment_predicate_admission_probe.dag new file mode 100644 index 00000000000..172c51959a2 --- /dev/null +++ b/dag/test/probe/path_segment_predicate_admission_probe.dag @@ -0,0 +1,33 @@ +module test.probe.path_segment_predicate_admission_probe + +// THIS MODULE RESOLVES TODAY, AND THAT IS THE FINDING -- an EXPECTING-RED hole, as its sibling +// test.probe.refinement_seam_admission_probe. +// +// std.types path_segment_safety_note names the whole law: `/` and `\` introduce a level, `.` and +// `..` navigate, CR and LF terminate a record in every line-oriented format this repo writes, NUL +// terminates the string at the syscall boundary. NONE OF IT IS A REFINEMENT PREDICATE. +// `PathSegment = NonEmptyStr where brand("PathSegment")`, and `brand` is on the compiler's +// DEFERRED list (v1.compiler.infer where_refinement_is_deferred_predicate), so PathSegment +// contributes no decidable predicate of its own and inherits only `non_empty` transitively. The +// law itself lives in std.types path_segment_is_safe, an ordinary runtime fn that no seam +// consults. +// +// So of the characters that note calls the law, ZERO are refused at any seam, on any route, in any +// spelling -- INCLUDING a bare literal, which is where every other predicate in this corpus does +// refuse. The blank is the sole refusal, and only because `non_empty` reached it. + +import std.types { String, PathSegment, GlobSegment } + +data navigates_out_of_its_parent: PathSegment = ".." as PathSegment + +data introduces_a_level: PathSegment = "a/b" as PathSegment + +data introduces_a_level_backslash: PathSegment = "a\\b" as PathSegment + +data terminates_a_line_oriented_record: PathSegment = "a\nb" as PathSegment + +data terminates_at_the_syscall_boundary: PathSegment = "a\x00b" as PathSegment + +data a_glob_segment_navigates_too: GlobSegment = ".." as GlobSegment + +fn any_string_becomes_a_segment(raw: String) -> PathSegment { raw as PathSegment } diff --git a/dag/test/probe/refinement_seam_admission_probe.dag b/dag/test/probe/refinement_seam_admission_probe.dag new file mode 100644 index 00000000000..2413c04156a --- /dev/null +++ b/dag/test/probe/refinement_seam_admission_probe.dag @@ -0,0 +1,40 @@ +module test.probe.refinement_seam_admission_probe + +// THIS MODULE RESOLVES TODAY, AND THAT IS THE FINDING. Every construction below puts a value the +// declared refinement forbids into a position declared to hold it, and the compiler admits all of +// them. It is an EXPECTING-RED hole, not a red: the witness asserts the admission, and flips when +// the wall lands (DESIGN 4b(4) -- the probe then becomes the permanent regression control rather +// than retiring). +// +// std.types declares `NonEmptyStr = String where non_empty`. Enforcement lives in +// v1.compiler.infer where_refinement_mismatch_diags, reached from infer_expr wherever an expected +// type is threaded -- but where_refinement_diags_for_predicate DECIDES ONLY WHEN THE VALUE IS A +// LITERAL, and every non-deciding arm emits WhereRefinementUnenforced, whose six reasons are all +// advisory by policy (v1.std.core is_where_refinement_unenforced_advisory_reason). So the wall is +// a property of the SPELLING AT THE SITE, not of the refinement. + +import std.types { String, Int, List, NonEmptyStr, PathSegment } + +// THE #124 SHAPE. A blank element in a List flows into a List parameter with +// no cast. Measured: zero blocking diagnostics AND zero advisory -- the seam produces no +// diagnostic of any severity, which is worse than the advisory seams below. +fn blanks() -> List { ["", "b"] } + +fn take_nonempty_list(xs: List) -> Int { count(xs) } + +fn blank_reaches_a_nonempty_list() -> Int { take_nonempty_list(xs: blanks()) } + +// A ONE-LINE ALIAS DEFEATS THE LITERAL WALL. `data v: PathSegment = "" as PathSegment` REFUSES +// (blocking TypeMismatch, the positive control the witness asserts). The identical construction +// through a local alias of that same type is admitted silently. +type Seg = PathSegment + +data blank_through_an_alias: Seg = "" as Seg + +// The advisory seams: a value that is not a literal is exempt at every position that threads an +// expected type. One WhereRefinementUnenforced advisory each, none of them blocking. +fn take_nonempty(s: NonEmptyStr) -> Int { 1 } + +fn any_string_reaches_a_nonempty_parameter(raw: String) -> Int { take_nonempty(s: raw) } + +fn any_string_becomes_a_nonempty_return(raw: String) -> NonEmptyStr { raw as NonEmptyStr }