Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
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
32 changes: 31 additions & 1 deletion dag/gunbc/declaration_index_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -201,6 +201,31 @@ data declaration_index_seed_growth_justification: SeedGrowthJustification = Seed
decl_name: "citation_debt_findings",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.declaration_index",
decl_name: "resolved_roster_findings",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.declaration_index",
decl_name: "citation_field_suffix",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.declaration_index",
decl_name: "NEXT_RUNG_TRIGGER_CITATIONS",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.declaration_index",
decl_name: "next_rung_trigger_citation_findings",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.declaration_index",
decl_name: "next_rung_trigger_citation_findings_against",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.declaration_index",
decl_name: "cited_symbol_findings",
Expand Down Expand Up @@ -325,11 +350,16 @@ data declaration_index_seed_growth_justification: SeedGrowthJustification = Seed
module_path: "v1_compiler.tests.declaration_index_integrity",
decl_name: "a_second_citation_of_an_enrolled_target_in_another_declaration_still_refuses",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.tests.declaration_index_integrity",
decl_name: "a_next_rung_trigger_that_resolves_is_the_stamp_firing_not_a_lost_control",
field: WholeDeclaration
}
],
reason: "WHY RUST IS STILL NEEDED, and it is a REACHABILITY limit rather than a modeling gap: the subject is INGESTION -- the moment a .dag file is read off the filesystem and parsed -- and the only ingestion that executes today is host Rust. A .dag witness cannot reach it: run_required_floor's hermetic envelope refuses host effects during preparation, so a witness whose subject is a filesystem walk is counted executed while its assertion never runs. Asserting the index's behaviour from a mocked file tree would assert the mock, which is the specification-without-execution trap, so the construction and its discriminating evidence both have to live where the walk does.\n\nTHE CONSEQUENCE OF REFUSING IT, stated second because it is not the admitting argument: there is no second executing ingestion to re-home this to, so a refusal would leave both of DESIGN's next-rung triggers -- section 6's module-authorship trigger and section 3's cited-symbol restoration trigger -- undischargeable until v2 is the compiler.\n\nWHAT THE GROWTH BUYS, at identity grain rather than as a category: three walls on one construction, replacing one deleted corpus-walk census and two obligations that had no mechanism at all. It also NETS DOWN inside claim_executor, which loses the --required-cited-symbol mode and its three helper functions.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete all 62 when INGESTION is itself modeled -- when the .dag source walk and the per-module record it derives are expressed as a .dag operation over a typed filesystem transport, the index becomes an ordinary substrate fold and these declarations move to the substrate. A PARTIAL migration IS admissible and is the expected shape: the moment the RECORD DERIVATION is modeled (record_from_module is a pure function of one parse tree and needs no host effect at all), the record builder and every finding function follow it, while the directory walk and the parse-clean plumbing stay behind for as long as the WALK is host-only; delete those on the second step. What does NOT dissolve them is the checks moving to another host entry point, and what does NOT dissolve them is a hermetic witness asserting a fabricated module tree -- that would retire the evidence while retiring nothing it guards.",
trigger: "Delete all 68 when INGESTION is itself modeled -- when the .dag source walk and the per-module record it derives are expressed as a .dag operation over a typed filesystem transport, the index becomes an ordinary substrate fold and these declarations move to the substrate. A PARTIAL migration IS admissible and is the expected shape: the moment the RECORD DERIVATION is modeled (record_from_module is a pure function of one parse tree and needs no host effect at all), the record builder and every finding function follow it, while the directory walk and the parse-clean plumbing stay behind for as long as the WALK is host-only; delete those on the second step. What does NOT dissolve them is the checks moving to another host entry point, and what does NOT dissolve them is a hermetic witness asserting a fabricated module tree -- that would retire the evidence while retiring nothing it guards.",
current_boundary: "src/v1/stage0/src/declaration_index.rs; src/v1/stage0/src/cli_run.rs run_dag_parse_sweep; src/v1/stage0/tests/declaration_index_integrity.rs; src/v1/stage0/src/bin/claim_executor.rs; src/v1/stage0/src/bin/v1_src_dag_parse.rs; dag/gunbc/declaration_index_seed_growth.dag"
}

