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
50 changes: 50 additions & 0 deletions dag/gunbc/namespace/namespace_step0_canary.dag
Original file line number Diff line number Diff line change
Expand Up @@ -199,6 +199,56 @@ fn namespace_step0_unavailable_receipt(
}
}

// THE STEP-0 PRODUCER'S OWN CONSTRUCTOR, and the one the freeze note above reserved for it: "the
// eventual strip producer must own a separate constructor whose inputs are the executed rewrite and
// its observation". Its inputs are exactly that -- the statements a typed source rewrite actually
// removed, and the cause the containment compile of the rewritten sources actually reported. It
// cannot be reached from the fixtures' caller seal and the fixtures cannot be reached from here, so
// production and fixture mint through disjoint doors and neither can stand in for the other.
//
// IT IS DECLARED HERE BECAUSE NamespaceStep0CanaryReceipt IS sole_constructor. Ownership of the
// production route is expressed by the caller seal, not by which file the constructor sits in: the
// only caller admitted is the producer's fold, so no other module -- and no future witness -- can
// mint a subject-entered receipt.
//
// THE ARGUMENTS IT REFUSES TO INVENT. A producer that stripped nothing has no observation, and
// passing an empty list here would mint a receipt the classifier refuses at ObservedSubjectField
// rather than one that quietly claims entry; the producer refuses before reaching this row instead.
// Likewise a containment compile that COMPLETED has no blocking cause, and there is no argument
// here that could express it -- which is why the producer's refusal coproduct carries that case.
fn namespace_step0_strip_applied_receipt(
contract_identity: NonEmptyStr,
source_commit: GitObjectId,
source_tree: GitObjectId,
compiler_program: NonEmptyStr,
compiler_executable_sha256: Sha256Digest,
input_subject_manifest: NonEmptyStr,
observed_tree: GitObjectId,
observed_import_statements: List<NonEmptyStr>,
containment_compile_cause: NonEmptyStr
) -> NamespaceStep0CanaryReceipt
admit_callers: [
decl_ref(module_path: "gunbc.namespace_step0_strip_producer", decl_name: "namespace_step0_strip_receipt")
]
= NamespaceStep0CanaryReceipt {
contract_identity: contract_identity,
source_commit: source_commit,
source_tree: source_tree,
compiler_program: compiler_program,
compiler_executable_sha256: compiler_executable_sha256,
input_subject_manifest: input_subject_manifest,
completed_production_prefix: [CanaryContractFrozen, SourceTreePinned, CompilerExecutablePinned, InputSubjectManifestPinned, TypedImportStripApplied],
first_blocking_transition: CompileContainmentResolution,
first_blocking_cause: ContainmentCompileObservationRefused { cause: containment_compile_cause },
subject_entry: Step0SubjectEntered,
observation_completeness: Step0ObservationIncomplete,
observed_subject: Step0StripObservation {
observed_tree: observed_tree,
observed_manifest: input_subject_manifest,
observed_import_statements: observed_import_statements
}
}

// Admission is intentionally exact and narrow, but it is NOT frozen to today's frontier. The two
// coherent shapes are today's stop at the strip and the next possible stop after a real strip has
// entered the subject. That makes a longer prefix and a different blocker fixture-authorable now,
Expand Down
225 changes: 225 additions & 0 deletions dag/gunbc/namespace/namespace_step0_strip_producer.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,225 @@
module gunbc.namespace_step0_strip_producer

