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

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,10 @@ import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable }
// refuses that reading at either gate. That removes a standing mechanically-preventable wall,
// so it is declared here rather than landed silently.
//
// WHAT THIS DROP IS NOT. It is not the typed cost-debt constructor. Half two of the same
// change (`v2.workflow.floor_cost_debt_admission` `floor_cost_debt_row`) still refuses a 325ms
// observed reading into the roster, so Roster ground cannot be minted from a margin crossing.
// WHAT THIS DROP IS NOT. It does not cover the Roster ground. A typed admission is
// live-conditioned (`v2.workflow.floor_enrolment_margin` `enrolment_declared_measured_standing`):
// a 325ms reading under the per-subject line leaves it stale and blocking, and a planned Roster
// identity with no reading is NotMeasured, so Roster ground cannot hold on a margin crossing.
// Undeclared new witnesses at 325ms still refuse over the margin. Wall deadline and semantic
// red stay armed. Censored and absent-with-verdict readings still stop the run on
// changed-witness; those walls were not lowered.
Expand Down
2 changes: 1 addition & 1 deletion docs/design-rung-drops.md

Large diffs are not rendered by default.

14 changes: 9 additions & 5 deletions docs/plans/enrolment-margin-eval-step-denomination.md
Original file line number Diff line number Diff line change
Expand Up @@ -171,11 +171,15 @@ are a lower bound with no ceiling, exactly as its CPU is.

## Phase 3 — retire the CPU line, or say why it stays

`required_floor_per_subject_cpu_line_ms` exists only because two per-subject gates still
read a CPU clock. When Phase 2 lands, the enrolment margin is not one of them, and the
remaining consumer is `v2.workflow.floor_cost_debt_admission`. Phase 3 decides that one:
either it is denominated too and the symbol is deleted with its own dissolution
condition discharged, or the symbol survives with a population of exactly one, stated.
`required_floor_per_subject_cpu_line_ms` exists only because per-subject decisions still
read a CPU clock. Since gunbc#11700 `v2.workflow.floor_cost_debt_admission` compares nothing
(a typed admission is identity and reason); the consumers are both in
`v2.workflow.floor_enrolment_margin`: the margin budget, which must sit below the line, and
the live Roster ground (`enrolment_declared_measured_standing`), which admits only a reading
over it. When Phase 2 denominates the margin, the Roster ground is the remaining consumer, and
Phase 3 decides that one: either it is denominated too and the symbol is deleted with its own
dissolution condition discharged, or the symbol survives with a population of exactly one,
stated.

**Only when no per-subject budget reads a run-level figure does the drop's clause (iv)
retire**, and the drop is retired by its trigger and by nothing else.
Expand Down
242 changes: 217 additions & 25 deletions src/v1/stage0/src/cli_run/required_floor_runner.rs

Large diffs are not rendered by default.

404 changes: 383 additions & 21 deletions src/v2/extdeps/languages/dag.dag

Large diffs are not rendered by default.

206 changes: 206 additions & 0 deletions src/v2/test/claim/parse/g0_service_decl_parse_probe_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,206 @@
module v2.test.parse.g0_service_decl_parse_probe

import v2.compiler.normalize { normalize }
import v2.compiler.parse { ParseArtifact, parse_module }
import v2.compiler.tokenize { tokenize }
import v2.extdeps.languages.dag { dag_language_model }
import v2.std.diagnostic { Accepted, Diagnostic, NonEmptyDiagnostics, Outcome, Rejected }
import v2.std.language_model { LanguageModel }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import v2.std.logic { Bool }
import v2.std.node { well_formed }
import v2.std.text { String }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// SH-3: G0 had no service production. v1 parse_service_def expects keyword
// `service`, then a dotted name, then a brace body of operations (and optional
// transport/config). The first native fatal was leftover token `service` at
// dag/extdeps/access/posix_effective_principal_read_op.dag. The family is the
// nest below; service-level `config` and the v2-inline operation form remain
// v1-admitted remainder. Parsing is not lowering: the route rows below pin that a parsed
// service is refused at the normalized-tree door.

