Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 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
1 change: 1 addition & 0 deletions _internal/INVARIANTS_OPS.md
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX
| `src/v3/compiler/tests/integration/dissolution_subsumption_carrier_test.rs` | **Design contract:** `docs/design-dissolution-lens.md` §11.2 (`DissolutionSubsumption` carrier with `subsumed_fixes: Set<DiffId>` set semantics + `SubsumptionVerification` coproduct). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + the matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the parse-level carrier ratchet. **Dissolution:** remove when `src/v4/lens/subsumption.dag` is exercised by `.dag` `TestClaim` rows or a generated harness that mechanically reads the carrier and first subsumption row without this host parser check. **Interim ratchet:** `dissolution_subsumption_carrier_shape_locked` parses `src/v4/lens/subsumption.dag` and asserts the `DiffId` / `TestClaimId` / `ProducerStageId` handles, the `MechanicalReverification | ProducerStageDerivation` verification coproduct, and the `DissolutionSubsumption { root_fix: DiffId, subsumed_fixes: Set<DiffId>, verification: SubsumptionVerification }` carrier shape (with the legacy non-empty `SubsumedFixes` / `ProducerStageDerivationPath` wrappers explicitly absent). `dissolution_subsumption_first_row_is_mechanical_reverification` asserts the first data row pins `affected_set_irt1_frontier_root_fix`, references the named `affected_set_irt1_subsumed_fixes` Set binding, and uses `MechanicalReverification` against `affected_set_irt1_leaf_claim_suite`. `affected_set_irt1_subsumed_fixes_membership_predicate_enumerates_six_leaves` asserts the `fn affected_set_irt1_subsumed_fixes_value() -> Set<DiffId>` helper that backs the named `affected_set_irt1_subsumed_fixes` data row references the six `affected_set_*_leaf_fix` `Symbol` handles in its `Set { member: fn(d) { … } }` predicate. `affected_set_irt1_leaf_claim_suite_authored_for_mechanical_reverification` parses `irt1_leaf_claim_suite.dag` and asserts the aggregate `TestClaim` row for the `affected_set_irt1_leaf_claim_suite` handle. |
| `src/v3/compiler/tests/integration/extdeps_sql_transport_test.rs` | **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row `T-PB-B` / `pb_rust_tests_outside_residual_zero`; this Rust integration receipt keeps HTTP/SQL/audit extdeps compiled by the existing v3 parser before downstream emission-target consumers rely on them. **Dissolution:** remove when extdeps transport and Phase 3 emission-target files are covered by a `.dag`-native parse/authority suite or generated test harness rather than per-file Rust `compile_to_dag` probes. **Interim ratchet:** `rest_transport_dag_compiles_cleanly` and `sql_transport_dag_compiles_cleanly` pin `dsl/extdeps/transports/rest.dag` and `dsl/extdeps/transports/sql.dag`; `http_server_extdep_dag_compiles_cleanly`, `sql_migration_extdep_dag_compiles_cleanly`, and `audit_cloudevents_extdep_dag_compiles_cleanly` pin `dsl/extdeps/http/server.dag`, `dsl/extdeps/sql/migration.dag`, and `dsl/extdeps/audit/cloudevents.dag` as parseable staged emission-target substrate. The field-sensitive companions (`http_server_target_fields_are_authoritative_substrate_edges`, `sql_migration_target_fields_bound_raw_sql_scaffold`, `audit_cloudevents_target_fields_preserve_core_names`) consume the new target-contract fields directly so they fail on raw `String`/`Int` regressions, missing SQL scaffold bounds, or CloudEvents alias drift while the first real projection consumer is still staged; the audit ratchet also locks CloudEvents core fields to branded carriers and `std.types.Timestamp` rather than raw strings. |
| `src/v3/compiler/tests/integration/v4_extdeps_coordination_dag_smoke_test.rs` | **TASKS.md** T-4.8 (`src/v4/extdeps/coordination.dag` — multi-program coordination as effect-typed Bind composition; PR #3207 decomposed shape with `WireContractFacts` carrying `ExchangePattern` / parameterized `SettlementGuarantee<SettleBound>` / `ConsistencyGuarantee<ConvergeBound>`, `CoordinationBind` carrying the tracked `CoordinationEffectKind` bridge, and WIRECONTRACT-OBLIGATION-TABLE-T4.8 per-effect obligation rows routed through the same guarantee discriminants with `Required*Bound` payload types rather than fabricated concrete bounds). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness; SG-0 census net +1 pairing `(c)` is mechanically prepended via `scripts/ci-merge/sg0-pr-body-append.3590.txt` in CI. **Dissolution:** remove when `src/v4/extdeps/coordination.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust parse ratchet. **Interim ratchet:** `v4_extdeps_coordination_dag_parses`; `v4_extdeps_coordination_wire_contract_uses_decomposed_facts`; `v4_extdeps_coordination_effect_kind_has_obligation_table` tokenize/parse the pinned `include_str!` source and assert the decomposed `WireContractFacts` fields, `WireContract { facts, bind }`, tracked `CoordinationEffectKind` arms, parameterized `CoordinationEffectObligation` field types, all four obligation table entries and exchange mappings, list-literal table surface, and the `coordination_effect_obligation` / `wire_contract_obligation_table_t4_8` function surfaces. |
| `src/v3/compiler/tests/integration/v4_extdeps_openapi_dag_smoke_test.rs` | **TASKS.md** T-4.6 (`src/v4/extdeps/formats/openapi.dag` — OpenAPI 3.1 wire-contract facts; SL-3229-OPENAPI-WIRECONTRACT-COORDINATION carries `OpenApiOperationWireContractFacts.coordination: OpenApiHttpWireContractFacts` (Http-only witness carrier); `WireContractFacts` derived only via `openapi_http_wire_contract_facts_to_coordination` / Outcome constructors sourcing `coordination_effect_obligation(Http)` (`ImmediateSettlement` / `NoReplicaConvergence` accepted; bounded required guarantees fail-closed via `Outcome`/`Rejected`). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `openapi.dag` wire-contract composition is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust parse ratchet. **Interim ratchet:** `v4_extdeps_openapi_dag_parses`; `v4_extdeps_openapi_operation_wire_contract_composes_coordination_facts` tokenize/parse the pinned source and assert `OpenApiOperationWireContractFacts` embeds `WireContractFacts`, Http obligation sourcing, Http-only settlement/consistency projection with fail-closed bounded arms, absence of parallel `RequestReply` witness / `steps:0` coercion, and `Outcome<WireContractFacts>` composition into `WireContract`. |
| `src/v3/compiler/tests/integration/v4_extdeps_react_dag_smoke_test.rs` | **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-4.7 (`src/v4/extdeps/frameworks/react.dag`, React 19.2.0–pinned framework substrate). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/extdeps/frameworks/react.dag` (or the v4 extdeps fixture set it belongs to) is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_react_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
| `src/v3/compiler/tests/integration/v4_extdeps_file_system_dag_smoke_test.rs` | **TASKS.md** T-4.5 / Wave-2-C2 (`src/v4/extdeps/file_system.dag` — external file-system resource + modeled read/write effects; Practice 11 companion: no `import v4.std.node`, no `NodeFileBinding`; POSIX substrate exports retained for `posix.dag` / `testgen.dag`). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `file_system.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust probe. **Interim ratchet:** `v4_extdeps_file_system_dag_tokenizes_and_parses` plus Practice-11 companion tests (parse-surface import/type bans, POSIX-grounded `FilePath`, per-operation receipt record shapes, Wave-2 `ModeledFileEffects.file_read`/`file_write` arrow signatures + legacy `FileSystemOperations` / request-carrier coexistence). |
| `src/v3/compiler/tests/integration/v4_p9_llvm_instruction_cost_single_owner_test.rs` | **P9 single-owner (R2-1):** replaces dissolved `v4_lens_cost_dag_smoke_test.rs` ratchet — `fn llvm_instruction_cost` must appear exactly once under `src/v4/`, in `src/v4/lens/cost.dag` (whole-tree parse does **not** substitute; see `docs/v4-close-interrogation.md` §P5(b) / `feature:p9-llvm-instruction-cost-single-owner`). Complements `.dag` TestClaim `src/v4/test/claim/lens_cost/p9_llvm_instruction_cost_registry_owner.dag` (registry exclusivity). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the harness. **Dissolution:** remove when M2 reflection or generated harness executes the `.dag` claim over the full v4 corpus without this host file-walk ratchet. **Interim ratchet:** `v4_p9_llvm_instruction_cost_defined_only_in_lens_cost_dag` walks `src/v4/**/*.dag` for `fn llvm_instruction_cost`; `v4_p9_llvm_instruction_cost_absent_from_llvm_ir_dag` asserts `llvm_ir.dag` does not re-author the cost table. |
Expand Down
3 changes: 3 additions & 0 deletions scripts/ci-merge/sg0-pr-body-append.3869.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
SG-0 hand-path delta: +1

SG-0 pairing: (c) dispatch for P5(b) net +1 on `EXPECTED_HAND_AUTHORED_TEST` (`v4_extdeps_openapi_dag_smoke_test.rs`); concrete dispatch evidence: `docs/briefs/r4-program-dispatch-plan.md` T-4.6 / SL-3229 OpenAPI wire-contract row. Primary checkable lane cite is `_internal/ROADMAP_OPS.md` Nine lanes row T-PB-B / `pb_rust_tests_outside_residual_zero` with same-PR `_internal/INVARIANTS_OPS.md` SG-0 hand-authored integration test receipts table row for that path. T-4.6 context: `src/v4/extdeps/formats/openapi.dag` SL-3229-OPENAPI-WIRECONTRACT-COORDINATION; retire when OpenAPI operation wire-contract facts are exercised by `.dag` `TestClaim` rows or a generated harness without this host Rust parse ratchet.
2 changes: 2 additions & 0 deletions src/v3/compiler/tests/integration.rs
Original file line number Diff line number Diff line change
Expand Up @@ -289,6 +289,8 @@ mod v4_compiler_parse_table_dag_smoke_test;
mod v4_extdeps_coordination_dag_smoke_test;
#[path = "integration/v4_extdeps_file_system_dag_smoke_test.rs"]
mod v4_extdeps_file_system_dag_smoke_test;
#[path = "integration/v4_extdeps_openapi_dag_smoke_test.rs"]
mod v4_extdeps_openapi_dag_smoke_test;
#[path = "integration/v4_extdeps_react_dag_smoke_test.rs"]
mod v4_extdeps_react_dag_smoke_test;
#[path = "integration/v4_lens_affected_set_dag_smoke_test.rs"]
Expand Down
2 changes: 2 additions & 0 deletions src/v3/compiler/tests/integration/sg0_census_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -855,6 +855,8 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[
// T-4.8 coordination substrate: decomposed WireContractFacts + CoordinationBind shape,
// with WIRECONTRACT-OBLIGATION-TABLE-T4.8 per-effect obligation rows.
"src/v3/compiler/tests/integration/v4_extdeps_coordination_dag_smoke_test.rs",
// T-4.6 openapi wire-contract composition with coordination.dag (SL-3229-OPENAPI-WIRECONTRACT-COORDINATION).
"src/v3/compiler/tests/integration/v4_extdeps_openapi_dag_smoke_test.rs",
// T-4.7 React framework substrate: `compile_to_dag` smoke on
// `src/v4/extdeps/frameworks/react.dag` (zero module diagnostics).
// SG-0 ratchet per INVARIANTS §P5(b) + typescript extdeps precedent.
Expand Down
140 changes: 140 additions & 0 deletions src/v3/compiler/tests/integration/v4_extdeps_openapi_dag_smoke_test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,140 @@
//! **Layer:** integration
//!
//! T-4.6 / SL-3229-OPENAPI-WIRECONTRACT-COORDINATION ratchet for
//! `src/v4/extdeps/formats/openapi.dag`: `OpenApiOperationWireContractFacts`
//! carries `OpenApiHttpWireContractFacts` (Http-only witness carrier); coordination
//! `WireContractFacts` is derived only via `openapi_http_wire_contract_facts_to_coordination`.
//!
//! **PR receipt (P5 Mechanism (b)):** this harness + matching
//! `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` + INVARIANTS table
//! row land in the same PR.

use v3_compiler::parse_for_test;
use v3_compiler::parse_surface::{SurfaceField, SurfaceItem, SurfaceType, TypeAngleArg};
use v3_compiler::tokenize_for_test;

const OPENAPI_DAG: &str = include_str!("../../../../v4/extdeps/formats/openapi.dag");
const OPENAPI_PATH: &str = "src/v4/extdeps/formats/openapi.dag";

fn openapi_surface_or_panic() -> v3_compiler::parse_surface::SurfaceModule {
let tokens = tokenize_for_test(OPENAPI_DAG, OPENAPI_PATH)
.unwrap_or_else(|e| panic!("{OPENAPI_PATH}: tokenize: {e:?}"));
parse_for_test(&tokens, OPENAPI_PATH).unwrap_or_else(|e| panic!("{OPENAPI_PATH}: parse: {e:?}"))
}

fn type_record_fields<'a>(
module: &'a v3_compiler::parse_surface::SurfaceModule,
name: &str,
) -> &'a [SurfaceField] {
module
.items
.iter()
.find_map(|item| match item {
SurfaceItem::TypeRecord {
name: item_name,
fields,
..
} if item_name == name => Some(fields.as_slice()),
_ => None,
})
.unwrap_or_else(|| panic!("missing type record {name}"))
}

fn surface_type_name(ty: &SurfaceType) -> String {
match ty {
SurfaceType::Named { name, .. } => name.clone(),
SurfaceType::Parameterized { name, args, .. } => {
let rendered = args
.iter()
.map(|arg| match arg {
TypeAngleArg::TypeExpr { ty } => surface_type_name(ty),
TypeAngleArg::WidthNatLiteral { decimal, .. } => decimal.clone(),
})
.collect::<Vec<_>>()
.join(", ");
format!("{name}<{rendered}>")
}
SurfaceType::Optional { inner, .. } => format!("?{}", surface_type_name(inner)),
SurfaceType::Arrow { .. } => "fn".to_string(),
}
}

fn record_field_type(fields: &[SurfaceField], name: &str) -> String {
fields
.iter()
.find(|field| field.name == name)
.map(|field| surface_type_name(&field.ty))
.unwrap_or_else(|| panic!("missing field {name}"))
}

#[test]
fn v4_extdeps_openapi_dag_parses() {
let _module = openapi_surface_or_panic();
}

#[test]
fn v4_extdeps_openapi_operation_wire_contract_composes_coordination_facts() {
let module = openapi_surface_or_panic();
let facts = type_record_fields(&module, "OpenApiOperationWireContractFacts");
assert_eq!(
record_field_type(facts, "coordination"),
"OpenApiHttpWireContractFacts"
);
let http_facts = type_record_fields(&module, "OpenApiHttpWireContractFacts");
assert_eq!(
record_field_type(http_facts, "http_exchange"),
"OpenApiHttpRequestReplyWitness"
);
assert_eq!(
record_field_type(http_facts, "http_settlement"),
"OpenApiHttpImmediateSettlementWitness"
);
assert_eq!(
record_field_type(http_facts, "http_consistency"),
"OpenApiHttpNoReplicaConvergenceWitness"
);
assert_eq!(
record_field_type(facts, "admitted_method"),
"OpenApiAdmittedHttpMethod"
);
assert_eq!(
record_field_type(facts, "path_template"),
"OpenApiPathTemplateKey"
);
assert!(
OPENAPI_DAG.contains("fn openapi_http_obligation() -> CoordinationEffectObligation")
&& OPENAPI_DAG.contains("coordination_effect_obligation(effect: Http)"),
"OpenAPI wire-contract facts must source the Http obligation row from coordination.dag"
);
assert!(
OPENAPI_DAG.contains("fn openapi_http_settlement_from_obligation(")
&& OPENAPI_DAG.contains("ImmediateSettlement => Accepted { value: ImmediateSettlement")
&& OPENAPI_DAG.contains("openapi_http_bounded_settlement_not_admitted"),
"Http settlement must project ImmediateSettlement from the obligation row and fail-closed on bounded required settlement"
);
assert!(
OPENAPI_DAG.contains("fn openapi_http_consistency_from_obligation(")
&& OPENAPI_DAG.contains("NoReplicaConvergence => Accepted { value: NoReplicaConvergence")
&& OPENAPI_DAG.contains("openapi_http_bounded_consistency_not_admitted"),
"Http consistency must project NoReplicaConvergence from the obligation row and fail-closed on bounded required consistency"
);
assert!(
!OPENAPI_DAG.contains("data openapi_operation_exchange_request_reply")
&& !OPENAPI_DAG.contains("wire_contract_settlement_from_obligation")
&& !OPENAPI_DAG.contains("SettleBound { steps: 0 }"),
"OpenAPI must not carry a parallel RequestReply witness, generic obligation coercion with fabricated bounds, or steps:0 stubs"
);
assert!(
OPENAPI_DAG.contains("type OpenApiHttpWireContractFacts {")
&& OPENAPI_DAG.contains("fn openapi_http_wire_contract_facts_to_coordination(")
&& OPENAPI_DAG.contains("fn openapi_http_wire_contract_facts(")
&& OPENAPI_DAG.contains("-> Outcome<OpenApiHttpWireContractFacts>")
&& OPENAPI_DAG.contains("fn openapi_operation_wire_contract_facts(")
&& OPENAPI_DAG.contains("-> Outcome<OpenApiOperationWireContractFacts>")
&& OPENAPI_DAG.contains("fn openapi_operation_wire_contract(")
&& OPENAPI_DAG.contains("facts: openapi_http_wire_contract_facts_to_coordination(facts: facts.coordination)")
&& OPENAPI_DAG.contains("bind: BindRef")
&& OPENAPI_DAG.contains("bind: openapi_http_coordination_bind(bind: bind)"),
"OpenApi operation WireContract must use Http-only fact carrier and derive coordination WireContractFacts in the constructor path only"
);
}
Loading
Loading