import std.types { Int, List, NonEmptyStr, String }
import std.content_hash { Sha256Digest }
import std.import {
ImportStripOutcome,
ImportStatementsStripped,
ImportStripRefused,
ImportStripRefusal,
ParsedImportStatement,
ParsedImportStatements,
ImportStatementsParsed,
ImportStatementParseRefused,
strip_import_statements,
}
import extdeps.git.object_store { GitObjectId }
import gunbc.parsed_import_statement_production { parsed_import_statements_live }
import gunbc.compile_diagnostic_census { CompileDiagnosticCensusRow }
import tools.multi_module_compile_fixture {
FixtureSource,
MultiModuleCompileFixture,
MultiModuleCompileFixtureOutcome,
FixtureInstrumentRefused,
FixtureCompileRefused,
FixtureCompileCompleted,
compile_fixture,
}
import gunbc.namespace_step0_canary {
NamespaceStep0CanaryReceipt,
namespace_step0_canary_contract,
namespace_step0_manifest_identity,
namespace_step0_strip_applied_receipt,
}

// THE OWNED STEP-0 PRODUCER. It applies the typed import strip to a supplied subject and folds the
// compile observation that follows it, and those two acts are the two capabilities the frozen canary
// names as missing (gunbc.namespace_step0_canary namespace_step0_unavailable_receipt: "a typed
// parse-level source rewrite that removes one complete import statement" and "an owned Step-0
// producer that applies the rewrite and folds the resulting compile observation").
//
// EVERY STAGE REFUSES RATHER THAN WIDENS. A source whose imports did not parse is not a source with
// no imports; a span set the rewrite would not accept is not a clean rewrite; a subject in which
// nothing was removed did not enter the Step 0 subject. Each is a typed, located cause here, and
// none of them can reach the receipt constructor -- which is why that constructor takes the removed
// statements and the compile's own cause as arguments rather than deriving them.
//
// AND A COMPLETED CONTAINMENT COMPILE IS A REFUSAL HERE, WHICH IS THE OPPOSITE OF A FAILURE. The
// canary's receipt has exactly two blocking transitions and no spelling for "nothing blocked", so a
// stripped subject that COMPILES has no honest receipt on this carrier. Minting one anyway would be
// fabricating a blocker that did not occur; reporting it as its own refusal cause is how the day
// Step 0 actually succeeds becomes visible instead of being rendered as a stall.
//
// WHAT THIS PRODUCER DOES NOT ESTABLISH, stated because a receipt must not claim coverage it does
// not have. It observes the sources it was HANDED. That the handed vector is the whole of the tree
// the receipt names is the caller's obligation and is bound only by the canary's commit and tree
// pins; nothing here can check it. The next-rung trigger is a capability that COLLECTS the subject
// from the pinned tree, so the vector and the tree have one producer instead of two.

type Step0StripProductionRefusalCause
= Step0SourceImportsNotParsed {
file: NonEmptyStr
cause: NonEmptyStr
}
| Step0SourceRewriteRefused {
file: NonEmptyStr
refusal: ImportStripRefusal
}
| Step0SubjectHadNoImportStatements
| Step0ContainmentCompileInstrumentRefused {
cause: NonEmptyStr
}
| Step0ContainmentCompileCompleted {
module_count: Int
}

type Step0StripProduction
= Step0ReceiptProduced {
receipt: NamespaceStep0CanaryReceipt
}
| Step0StripProductionRefused {
cause: Step0StripProductionRefusalCause
}

// One source, rewritten. The parse observation and the rewrite are two different authorities and
// both can refuse, so the two refusals stay apart: a parse that never ran and a span set the
// rewrite rejected have different owners and different repairs.
type Step0SourceStrip
= Step0SourceStripped {
source: FixtureSource
removed_statements: List<String>
}
| Step0SourceStripRefused {
cause: Step0StripProductionRefusalCause
}

fn namespace_step0_strip_source(source: FixtureSource) -> Step0SourceStrip {
match parsed_import_statements_live(file: source.path as String, source: source.content) {
ImportStatementParseRefused { cause: cause } =>
Step0SourceStripRefused { cause: Step0SourceImportsNotParsed { file: source.path, cause: cause } }
ImportStatementsParsed { statements: statements } =>
match strip_import_statements(
source_file: source.path as String,
source: source.content,
statements: statements
) {
ImportStripRefused { refusal: refusal } =>
Step0SourceStripRefused { cause: Step0SourceRewriteRefused { file: source.path, refusal: refusal } }
ImportStatementsStripped { rewritten_source: rewritten, removed_statements: removed } =>
Step0SourceStripped {
source: FixtureSource { path: source.path, content: rewritten },
removed_statements: removed
}
}
}
}

