Skip to content
Merged
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
214 changes: 214 additions & 0 deletions src/v2/lens/realization_vocabulary_containment.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,214 @@
// src/v2/lens/realization_vocabulary_containment.dag
// Scope: realization-vocabulary containment guard (DESIGN §3/§4/§5). Target-AST construction
// vocabulary — the hand-rolled per-language bash AST sidecar
// `extdeps.languages.bash.program` (ShellStmt/ShellWord/serialize_bash) and any future
// per-language AST sidecar — may be imported ONLY at the REALIZATION EDGE:
// (a) the extdeps/languages/** language models, and
// (b) the emit fold (05_emit / 06_translate / self_host candidate_generation),
// where `emit(intent, Bash)` selects a realization (DESIGN §4: emit = serialize_target ∘
// translate, one grammar read backward). Anywhere else, importing the sidecar AST is a
// `RealizationVocabularyLeak` — authoring target-language construction inside CONSUMER code
// forks the row-driven emit (DESIGN §2: N models, not N×M adapters). Making that import
// unwritable in consumer code is the construction wall behind "shell(intent()) is a
// realization-edge feature, never authored inside consumer code".
//
// MECHANISM (N+M — NOT a new lens mechanism): a SIBLING rule over the SAME host-enumerated
// `v2.lens.layering_imports.LayerImportFact{layer, path, import_module}` rows. The predicate
// reads `import_module` (∈ the sidecar vocabulary) and `path` (∉ realization-edge ∧ ∉ the
// exception roster); `layer` is unused (path is the discriminator here).
//
// RATCHET — honest, fail-closed, SHRINKING. The current importers go RED today, so this cannot
// ship as an instant green wall. They are carried in `realization_vocab_exception_roster`, a
// NAMED exception roster that only shrinks. The roster is NOT a license to add importers —
// a NEW (unrostered) non-edge importer goes RED immediately.
// dissolve-on: the bash-sidecar arc (warm-badger-46 shell(intent()) → emit(intent, Bash))
// migrates each rostered consumer off `serialize_bash`; as each lands, drop it from the
// roster. When the roster empties, this guard is a PURE WALL and
// extdeps.languages.bash.program is deletable (its terminal step — NOT this lens's job).
//
// Consumer (executable, §5): the live witnesses under
// src/v2/test/claim/realization_vocabulary_containment/ — floor-auto-discovered `test fn`s
// that scan the real tree by execution (the clean-tree green pass + the planted-leak RED
// receipt), plus the hardcoded-fact lens-unit discriminators.

module v2.lens.realization_vocabulary_containment

import v2.lens.layering_imports {
LayerImportFact,
layer_import_facts_live
}
import v2.std.algebra {
fold_list,
is_empty,
is_prefix_of,
length,
list_snoc_item
}
import v2.std.collection { List }
import v2.std.logic { Bool }
import v2.std.text { Char, String }

// ── single-authority policy data ──────────────────────────────────────────────

// Target-AST construction vocabulary: the per-language AST sidecar module(s). Today only the
// bash sidecar exists; a future per-language sidecar is added here (one row), not a new lens.
data target_ast_vocab_modules: List<String> = [
"extdeps.languages.bash.program"
]

// Realization-edge allowset (repo-relative path PREFIXES). The only places that may import the
// sidecar AST: the language models (extdeps/languages/**, incl. the sidecar's own home) and the
// emit fold where a realization is selected.
data realization_edge_path_prefixes: List<String> = [
"dsl/extdeps/languages/",
"src/v2/extdeps/languages/",
"src/v2/compiler/05_emit",
"src/v2/compiler/06_translate",
"src/v2/compiler/self_host/candidate_generation"
]