data probe_cached_lm: LanguageModel = dag_language_model()

fn parse_src(src: String) -> Outcome<ParseArtifact> {
let lm = probe_cached_lm
match tokenize(text: src, file: ^probe, rules: lm.lex) {
Accepted { value: ts, diagnostics: _ } => parse_module(tokens: ts, grammar: lm.grammar)
Rejected { diagnostics: d } => Rejected { diagnostics: d }
}
}

fn parses(src: String) -> Bool {
match parse_src(src: src) {
Accepted { value: _, diagnostics: _ } => true
Rejected { diagnostics: _ } => false
}
}

fn smallest_service_parsed() -> Outcome<ParseArtifact> {
parse_src(src: smallest_service_source)
}

fn refuses(src: String) -> Bool {
match parses(src: src) {
true => false
false => true
}
}

data fn_control_source: String = "module m\nfn f() -> Int { 1 }\n"

data smallest_service_source: String = "module m\nservice S {\n operation Op {\n input { x: Int }\n output { y: Int from \"y\" }\n readonly\n transport shell { argv: [\"a\"] }\n }\n}\n"

data missing_name_red_source: String = "module m\nservice {\n operation Op { input { x: Int } }\n}\n"

data missing_brace_red_source: String = "module m\nservice S\nfn f() -> Int { 1 }\n"

data unknown_modifier_red_source: String = "module m\nservice S {\n operation Op {\n input { x: Int }\n volatile\n transport shell { argv: [\"x\"] }\n }\n}\n"

data field_default_source: String = "module m\nservice S {\n operation Op {\n input { path: String, max_depth: Int = 1 }\n transport shell { argv: [\"a\"] }\n }\n}\n"

data field_default_without_expr_red_source: String = "module m\nservice S {\n operation Op {\n input { max_depth: Int = }\n }\n}\n"

// The service body of dag/extdeps/access/posix_effective_principal_read_op.dag, the first native
// fatal this family exists to clear: newline-separated output fields, exit, mock_response.
data posix_effective_principal_service_source: String = "module m\nservice access.PosixEffectivePrincipal {\n operation Read {\n input { read: EffectivePosixPrincipalRead }\n output {\n exit_code: Int from \"exit_code\"\n success: Bool from \"exit_success\"\n stdout: String from \"stdout\"\n stderr: String from \"stderr\"\n }\n readonly\n\n transport shell { argv: [\"whoami\"] }\n exit {\n 0 => Unit\n nonzero => String \"whoami failed\"\n }\n mock_response {\n 0 => { exit_code: 1, success: false, stdout: \"\", stderr: \"hermetic effective-principal observation unavailable\" } \"hermetic access.PosixEffectivePrincipal.Read refuses external identity observation\"\n }\n }\n}\n"

data remaining_arms_service_source: String = "module m\nservice S {\n transport rest { base: \"u\" }\n operation Op {\n input { x: Int }\n idempotent\n hermetic\n response {\n 200 => Int\n 404 => String \"missing\"\n }\n }\n}\n"

data exit_entry_without_arrow_red_source: String = "module m\nservice S {\n operation Op {\n exit {\n 0 Unit\n }\n }\n}\n"

// v1 parse_mock_response_entries_acc takes the trailing description as optional, so the
// refusal pinned here is the missing expression, not a missing message.
data mock_entry_without_expr_red_source: String = "module m\nservice S {\n operation Op {\n mock_response {\n 0 =>\n }\n }\n}\n"

// The io field tail is service-scoped: a general type field with a default or a `from` key still
// refuses at parse, and the plain type control shows the refusal is the tail, not the type.
data plain_type_source: String = "module m\ntype T { x: Int }\n"

data type_field_default_red_source: String = "module m\ntype T { x: Int = 1 }\n"

data type_field_from_red_source: String = "module m\ntype T { x: Int from \"k\" }\n"

data keyword_as_name_source: String = "module m\nfn f(from: Int, input: Int) -> Int { let transport = from\n transport + input }\n"

test fn fn_control_still_parses_holds() -> Bool {
parses(src: fn_control_source)
}