// The absorbing arm is the refusal, and the first one is the one reported: a later source cannot
// repair an earlier one, and continuing would compile a subject already known to be unstripped.
type Step0StripFold
= Step0StripFolding {
sources: List<FixtureSource>
removed_statements: List<String>
}
| Step0StripFoldHalted {
cause: Step0StripProductionRefusalCause
}

fn namespace_step0_strip_fold_step(fold: Step0StripFold, source: FixtureSource) -> Step0StripFold {
match fold {
Step0StripFoldHalted { cause: cause } => Step0StripFoldHalted { cause: cause }
Step0StripFolding { sources: sources, removed_statements: removed } =>
match namespace_step0_strip_source(source: source) {
Step0SourceStripRefused { cause: cause } => Step0StripFoldHalted { cause: cause }
Step0SourceStripped { source: stripped, removed_statements: source_removed } =>
Step0StripFolding {
sources: sources |> list_push(stripped),
removed_statements: concat(removed, source_removed)
}
}
}
}

fn namespace_step0_strip_subject(sources: List<FixtureSource>) -> Step0StripFold {
sources |> fold(
init: Step0StripFolding { sources: [], removed_statements: [] },
f: (fold, source) => namespace_step0_strip_fold_step(fold: fold, source: source)
)
}

// The compile observation, folded to the one thing the canary's carrier can say about it: whether
// containment resolution refused, and with what cause. The instrument's three arms stay apart
// because a broken harness, a refusing subject and a passing subject have different owners: only
// the middle one is an observation of containment resolution at all.
type Step0ContainmentObservation
= Step0ContainmentResolutionRefused {
cause: NonEmptyStr
}
| Step0ContainmentObservationUnavailable {
cause: Step0StripProductionRefusalCause
}

fn namespace_step0_containment_refusal_text(diagnostics: List<CompileDiagnosticCensusRow>) -> NonEmptyStr {
concat(
"containment resolution of the import-stripped subject refused with ",
concat(to_string(count(diagnostics |> filter(d => d.blocking))), " blocking diagnostic(s)")
) as NonEmptyStr
}

fn namespace_step0_observe_containment(
outcome: MultiModuleCompileFixtureOutcome
) -> Step0ContainmentObservation {
match outcome {
FixtureInstrumentRefused { cause: cause } =>
Step0ContainmentObservationUnavailable { cause: Step0ContainmentCompileInstrumentRefused { cause: cause } }
FixtureCompileCompleted { module_count: module_count, emitted_files: _, diagnostics: _, source_digest: _, compiler_digest: _ } =>
Step0ContainmentObservationUnavailable { cause: Step0ContainmentCompileCompleted { module_count: module_count } }
FixtureCompileRefused { module_count: _, diagnostics: diagnostics, source_digest: _, compiler_digest: _ } =>
Step0ContainmentResolutionRefused { cause: namespace_step0_containment_refusal_text(diagnostics: diagnostics) }
}
}