// SHRINKING exception roster — the consumer modules that import the sidecar TODAY (verified by
// `grep -rln 'extdeps.languages.bash.program' dsl src/v2 | grep -v _test | grep -v
// 'extdeps/languages/bash'`). Each migrates off serialize_bash under warm-badger-46; drop it
// here when it lands. DO NOT ADD ROWS — a new non-edge importer is a RealizationVocabularyLeak.
data realization_vocab_exception_roster: List<String> = [
"dsl/gunbc/ci_spec.dag",
"dsl/gunbc/ci_yaml_validate.dag",
"dsl/tools/build_step.dag",
"dsl/tools/dsl_compile_clean_transport.dag",
"dsl/tools/emit_host_transport.dag",
"dsl/tools/host_prelude.dag",
"dsl/tools/layering_imports_transport.dag",
"dsl/tools/resolved_imports_transport.dag",
"src/v2/workflow/compiler_closure_ingest_transport.dag",
"src/v2/workflow/source_root_ingest_transport.dag"
]

// Consumer-source scan roots for the live clean-tree witness: every layer that holds (or could
// hold) consumer code, EXCLUDING the test trees (fixtures planted under src/v2/test/** import
// the sidecar by design and are scanned in isolation by the RED receipt, never here).
data realization_vocab_consumer_scan_roots: List<String> = [
"dsl/std",
"dsl/extdeps",
"dsl/compiler",
"dsl/tools",
"dsl/gunbc",
"src/v2/std",
"src/v2/extdeps",
"src/v2/compiler",
"src/v2/workflow",
"src/v2/lens"
]

// One violation row.
type RealizationVocabularyLeak {
path: String
import_module: String
}

data empty_realization_vocab_leaks: List<RealizationVocabularyLeak> = []

// ── predicate ─────────────────────────────────────────────────────────────────

fn char_eq(a: Char, b: Char) -> Bool {
a == b
}

fn list_contains_str(xs: List<String>, target: String) -> Bool {
fold_list(
xs: xs,
empty: false,
cons: fn(acc, s) { acc || (s == target) }
)
}

fn path_has_any_prefix(prefixes: List<String>, path: String) -> Bool {
fold_list(
xs: prefixes,
empty: false,
cons: fn(acc, p) { acc || is_prefix_of(prefix: p, xs: path, eq: char_eq) }
)
}

fn module_is_target_ast_vocab(module: String) -> Bool {
list_contains_str(xs: target_ast_vocab_modules, target: module)
}

fn path_is_realization_edge(path: String) -> Bool {
path_has_any_prefix(prefixes: realization_edge_path_prefixes, path: path)
}

// A leak: imports the sidecar AST vocabulary, is NOT a realization-edge module, and is NOT
// carried by the (shrinking) exception roster. Roster is an explicit parameter so a witness can
// prove the ratchet shrinks honestly (drop a member → its live import goes RED).
fn is_realization_vocab_leak(fact: LayerImportFact, roster: List<String>) -> Bool {
module_is_target_ast_vocab(module: fact.import_module)
&& (path_is_realization_edge(path: fact.path) == false)
&& (list_contains_str(xs: roster, target: fact.path) == false)
}

// ── scan / count / holds ────────────────────────────────────────────────────────

fn scan_facts_for_leaks(
facts: List<LayerImportFact>,
roster: List<String>
) -> List<RealizationVocabularyLeak> {
fold_list(
xs: facts,
empty: empty_realization_vocab_leaks,
cons: fn(acc, fact) {
if is_realization_vocab_leak(fact: fact, roster: roster) {
list_snoc_item(
xs: acc,
item: RealizationVocabularyLeak {
path: fact.path,
import_module: fact.import_module
}
)
} else {
acc
}
}
)
}

fn realization_vocab_leak_count(
facts: List<LayerImportFact>,
roster: List<String>
) -> Int {
length(xs: scan_facts_for_leaks(facts: facts, roster: roster))
}

fn realization_vocab_containment_holds(
facts: List<LayerImportFact>,
roster: List<String>
) -> Bool {
is_empty(xs: scan_facts_for_leaks(facts: facts, roster: roster))
}

// ── canonical-roster convenience (binds the single-authority roster) ──────────────

