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
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
{
"content_hash": "3b62a12fa613afa8fd26dc4d5577b5597bf59f5e01d0aaf170b151fe754b7516",
"content_hash": "107ae56109f33854c4e35d0d7a095af544fd86b95efb9206f932420c08a889fe",
"contract_id": "experiment-capture-spec-v1",
"last_change": {
"content_hash": "3b62a12fa613afa8fd26dc4d5577b5597bf59f5e01d0aaf170b151fe754b7516",
"summary": "Add the distinct materialization-attestation reference kind to portable artifact joins; it never replaces the original scenario-snapshot identity (#1241)."
"content_hash": "107ae56109f33854c4e35d0d7a095af544fd86b95efb9206f932420c08a889fe",
"summary": "Constrain required evidence media types to registered, content-provable output contracts (#1401)."
},
"schema_path": "contracts/schemas/experiment-core/experiment-capture-spec-v1.json",
"stability": "draft"
Expand Down
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
{
"content_hash": "ec16ef507c579c16f81e499965255e1ac013f2826bc0b975f1413ce79cb70b74",
"content_hash": "643052d648a1afd04f50e70f0127cc467bf20084156754aceec5964a78529d81",
"contract_id": "sdl-authoring-input-v1",
"last_change": {
"summary": "Add participant-local outcomes and identity assignment alongside opt-in bounded shared-time guarantees.",
"content_hash": "ec16ef507c579c16f81e499965255e1ac013f2826bc0b975f1413ce79cb70b74"
"content_hash": "643052d648a1afd04f50e70f0127cc467bf20084156754aceec5964a78529d81",
"summary": "Constrain required evidence media types to registered, content-provable output contracts (#1401)."
},
"schema_path": "contracts/schemas/sdl/sdl-authoring-input-v1.json",
"stability": "draft"
Expand Down
12 changes: 12 additions & 0 deletions contracts/schemas/experiment-core/experiment-capture-spec-v1.json
Original file line number Diff line number Diff line change
Expand Up @@ -1407,6 +1407,18 @@
],
"level": "error",
"validator": "raes_contracts.contracts.ExperimentCaptureSpecModel._validate_capture_spec"
},
{
"description": "Every required media type must have a registered content-proof path and be supported by its declared output_contract.",
"id": "capture-media-type-provable",
"inputs": [
{
"contract_id": "experiment-capture-spec-v1",
"instance_path": "#/capture_requirements"
}
],
"level": "error",
"validator": "raes_contracts.contracts.ExperimentCaptureRequirementModel._validate_capture_requirement"
}
],
"x-raes-plane": "authored_evidence_requirement",
Expand Down
12 changes: 12 additions & 0 deletions contracts/schemas/sdl/sdl-authoring-input-v1.json
Original file line number Diff line number Diff line change
Expand Up @@ -27415,6 +27415,18 @@
"type": "object",
"x-raes-document-phase": "normalized-authoring-object",
"x-raes-invariants": [
{
"description": "Every declared required evidence media type must have a registered content-proof path; an explicit output_contract must support every declared type.",
"id": "required-evidence-media-type-provable",
"inputs": [
{
"contract_id": "sdl-authoring-input-v1",
"instance_path": "#/evidence_requirements"
}
],
"level": "error",
"validator": "raes.evidence_requirements.EvidenceRequirement._validate_capture_intent"
},
{
"description": "Generated artifact output names and paths, consumers, and dependency entries must be unique, and generated artifact consumers must be read-only. Explicit selections must name declared consumer-selectable outputs; SSH artifact consumers must select outputs and every consumer-selectable SSH output must be selected.",
"id": "stateful-generated-artifact-semantics",
Expand Down
45 changes: 45 additions & 0 deletions docs/migration/required-capture-admission.md
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,51 @@ validated requirement-to-artifact bindings.
Historical `satisfies_refs`, payload summaries, and backend assertions remain
metadata; they are not proof of emitted content.

## Media-type coherence (issue #1401)

Required capture currently has a closed, JSON-based output-proof vocabulary.
Until a separately governed byte contract and verifier exist for another
encoding, the eligible media types are `application/json` and the registered
array-root `application/jsonl` encoding. Reject an entire authored
SDL `media_types` list or experiment `expected_media_types` list if any member
is unsupported; a supported alternative must not mask an impossible one.
`text/plain`, `application/x-ndjson`, and PCAP are therefore invalid required
capture declarations. This tightens earlier SDL authoring behavior, including
the PCAP example in the DSL-124 test, and needs an explicit authoring diagnostic.
An omitted SDL media-type list remains unconstrained on this dimension.

The authoritative eligibility source is
`raes_contracts.evidence_output_validation.evidence_output_registrations()`:
registry resolution couples each output-contract id to its published schema,
semantic validator, and JSON root, from which the supported encodings derive.
An explicit SDL `output_contract` or a
capture-spec `output_contract` must resolve there, and every declared media
type must be valid for that specific contract. An SDL requirement with no
output contract retains its existing intent-only semantics, but its declared
media types must still belong to the union of eligible encodings. In particular,
`application/jsonl` cannot be paired with the object-root
`experiment-evidence-record-v1`. Neither that record contract nor an arbitrary
`application/json` label licenses unrelated JSON or text artifact bytes.

Keep one eligibility rule shared by SDL and capture-spec validation and the
existing offer and content validators. The model validators must expose an
explicit unsupported-media or incompatible-contract error; the published SDL,
capture-spec, and backend-manifest schemas and their semantic-invariant metadata
must not imply broader eligibility. Preserve the existing atomic offer matcher,
admission diagnostics, bounded byte reader, checksum and locator checks, schema
and semantic validation, RFC 6901 field checks, and process-local proof object.
The field selectors address the decoded JSON document; for JSON Lines they
address the decoded array. Do not interpret them as selectors into arbitrary
text, or use an evidence-record envelope as a stand-in for the artifact bytes.

This decision governs required-capture proof, not descriptive legacy
`supported_media_types` summaries, runtime capture implementation, storage,
export, or a generic non-JSON contract framework. A future encoding belongs as
an explicit registry-owned contract/encoding plus bounded byte parser and
content proof, with publication and conformance evidence before it becomes
eligible at authoring or in an offer. No URI fetch, credential handling, or
serialized proof token is introduced here.

## Shared proof and extension points

Issue #1237 makes `validate_experiment_run_evidence()` and
Expand Down
1 change: 1 addition & 0 deletions docs/requirements/DSL-124/requirement.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,3 +37,4 @@ Scenario authors may need to require that particular data be captured from parti
- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_contracts/capture_dimensions.py` (Shared authored capture dimension projection)
- TESTS → TEST `implementations/python/tests/test_issue_1237_capture_dimensions.py` (Independent authored demand projection and admission parity)
- TESTS → TEST `implementations/python/tests/test_issue_1112_capture_admission.py` (Authored evidence demand admission and non-demand boundaries)
- TESTS → TEST `implementations/python/tests/test_issue_1401_media_type_coherence.py` (Authored required media types reject unprovable encodings)
1 change: 1 addition & 0 deletions docs/requirements/EXP-707/requirement.md
Original file line number Diff line number Diff line change
Expand Up @@ -28,3 +28,4 @@ Requirement inventory expansion. Experiment data capture requirements are distin
- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_contracts/contracts/experiment_capture.py` (Field- and output-contract-qualified capture requirements)
- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_processor/trial_compiler/inputs.py` (Digest-bound capture specification admission)
- TESTS → TEST `implementations/python/tests/test_sce_002_trial_compiler.py` (Capture specification identity and backend admission tests)
- TESTS → TEST `implementations/python/tests/test_issue_1401_media_type_coherence.py` (Required media declarations reject unprovable encodings and accept content-provable JSON encodings)
1 change: 1 addition & 0 deletions docs/requirements/EXP-708/requirement.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,3 +54,4 @@ Requirement inventory expansion. Raw captured evidence must be modeled explicitl
- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_contracts/contracts/experiment_conditions.py` (Condition matching excludes unsupported evidence-id claims)
- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_contracts/evidence_satisfaction.py` (Content-backed emitted evidence satisfaction validation)
- TESTS → TEST `implementations/python/tests/test_issue_1112_capture_admission.py` (Evidence record, artifact byte, digest, and field proof coverage)
- TESTS → TEST `implementations/python/tests/test_issue_1401_media_type_coherence.py` (Registered media declarations reach content-backed evidence proof)
1 change: 1 addition & 0 deletions docs/requirements/EXP-715/requirement.md
Original file line number Diff line number Diff line change
Expand Up @@ -42,3 +42,4 @@ Requirement inventory expansion. Observation support must be declared explicitly
- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_conformance/conformance/target_manifest_probe.py` (Fail-closed capture-offer manifest conformance validation)
- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_processor/capture_admission.py` (Conjunctive required-capture capability admission)
- TESTS → TEST `implementations/python/tests/test_issue_1112_capture_admission.py` (Capture-offer manifest and admission failure coverage)
- TESTS → TEST `implementations/python/tests/test_issue_1401_media_type_coherence.py` (Every eligible media declaration can be represented by a valid capture offer)
158 changes: 158 additions & 0 deletions docs/research/formal-semantic-validation/analysis-v67.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
{
"analysis_id": "issue-1401-analysis-v67",
"claim": {
"allowed_evidence": [
"production parser and semantic-validator results",
"canonical compiled digests",
"participant contract regression tests",
"pinned protocol, corpus, and execution snapshot"
],
"claim_id": "asr-530-formal-semantic-validation-retest",
"disallowed_evidence": [
"schema success as semantic proof",
"workflow reachability as network or exploit reachability",
"FM labels as gate outcomes",
"attribution as counterfactual proof",
"formal prose or maintainer confidence alone"
],
"evidence_artifacts": [
"docs/research/formal-semantic-validation/protocol-v2.json",
"docs/research/formal-semantic-validation/corpus/manifest-v4.json",
"docs/research/formal-semantic-validation/execution-snapshot-v67.json",
"docs/research/formal-semantic-validation/evidence/finite-domain-satisfiable-v4.json",
"docs/research/formal-semantic-validation/evidence/finite-domain-unsatisfiable-v4.json",
"docs/research/formal-semantic-validation/evidence/typed-exploit-path-valid-v4.json",
"docs/research/formal-semantic-validation/evidence/typed-exploit-path-invalid-v4.json"
],
"falsification_protocol": "Replay every retained and new case through its production entrypoint, require complete digest and evidence joins, execute participant fixtures, and derive status from the recorded outcomes.",
"objective_fail_criteria": "A supported negative passes, a positive fails, an observation drifts, a required participant case is missing, or weaker evidence is promoted to solver, exploit-path, runtime-stability, or counterfactual assurance.",
"objective_pass_criteria": "Every claim class has positive and negative cases, all supported cases reproduce the frozen outcome, every participant obligation has passing positive and negative fixtures, and unsupported classes remain untested.",
"statement": "At the recorded source-state digest, the retained RAES controls have the bounded statuses recorded here; historical releases are integrity evidence, not current replay evidence.",
"threats_to_validity": [
"The issue-specific corpus is intentionally small and does not enumerate every validator invariant.",
"The participant fixtures exercise reference production contracts and tests, not every independent backend realization.",
"The replay gate runs on one Python reference configuration and one pinned RAES revision.",
"Unsupported solver-level classes have protocol cases but no executable observations."
]
},
"claim_results": [
{
"case_count": 2,
"claim_class_id": "schema-validity",
"evidence_status": "demonstrated",
"limitations": [
"Bounded to the named source/model structural controls."
],
"matching_case_count": 2,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 0
},
{
"case_count": 4,
"claim_class_id": "semantic-consistency",
"evidence_status": "partial",
"limitations": [
"Partial coverage of named static semantics and participant obligations, not universal consistency."
],
"matching_case_count": 4,
"participant_obligation_count": 7,
"replayable_case_count": 4,
"unsupported_case_count": 0
},
{
"case_count": 2,
"claim_class_id": "graph-reachability",
"evidence_status": "partial",
"limitations": [
"Partial workflow control-flow reachability only; not network, service, or exploit reachability."
],
"matching_case_count": 2,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 0
},
{
"case_count": 4,
"claim_class_id": "constraint-satisfiability",
"evidence_status": "demonstrated",
"limitations": [
"Demonstrated only for raes-finite-domain-satisfiability-v1 and its pinned solver configuration."
],
"matching_case_count": 4,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 2
},
{
"case_count": 4,
"claim_class_id": "exploit-path-validity",
"evidence_status": "demonstrated",
"limitations": [
"Demonstrated only for the admitted snapshot, typed graph, query, semantics, and bounded search profile."
],
"matching_case_count": 4,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 2
},
{
"case_count": 2,
"claim_class_id": "determinism-stability",
"evidence_status": "partial",
"limitations": [
"Partial parse-to-compile repeatability only; runtime and backend determinism are untested."
],
"matching_case_count": 2,
"participant_obligation_count": 0,
"replayable_case_count": 2,
"unsupported_case_count": 0
},
{
"case_count": 2,
"claim_class_id": "counterfactual-necessity",
"evidence_status": "untested",
"limitations": [
"Untested because no governed intervention or ablation entrypoint ran."
],
"matching_case_count": 2,
"participant_obligation_count": 0,
"replayable_case_count": 0,
"unsupported_case_count": 2
}
],
"corpus_revision": "4.0.0",
"evidence_status": "partial",
"execution_id": "issue-1401-execution-v67",
"generated_at": "2026-09-30T22:41:24.312224+00:00",
"limitations": [
"Satisfiability is limited to raes-finite-domain-satisfiability-v1 and its exact translation, theory, and Z3 configuration.",
"The subset-minimal unsatisfiable core is not a universal proof certificate.",
"Exploit-path results are limited to the admitted snapshot, normalized graph, query, transition semantics, and bounded search profile.",
"A valid path is not backend execution and an invalid path is not real-world non-exploitability.",
"The production exploit-path JSON loader permits duplicate keys; the research loader rejects them without claiming stronger production behavior.",
"Participant replay inherits the host environment and is not described as hermetic.",
"Counterfactual necessity remains untested.",
"Scoped observation demand is not a claim class in this preregistration and is not promoted to demonstrated by this retest.",
"EXP-732 provenance joins are verified by their dedicated regression suite; this retained corpus makes no universal run, apparatus, source, or augmentation assurance claim.",
"This retained corpus does not establish native backend attestation fidelity; materialization contract checks remain separate operational provenance, not experimental observations.",
"Capture admission and evidence-proof authority are verified by issue-1237 regression tests, not promoted to a new claim class by this retained corpus.",
"Evidence-requirement refinement lineage is outside this retained formal claim set; this retest refreshes integrated source provenance without promoting that feature to a formal claim.",
"Authoring-adapter transport behavior is outside this retained formal claim set.",
"Operational recovery observation and startup reconciliation are verified by their API-404 regression suite, not promoted to a new formal claim class by this retained corpus.",
"Single-owner store admission, immutable target/run scope, and provider shutdown ordering are verified by their API-404 CP-5 regression suite, not promoted to a formal claim by this retained corpus.",
"Mixed and staged trial admission is verified by its SEM-234/SCE-002/API-407 regression suite, not promoted to a new formal claim class by this retained corpus.",
"Offline control-plane maintenance, readiness, and bounded audit behavior are verified by issue #1186 runtime tests, not promoted to a formal claim by this retained corpus.",
"Issue #1187 control-plane crash/profile conformance and HTTP security changes are covered by their dedicated regression suite, not promoted to new claims by this retained corpus.",
"Issue #1189 profile declarations and capability admission are covered by dedicated runtime tests; the retained formal corpus does not execute control-plane profile composition.",
"Issue #1016 mixed-runtime coordination is covered by dedicated runtime tests; the retained formal corpus does not establish backend-native mixed realization, multi-controller coordination, IFC, or equivalence.",
"Issue #610's reconciliation demonstration harness is covered by its dedicated processor and CLI suite, not promoted to new claims by the retained language corpus.",
"Participant identity, organization ownership, and participant assignment are separated by issue #1338. This retained offline corpus does not establish participant autonomy, execution authority, live backend fidelity, or causal attribution.",
"Issue #1389 temporal-subject admission is verified by dedicated compiler tests and adds no new formal-semantic claim to this retained corpus.",
"Issue #971 model construction is verified by its own tests; this retained corpus establishes no participant-crossing equivalence or runtime-realization claim.",
"Issue #1359 control-plane route authority, participant-view scoping, and no-store HTTP boundary are verified by their dedicated HTTP-boundary suite and add no new formal-semantic claim to this retained corpus.",
"Issue #1401 required-evidence media-type coherence is verified by its dedicated suite and adds no new formal-semantic claim to this retained corpus."
],
"plain_language_outcome": "The retained formal cases reproduce their prior outcomes against source that rejects required evidence whose declared media type the output registry cannot prove; outcomes and bounded claim limits are unchanged.",
"protocol_revision": "2.0.0"
}
Loading
Loading