// THE FOLD, and the only caller the receipt constructor admits. Its arguments are the executed
// rewrite (the statements actually removed) and the observation that followed it (the containment
// compile's own cause); it invents neither.
//
// THE COMPILER IS ONE FACT AND ARRIVES FROM ONE CALLER. compiler_program travels beside
// compiler_executable_sha256 rather than being spelled here, because which program was run and
// which bytes it had are two halves of one observation about one dispatch; a literal here would
// make this module a second authority on the first half while the caller owned the second, and the
// two could then disagree with nothing to notice (review 58952).
fn namespace_step0_strip_receipt(
source_commit: GitObjectId,
source_tree: GitObjectId,
compiler_program: NonEmptyStr,
compiler_executable_sha256: Sha256Digest,
sources: List<FixtureSource>,
entry: NonEmptyStr
) -> Step0StripProduction {
match namespace_step0_strip_subject(sources: sources) {
Step0StripFoldHalted { cause: cause } => Step0StripProductionRefused { cause: cause }
Step0StripFolding { sources: stripped, removed_statements: removed } =>
if count(removed) == 0 {
Step0StripProductionRefused { cause: Step0SubjectHadNoImportStatements }
} else {
match namespace_step0_observe_containment(
outcome: compile_fixture(fixture: MultiModuleCompileFixture { sources: stripped, entry: entry })
) {
Step0ContainmentObservationUnavailable { cause: cause } =>
Step0StripProductionRefused { cause: cause }
Step0ContainmentResolutionRefused { cause: containment_cause } =>
Step0ReceiptProduced { receipt: namespace_step0_strip_applied_receipt(
contract_identity: namespace_step0_canary_contract.identity,
source_commit: source_commit,
source_tree: source_tree,
compiler_program: compiler_program,
compiler_executable_sha256: compiler_executable_sha256,
input_subject_manifest: namespace_step0_manifest_identity(),
observed_tree: source_tree,
observed_import_statements: removed |> map(statement => statement as NonEmptyStr),
containment_compile_cause: containment_cause
) }
}
}
}
}
24 changes: 24 additions & 0 deletions dag/gunbc/namespace/parsed_import_statement_bridge_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
module gunbc.parsed_import_statement_bridge_seed_growth

import std.decl_ref { DeclarationRef, WholeDeclaration }
import std.types { String }
import gunbc.roadmap_model { RoadmapNodeId }
import gunbc.seed_growth { SeedGrowthJustification }

// Seed-growth obligation for the host bridge that carries the v1 parser's import-statement extents
// to the dag consumers that rewrite them. Homed beside the obligation it declares rather than in
// gunbc.seed_growth_admission, which owns the roster and the join.

data parsed_import_statement_bridge_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef {
module_path: "v1_interpreter",
decl_name: "parsed_import_statements_value",
field: WholeDeclaration
}
],
reason: "WHY A HOST BRIDGE RATHER THAN A .dag CONSUMER CALLING THE PRODUCER DIRECTLY, and it is the same reachability limit gunbc.namespace_structural_observation_bridge_seed_growth records. The statements are delimited by v1.compiler.parse parse_import_statement_extents -- the parser reading its own token consumption -- and the required floor resolves --source-root dag --source-root src/v2 only. Measured over the whole corpus: NO dag module imports a v1 module, so a consumer under dag cannot name that producer at all.\n\nWHAT THE BRIDGE IS AND IS NOT. It is a TRANSPORT: one in-memory source in, the parse's own observation out, encoded into std.import's carrier. It reads no repository file, needs no module index, and is hermetic by construction. It decides nothing -- where a statement starts and stops is decided by the parser, and what to do with that region is decided by std.import strip_import_statements. The single hand declaration is the encoder, and it encodes a coproduct rather than a list precisely so that 'the parse refused' and 'this module has no imports' cannot become one value at the boundary.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits by PURPOSE -- does the change serve the v2 self-host program. The import-deletion program is that program's current frontier, and gunbc.namespace_step0_canary records that Step 0 is blocked at ApplyTypedImportStrip for want of exactly this capability.\n\nHAND-ITEM DELTA: +1, the encoder named above, a free function in src/v1/stage0/src/v1_interpreter.rs and therefore citable as WholeDeclaration with no impl-method class. The dispatch arm is a new match arm inside the existing eval_builtin_inner macro, an ExistingSeedItemModified rather than a new declaration, and v1_interpreter_dispatch_generated.rs is generated from gunbc.v1_interpreter_primitive_surface. src/v1/02_parse.dag, dag/std/import.dag and src/v1/gunbc/parsed_import_statements.dag are substrate changes whose Rust mirrors are emitted.",
owning_dissolution_lane: "namespace-structural-observations" as RoadmapNodeId,
trigger: "Delete it when a dag consumer can obtain one in-memory source's parsed import statements WITHOUT a host bridge -- that is, when the parse that delimits them is reachable from a consumer whose resolution roots include the compiler that produces it, and the delimited statements for one source are obtainable there. What does NOT dissolve it is the required floor gaining src/v1 as a source root on its own: that is an artifact and can land while the producer is still unreachable from any executing consumer. The capability this bridge supplies is ONE IN-MEMORY SOURCE'S IMPORT STATEMENTS DELIMITED BY THE ORDINARY PARSE INSIDE AN EXECUTING CONSUMER, and the trigger is satisfied only when something else supplies exactly that.",
current_boundary: "src/v1/stage0/src/v1_interpreter.rs free_call.parsed_import_statements arm and its encoder; dag/gunbc/namespace/parsed_import_statement_production.dag; dag/gunbc/v1/v1_interpreter_primitive_surface.dag roster row; src/v1/04_method.dag builtin signature; dag/std/primitives.dag spelling roster"
}
19 changes: 19 additions & 0 deletions dag/gunbc/namespace/parsed_import_statement_production.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
module gunbc.parsed_import_statement_production