test fn smallest_service_parses_holds() -> Bool {
match smallest_service_parsed() {
Accepted { value: _, diagnostics: _ } => true
Rejected { diagnostics: _ } => false
}
}

test fn smallest_service_tree_is_well_formed_holds() -> Bool {
match smallest_service_parsed() {
Accepted { value: a, diagnostics: _ } => well_formed(n: a.tree)
Rejected { diagnostics: _ } => false
}
}

test fn service_without_name_still_refuses_holds() -> Bool {
refuses(src: missing_name_red_source)
}

test fn service_without_brace_still_refuses_holds() -> Bool {
refuses(src: missing_brace_red_source)
}

test fn unknown_operation_modifier_still_refuses_holds() -> Bool {
refuses(src: unknown_modifier_red_source)
}

test fn service_keywords_remain_usable_as_names_holds() -> Bool {
parses(src: keyword_as_name_source)
}

test fn field_default_parses_holds() -> Bool {
parses(src: field_default_source)
}

test fn field_default_without_expr_still_refuses_holds() -> Bool {
refuses(src: field_default_without_expr_red_source)
}

test fn posix_effective_principal_service_parses_holds() -> Bool {
parses(src: posix_effective_principal_service_source)
}

test fn remaining_service_arms_parse_holds() -> Bool {
parses(src: remaining_arms_service_source)
}

test fn exit_entry_without_arrow_still_refuses_holds() -> Bool {
refuses(src: exit_entry_without_arrow_red_source)
}

test fn mock_entry_without_expr_still_refuses_holds() -> Bool {
refuses(src: mock_entry_without_expr_red_source)
}

test fn plain_type_still_parses_holds() -> Bool {
parses(src: plain_type_source)
}

test fn type_field_default_still_refuses_holds() -> Bool {
refuses(src: type_field_default_red_source)
}

test fn type_field_from_key_still_refuses_holds() -> Bool {
refuses(src: type_field_from_red_source)
}

// ROUTE, not only parse. A service parses but has no body-lowering producer yet, so normalize must
// land it on the declared lowered | wrapper-retained frontier (body_lowering_fold
// body_lower_wrapper_retained_shell) and the normalized-tree door must REFUSE it with a typed reason
// (normalized_tree admit_normalized_tree) -- never admit an unlowered service shell to resolve.
// The fn control is the positive half: the same door admits a module with nothing retained.
fn refused_for_retention(ne: NonEmptyDiagnostics) -> Bool {
fold_list(
xs: ne.tail,
empty: ne.head.reason == ^normalized_tree_reason_wrapper_retention_not_normalized,
cons: fn(found, d) { found || d.reason == ^normalized_tree_reason_wrapper_retention_not_normalized }
)
}

fn normalize_refuses_for_retention(src: String) -> Bool {
match parse_src(src: src) {
Rejected { diagnostics: _ } => false
Accepted { value: a, diagnostics: _ } =>
match normalize(parse_tree: a.tree) {
Accepted { value: _, diagnostics: _ } => false
Rejected { diagnostics: r } => refused_for_retention(ne: r)
}
}
}

fn normalize_admits(src: String) -> Bool {
match parse_src(src: src) {
Rejected { diagnostics: _ } => false
Accepted { value: a, diagnostics: _ } =>
match normalize(parse_tree: a.tree) {
Accepted { value: _, diagnostics: _ } => true
Rejected { diagnostics: _ } => false
}
}
}

// The route needs only a service declaration, not a populated one: an empty service still emits
// dag_surface_service_decl with no lowering producer. The populated smallest_service fixture
// measured 396ms here against the 302ms enrolment margin (floor run 35440687934), paying to parse
// and normalize an operation this claim never inspects (DESIGN 3, a witness discriminates at one
// interface).
data empty_service_source: String = "module m\nservice S {}\n"

test fn parsed_service_is_refused_at_the_normalized_tree_door_holds() -> Bool {
normalize_refuses_for_retention(src: empty_service_source)
}

test fn fn_control_is_admitted_at_the_normalized_tree_door_holds() -> Bool {
normalize_admits(src: fn_control_source)
}
Loading
Loading