fn realization_vocab_leak_count_canonical(facts: List<LayerImportFact>) -> Int {
realization_vocab_leak_count(facts: facts, roster: realization_vocab_exception_roster)
}

fn realization_vocab_containment_holds_canonical(facts: List<LayerImportFact>) -> Bool {
realization_vocab_containment_holds(facts: facts, roster: realization_vocab_exception_roster)
}

// ── live projection (reuses the layering host enumerator — layer tag unused) ──────

// Scan the given roots (consumer source by default) through the SAME host enumerator the
// layering lens uses, then apply the canonical-roster leak predicate. `extdeps_roots: []` —
// the std/extdeps layer split is irrelevant here, the path discriminator carries the rule.
fn realization_vocab_leak_count_live(scan_roots: List<String>) -> Int {
realization_vocab_leak_count_canonical(
facts: layer_import_facts_live(std_roots: scan_roots, extdeps_roots: [])
)
}

fn realization_vocab_containment_clean_live(scan_roots: List<String>) -> Bool {
realization_vocab_containment_holds_canonical(
facts: layer_import_facts_live(std_roots: scan_roots, extdeps_roots: [])
)
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
// Scope: live clean-tree witness — the realization-vocabulary containment guard, run by
// EXECUTION over the real consumer-source tree (the §5 green-by-execution pass, not a
// spec-only lens). Every current importer of the bash-AST sidecar is either a
// realization-edge module or carried by realization_vocab_exception_roster, so the live
// scan over the consumer-source roots must report ZERO leaks. A NEW (unrostered)
// non-edge importer added anywhere under these roots makes this go RED.

module v2.test.realization_vocabulary_containment.clean_tree

import v2.lens.realization_vocabulary_containment {
realization_vocab_consumer_scan_roots,
realization_vocab_leak_count_live,
realization_vocab_containment_clean_live
}
import v2.std.logic { Bool }

test fn realization_vocab_clean_tree_holds() -> Bool {
realization_vocab_containment_clean_live(scan_roots: realization_vocab_consumer_scan_roots)
&& (realization_vocab_leak_count_live(scan_roots: realization_vocab_consumer_scan_roots) == 0)
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
// Scope: lens-unit discriminators for v2.lens.realization_vocabulary_containment over
// HARDCODED LayerImportFact rows (no live tree). The §5 discriminating set:
// (1) a fresh NON-edge module importing the sidecar AST → RED (count 1);
// (2) a realization-edge module importing it → clean (count 0);
// (3) a rostered consumer importing it → clean (count 0);
// (4) the same rostered consumer with the member REMOVED → RED (count 1)
// — proves the ratchet shrinks honestly (de-roster ⇒ its import goes red);
// (5) a non-vocabulary import from a non-edge module → clean (count 0).

module v2.test.realization_vocabulary_containment.lens_unit.discriminators

import v2.lens.layering_imports { LayerImportFact }
import v2.lens.realization_vocabulary_containment {
realization_vocab_leak_count,
realization_vocab_leak_count_canonical
}
import v2.std.collection { List }
import v2.std.layer { LayerPrefixStd, LayerPrefixExtdeps }
import v2.std.logic { Bool }
import v2.std.text { String }

data sidecar_module: String = "extdeps.languages.bash.program"

// (1) fresh non-edge importer → RED under the canonical roster.
data fresh_leak_facts: List<LayerImportFact> = [
LayerImportFact {
layer: LayerPrefixStd,
path: "dsl/tools/_perturb_fresh_consumer.dag",
import_module: sidecar_module
}
]

test fn fresh_non_edge_import_is_leak_holds() -> Bool {
realization_vocab_leak_count_canonical(facts: fresh_leak_facts) == 1
}

// (2) realization-edge module (extdeps/languages/**) → NOT a leak (the allowset).
data edge_import_facts: List<LayerImportFact> = [
LayerImportFact {
layer: LayerPrefixExtdeps,
path: "src/v2/extdeps/languages/bash.dag",
import_module: sidecar_module
}
]

test fn realization_edge_import_is_not_leak_holds() -> Bool {
realization_vocab_leak_count_canonical(facts: edge_import_facts) == 0
}

// (3) a rostered consumer (host_prelude) → NOT a leak while rostered.
data rostered_import_facts: List<LayerImportFact> = [
LayerImportFact {
layer: LayerPrefixStd,
path: "dsl/tools/host_prelude.dag",
import_module: sidecar_module
}
]

test fn rostered_consumer_import_is_not_leak_holds() -> Bool {
realization_vocab_leak_count_canonical(facts: rostered_import_facts) == 0
}

// (4) the SAME rostered consumer, but the roster with host_prelude REMOVED → RED.
// Proves the roster is load-bearing: de-rostering a still-importing consumer goes red.
data roster_without_host_prelude: List<String> = [
"dsl/gunbc/ci_spec.dag",
"dsl/gunbc/ci_yaml_validate.dag",
"dsl/tools/build_step.dag",
"dsl/tools/dsl_compile_clean_transport.dag",
"dsl/tools/emit_host_transport.dag",
"dsl/tools/layering_imports_transport.dag",
"dsl/tools/resolved_imports_transport.dag",
"src/v2/workflow/compiler_closure_ingest_transport.dag",
"src/v2/workflow/source_root_ingest_transport.dag"
]

test fn de_rostered_consumer_import_is_leak_holds() -> Bool {
realization_vocab_leak_count(
facts: rostered_import_facts,
roster: roster_without_host_prelude
) == 1
}

// (5) negative control: a non-edge module importing a NON-vocabulary module → clean.
data non_vocab_import_facts: List<LayerImportFact> = [
LayerImportFact {
layer: LayerPrefixStd,
path: "dsl/tools/_perturb_fresh_consumer.dag",
import_module: "extdeps.shell"
}
]

test fn non_vocabulary_import_is_not_leak_holds() -> Bool {
realization_vocab_leak_count_canonical(facts: non_vocab_import_facts) == 0
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
// Scope: scanner-execution RED receipt — the live containment guard must flag the planted
// non-edge consumer that imports the bash-AST sidecar
// (src/v2/test/fixture/realization_vocab_scan/leak/plant.dag). The discriminating RED
// input that goes red when the live detection breaks: scanning the fixture dir in
// isolation MUST report exactly one RealizationVocabularyLeak (and not-clean). This is
// the by-execution oracle that the guard fires on a real, committed leak.

module v2.test.realization_vocabulary_containment.scanner.planted_leak

import v2.lens.realization_vocabulary_containment {
realization_vocab_leak_count_live,
realization_vocab_containment_clean_live
}
import v2.std.collection { List }
import v2.std.logic { Bool }
import v2.std.text { String }

data planted_leak_scan_roots: List<String> = [
"src/v2/test/fixture/realization_vocab_scan/leak"
]

test fn realization_vocab_planted_leak_detected_holds() -> Bool {
(realization_vocab_leak_count_live(scan_roots: planted_leak_scan_roots) == 1)
&& (realization_vocab_containment_clean_live(scan_roots: planted_leak_scan_roots) == false)
}
9 changes: 9 additions & 0 deletions src/v2/test/fixture/realization_vocab_scan/leak/plant.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
// FIXTURE — a planted NON-edge consumer module that imports the bash-AST sidecar vocabulary
// (`extdeps.languages.bash.program`). It is NOT a realization-edge module (path is not under
// extdeps/languages/** nor the emit fold) and is NOT in realization_vocab_exception_roster, so
// the realization-vocabulary containment guard MUST flag it as a RealizationVocabularyLeak.
// Read as TEXT by v2.lens.layering_imports.layer_import_facts_live (never module-resolved); the
// by-execution RED control that the guard actually fires. DO NOT import this module, and DO NOT
// add this path to the roster.
module v2.test.fixture.realization_vocab_scan.leak_plant
import extdeps.languages.bash.program { ShellStmt }
Loading