import std.import { ParsedImportStatements }
import std.types { String }

// THE PRODUCTION SEAM FOR PARSED IMPORT STATEMENTS, AND IT IS A TRANSPORT RATHER THAN AN AUTHORITY.
//
// The statements are delimited by v1.compiler.parse parse_import_statement_extents -- the parser
// reading its own consumption -- and carried in std.import's vocabulary. No module under dag
// imports a v1 module anywhere in the corpus, and the required floor resolves `dag` and `src/v2`
// only, so a dag consumer cannot name that producer at all; this row is the one crossing.
//
// IT DECIDES NOTHING. One in-memory source in, the parse's own observation out. It reads no
// repository file and consults no module index, so a witness on it is hermetic. If a policy
// question ever arises about WHICH sources to ask about, it belongs in the caller.

fn parsed_import_statements_live(file: String, source: String) -> ParsedImportStatements {
parsed_import_statements(file: file, source: source)
}
2 changes: 2 additions & 0 deletions dag/gunbc/seed_growth_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ import gunbc.claim_batch_function_preflight_seed_growth { claim_batch_function_p
import gunbc.declaration_index_seed_growth { declaration_index_seed_growth_justification }
import gunbc.emitted_closure_compile_seed_growth { emitted_closure_compile_seed_growth_justification }
import gunbc.namespace_structural_observation_bridge_seed_growth { namespace_structural_observation_bridge_seed_growth_justification }
import gunbc.parsed_import_statement_bridge_seed_growth { parsed_import_statement_bridge_seed_growth_justification }
import gunbc.namespace_wave_admission { namespace_wave_admission_seed_growth_justification }
import gunbc.parse_refusal_location_seed_growth { parse_refusal_location_seed_growth_justification }
import gunbc.qualified_pipe_callee_seed_growth { qualified_pipe_callee_seed_growth_justification }
Expand Down Expand Up @@ -215,6 +216,7 @@ fn seed_growth_justification_roster() -> List<SeedGrowthJustification> {
declaration_index_seed_growth_justification,
emitted_closure_compile_seed_growth_justification,
namespace_structural_observation_bridge_seed_growth_justification,
parsed_import_statement_bridge_seed_growth_justification,
namespace_wave_admission_seed_growth_justification,
qualified_pipe_callee_seed_growth_justification,
target_invocation_seed_growth_justification,
Expand Down
Loading
Loading