Expand Down
34 changes: 28 additions & 6 deletions dag/gunbc/fabric/fabric_witness_run.dag
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ import product.fabric.work {
ExecutionRequirements, Shape, HardRequirements, CapacityClass, ControlPlaneCapacity,
CapabilityManifestRef, TrustDomainRef,
ProgramRef, SourceManifestRef, ArtifactManifestRef, EffectContractRef, OutputContractRef,
declared_output_obligations_from_manifests,
declared_terminal_obligations,
work_for,
}
import std.content_hash { ContentHash, content_hash_of_value, serialize_content_hash }
Expand Down Expand Up @@ -159,6 +161,10 @@ fn action_ref_material(action: ActionRef) -> NonEmptyStr {
concat("action:", concat(framed_string(value: action.owner), concat(framed_string(value: action.repo), framed_string(value: action.ref))))
}

// Opaque contract name. Obligations are the structured field —
// they used to be framed into the OutputContractRef string (content-serialised
// meaning fork). Deleting that encoding is the cut; the roster no longer hides
// in a name.
fn required_build_contract_from_materials(
source: NonEmptyStr,
checkout: NonEmptyStr,
Expand All @@ -168,8 +174,8 @@ fn required_build_contract_from_materials(
environment: NonEmptyStr,
cache: NonEmptyStr,
credentials: NonEmptyStr,
outputs: NonEmptyStr,
terminal: NonEmptyStr,
output_manifest: List<NonEmptyStr>,
terminal_result_manifest: List<NonEmptyStr>,
) -> WorkContract {
WorkContract {
program: concat("gunbc.required-witnesses-build.program:", framed_string(value: command)),
Expand All @@ -182,7 +188,11 @@ fn required_build_contract_from_materials(
inputs: concat("gunbc.required-witnesses-build.inputs:", concat(framed_string(value: environment), concat(framed_string(value: cache), framed_string(value: credentials)))),
runtime_closure: concat("gunbc.required-witnesses-build.runtime:", concat(framed_string(value: toolchain), framed_string(value: executable))),
effect_contract: "gunbc.required-witnesses-build.effects.checkout-read-cache-and-permitted-credentials-only",
output_contract: concat("gunbc.required-witnesses-build.outputs:", concat(framed_string(value: outputs), framed_string(value: terminal))),
output_contract: "gunbc.required-witnesses-build.outputs",
output_obligations: declared_output_obligations_from_manifests(
artifacts: output_manifest,
terminals: terminal_result_manifest,
),
}
}

Expand All @@ -208,12 +218,23 @@ fn bind_required_witnesses_build_work(
Absent => RequiredBuildWorkRefused { cause: RequiredBuildCoordinateMissing { coordinate: "permitted-credential-refs" } }
Present { value: credentials } => match non_empty_strings_material(label: "outputs", values: spec.output_manifest) {
Absent => RequiredBuildWorkRefused { cause: RequiredBuildCoordinateMissing { coordinate: "output-manifest" } }
Present { value: outputs } => match non_empty_strings_material(label: "terminal", values: spec.terminal_result_manifest) {
Present { value: _ } => match non_empty_strings_material(label: "terminal", values: spec.terminal_result_manifest) {
Absent => RequiredBuildWorkRefused { cause: RequiredBuildCoordinateMissing { coordinate: "terminal-result-manifest" } }
Present { value: terminal } => {
Present { value: _ } => {
let source = concat("git-source:", concat(framed_string(value: git_object_id_wire_hex(oid: subject.commit)), framed_string(value: git_object_id_wire_hex(oid: subject.tree))))
let command = command_material(command: spec.command)
let contract = required_build_contract_from_materials(source: source, checkout: checkout, toolchain: toolchain, executable: executable, command: command, environment: environment, cache: cache, credentials: credentials, outputs: outputs, terminal: terminal)
let contract = required_build_contract_from_materials(
source: source,
checkout: checkout,
toolchain: toolchain,
executable: executable,
command: command,
environment: environment,
cache: cache,
credentials: credentials,
output_manifest: spec.output_manifest,
terminal_result_manifest: spec.terminal_result_manifest,
)
let requirements = floor_execution_requirements()
let work = work_for(principal: principal, contract: contract, requirements: requirements)
RequiredBuildWorkBound {
Expand Down Expand Up @@ -390,6 +411,7 @@ fn floor_work_contract(source: SourceManifestRef) -> WorkContract {
runtime_closure: "gunbc.toolchain.rust-1.93.0+clippy+rustfmt",
effect_contract: "gunbc.floor.effects.read-only-corpus",
output_contract: "gunbc.floor.outputs.required-floor-summary",
output_obligations: declared_terminal_obligations(ids: ["required-floor-summary"]),
}
}

Expand Down
Loading
Loading