diff --git a/docs/mncs-reconstruction/evidence/mnel-core-differential-study.json b/docs/mncs-reconstruction/evidence/mnel-core-differential-study.json index dfb8ea1..4dff03b 100644 --- a/docs/mncs-reconstruction/evidence/mnel-core-differential-study.json +++ b/docs/mncs-reconstruction/evidence/mnel-core-differential-study.json @@ -7,8 +7,8 @@ "reference_side": { "implementation": "Machine-Native-Experimental-Learning src/mnel (Python control plane)", "corpus": "mncs/corpora/mnel-core-reference.json", - "corpus_sha256": "0f0510e8eb5e8522ba935ba7c22d67f9209e0c462a9c5866fba3c2e60d444541", - "cases": 160, + "corpus_sha256": "a818605acab5768b5fb67078bb5c54c3983d043648c5316b6a5267a5fff7c2e4", + "cases": 172, "oracle_kinds": [ "derived-table", "reference-code" @@ -16,9 +16,16 @@ }, "mncs_side": { "source": "mncs/source/mnel/all.mncs", - "source_sha256": "93edf3cb10c7098ff255e8a4067356a394c75a88389e61047d043ddd8fdf2a7d", - "module": "mnel.core", - "language_profile": "0.5" + "source_sha256": "0e5b61440462ad287a0821ef14adf40b74ee519d9eede37fd4a0c905c328f2e0", + "module": "mnel.all", + "language_profile": "0.8", + "standard_library_bindings": [ + "mncs.core.status.v1", + "mncs.core.logic.v1", + "mncs.core.random.v1", + "mncs.core.numeric.v1" + ], + "library_path": "/home/epi13/Documents/Projects/mncs-language/library" }, "backends": [ { @@ -26,8 +33,21 @@ "outcome": "corpus-executed", "summary": { "exit_code": 0, - "cases_total": 160, - "cases_met": 160, + "cases_total": 172, + "cases_met": 172, + "experiment_status": "UNKNOWN", + "unresolved_reasons": [ + "compilation retained required unresolved obligations" + ] + } + }, + { + "backend": "mncs-portable-wasm-mvp", + "outcome": "corpus-executed", + "summary": { + "exit_code": 0, + "cases_total": 172, + "cases_met": 172, "experiment_status": "UNKNOWN", "unresolved_reasons": [ "compilation retained required unresolved obligations" diff --git a/docs/mncs-reconstruction/evidence/mnel-training-differential-study.json b/docs/mncs-reconstruction/evidence/mnel-training-differential-study.json new file mode 100644 index 0000000..a9583bd --- /dev/null +++ b/docs/mncs-reconstruction/evidence/mnel-training-differential-study.json @@ -0,0 +1,64 @@ +{ + "schema_version": "0.1", + "identity_kind": "bounded-differential-study-record", + "study": "mnel-training-slice", + "runner_identity": "mnel-mncs-differential-runner/0.1", + "interpretation": "bounded_observational_agreement_over_declared_corpus; not_universal_equivalence_not_conformance_not_assurance", + "reference_side": { + "implementation": "Machine-Native-Experimental-Learning src/mnel (Python control plane)", + "corpus": "mncs/corpora/mnel-training-reference.json", + "corpus_sha256": "848164449fc6e737d05ae9186e55581d3e95c8cc135fd8d048b431699511e141", + "cases": 15, + "oracle_kinds": [ + "reference-code" + ] + }, + "mncs_side": { + "source": "mncs/source/mnel/training.mncs", + "source_sha256": "b677125735e88cf3e64813214a74a9d40fb5cf2853308917943b2af535f0a5e8", + "module": "mnel.training", + "language_profile": "0.8", + "standard_library_bindings": [ + "mncs.core.status.v1", + "mncs.core.random.v1", + "mncs.core.numeric.v1" + ], + "library_path": "/home/epi13/Documents/Projects/mncs-language/library" + }, + "backends": [ + { + "backend": "mncs-research-bytecode", + "outcome": "corpus-executed", + "summary": { + "exit_code": 0, + "cases_total": 15, + "cases_met": 15, + "experiment_status": "UNKNOWN", + "unresolved_reasons": [ + "compilation retained required unresolved obligations" + ] + } + }, + { + "backend": "mncs-portable-wasm-mvp", + "outcome": "corpus-executed", + "summary": { + "exit_code": 0, + "cases_total": 15, + "cases_met": 15, + "experiment_status": "UNKNOWN", + "unresolved_reasons": [ + "compilation retained required unresolved obligations" + ] + } + } + ], + "comparison_status": "AGREEMENT_OVER_CORPUS", + "disagreements": [], + "non_claims": [ + "observed agreement is not proof of semantic equivalence", + "the corpus covers a bounded slice of MNEL training concepts only", + "backend envelope refusals are recorded, not resolved", + "unresolved obligations remain UNKNOWN; nothing here certifies the MNCS implementation against the reference beyond the corpus" + ] +} diff --git a/mncs/corpora/mnel-core-reference.json b/mncs/corpora/mnel-core-reference.json index 1a6b362..48f0263 100644 --- a/mncs/corpora/mnel-core-reference.json +++ b/mncs/corpora/mnel-core-reference.json @@ -7,21 +7,21 @@ "request": { "schema_version": "0.1", "target": { - "module": "mnel.verdict", - "function": "combine_verdict" + "module": "mncs.core.status.v1", + "function": "dominate" }, "arguments": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } }, { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -31,8 +31,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -47,21 +47,21 @@ "request": { "schema_version": "0.1", "target": { - "module": "mnel.verdict", - "function": "combine_verdict" + "module": "mncs.core.status.v1", + "function": "dominate" }, "arguments": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } }, { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -71,8 +71,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -87,21 +87,21 @@ "request": { "schema_version": "0.1", "target": { - "module": "mnel.verdict", - "function": "combine_verdict" + "module": "mncs.core.status.v1", + "function": "dominate" }, "arguments": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } }, { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -111,8 +111,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -127,21 +127,21 @@ "request": { "schema_version": "0.1", "target": { - "module": "mnel.verdict", - "function": "combine_verdict" + "module": "mncs.core.status.v1", + "function": "dominate" }, "arguments": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } }, { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -151,8 +151,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -167,21 +167,21 @@ "request": { "schema_version": "0.1", "target": { - "module": "mnel.verdict", - "function": "combine_verdict" + "module": "mncs.core.status.v1", + "function": "dominate" }, "arguments": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } }, { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -191,8 +191,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -207,21 +207,21 @@ "request": { "schema_version": "0.1", "target": { - "module": "mnel.verdict", - "function": "combine_verdict" + "module": "mncs.core.status.v1", + "function": "dominate" }, "arguments": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } }, { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -231,8 +231,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -247,21 +247,21 @@ "request": { "schema_version": "0.1", "target": { - "module": "mnel.verdict", - "function": "combine_verdict" + "module": "mncs.core.status.v1", + "function": "dominate" }, "arguments": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } }, { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -271,8 +271,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -287,21 +287,21 @@ "request": { "schema_version": "0.1", "target": { - "module": "mnel.verdict", - "function": "combine_verdict" + "module": "mncs.core.status.v1", + "function": "dominate" }, "arguments": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } }, { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -311,8 +311,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -327,21 +327,21 @@ "request": { "schema_version": "0.1", "target": { - "module": "mnel.verdict", - "function": "combine_verdict" + "module": "mncs.core.status.v1", + "function": "dominate" }, "arguments": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } }, { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -351,8 +351,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -362,6 +362,394 @@ "citation": "HardGateEvaluator aggregation rule (src/mnel/core.py evaluate): any FAIL => FAIL; else any UNKNOWN => UNKNOWN; else PASS." } }, + { + "id": "bool-and-0-0", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_and" + }, + "arguments": [ + { + "boolean": { + "value": false + } + }, + { + "boolean": { + "value": false + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": false + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.both (mncs/source/mnel/logic.mncs before stdlib binding): if left { right } else false." + } + }, + { + "id": "bool-or-0-0", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_or" + }, + "arguments": [ + { + "boolean": { + "value": false + } + }, + { + "boolean": { + "value": false + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": false + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.either (mncs/source/mnel/logic.mncs before stdlib binding): if left { true } else right." + } + }, + { + "id": "bool-not-0-0", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_not" + }, + "arguments": [ + { + "boolean": { + "value": false + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": true + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.not (mncs/source/mnel/logic.mncs before stdlib binding)." + } + }, + { + "id": "bool-and-0-1", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_and" + }, + "arguments": [ + { + "boolean": { + "value": false + } + }, + { + "boolean": { + "value": true + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": false + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.both (mncs/source/mnel/logic.mncs before stdlib binding): if left { right } else false." + } + }, + { + "id": "bool-or-0-1", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_or" + }, + "arguments": [ + { + "boolean": { + "value": false + } + }, + { + "boolean": { + "value": true + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": true + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.either (mncs/source/mnel/logic.mncs before stdlib binding): if left { true } else right." + } + }, + { + "id": "bool-not-0-1", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_not" + }, + "arguments": [ + { + "boolean": { + "value": false + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": true + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.not (mncs/source/mnel/logic.mncs before stdlib binding)." + } + }, + { + "id": "bool-and-1-0", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_and" + }, + "arguments": [ + { + "boolean": { + "value": true + } + }, + { + "boolean": { + "value": false + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": false + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.both (mncs/source/mnel/logic.mncs before stdlib binding): if left { right } else false." + } + }, + { + "id": "bool-or-1-0", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_or" + }, + "arguments": [ + { + "boolean": { + "value": true + } + }, + { + "boolean": { + "value": false + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": true + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.either (mncs/source/mnel/logic.mncs before stdlib binding): if left { true } else right." + } + }, + { + "id": "bool-not-1-0", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_not" + }, + "arguments": [ + { + "boolean": { + "value": true + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": false + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.not (mncs/source/mnel/logic.mncs before stdlib binding)." + } + }, + { + "id": "bool-and-1-1", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_and" + }, + "arguments": [ + { + "boolean": { + "value": true + } + }, + { + "boolean": { + "value": true + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": true + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.both (mncs/source/mnel/logic.mncs before stdlib binding): if left { right } else false." + } + }, + { + "id": "bool-or-1-1", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_or" + }, + "arguments": [ + { + "boolean": { + "value": true + } + }, + { + "boolean": { + "value": true + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": true + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.either (mncs/source/mnel/logic.mncs before stdlib binding): if left { true } else right." + } + }, + { + "id": "bool-not-1-1", + "request": { + "schema_version": "0.1", + "target": { + "module": "mncs.core.logic.v1", + "function": "bool_not" + }, + "arguments": [ + { + "boolean": { + "value": true + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": false + } + } + ], + "oracle": { + "kind": "derived-table", + "citation": "former mnel.logic.not (mncs/source/mnel/logic.mncs before stdlib binding)." + } + }, { "id": "gates-panel-all-pass", "request": { @@ -585,8 +973,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -663,8 +1051,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -741,8 +1129,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -819,8 +1207,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -897,8 +1285,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -1131,8 +1519,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -1209,8 +1597,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -1287,8 +1675,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -1365,8 +1753,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -1443,8 +1831,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -1677,8 +2065,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -1755,8 +2143,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -1833,8 +2221,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -1911,8 +2299,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -1989,8 +2377,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -2223,8 +2611,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -2301,8 +2689,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -2379,8 +2767,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -2457,8 +2845,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -2535,8 +2923,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -2769,8 +3157,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -2847,8 +3235,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -2925,8 +3313,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -3003,8 +3391,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -3081,8 +3469,8 @@ "expected": [ { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -11854,7 +12242,7 @@ "expected": [ { "record": { - "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AVerdict%3B", + "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AStatus%3B", "name": "ExperimentOutcome", "fields": [ [ @@ -11881,8 +12269,8 @@ "verdict", { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -12189,7 +12577,7 @@ "expected": [ { "record": { - "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AVerdict%3B", + "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AStatus%3B", "name": "ExperimentOutcome", "fields": [ [ @@ -12216,8 +12604,8 @@ "verdict", { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::PASS", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", "discriminant": 0 } } @@ -12524,7 +12912,7 @@ "expected": [ { "record": { - "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AVerdict%3B", + "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AStatus%3B", "name": "ExperimentOutcome", "fields": [ [ @@ -12551,8 +12939,8 @@ "verdict", { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::FAIL", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", "discriminant": 1 } } @@ -12859,7 +13247,7 @@ "expected": [ { "record": { - "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AVerdict%3B", + "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AStatus%3B", "name": "ExperimentOutcome", "fields": [ [ @@ -12886,8 +13274,8 @@ "verdict", { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -13194,7 +13582,7 @@ "expected": [ { "record": { - "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AVerdict%3B", + "type_identity": "mncs:0.2:record-type:mnel.core::ExperimentOutcome::final_state%3AExperimentState%3Bprinciple_maturity%3AMaturity%3Bverdict%3AStatus%3B", "name": "ExperimentOutcome", "fields": [ [ @@ -13221,8 +13609,8 @@ "verdict", { "finite": { - "type_identity": "mncs:0.2:finite-type:mnel.verdict::Verdict", - "variant_identity": "mncs:0.2:finite-variant:mnel.verdict::Verdict::UNKNOWN", + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::UNKNOWN", "discriminant": 2 } } @@ -13244,17 +13632,18 @@ "mncs/source/mnel/all.mncs", "mncs/source/mnel/authority.mncs", "mncs/source/mnel/core.mncs", + "mncs/source/mnel/dataset.mncs", "mncs/source/mnel/gates.mncs", "mncs/source/mnel/lifecycle.mncs", - "mncs/source/mnel/logic.mncs", "mncs/source/mnel/negative_memory.mncs", + "mncs/source/mnel/observation.mncs", "mncs/source/mnel/probe.mncs", "mncs/source/mnel/rejection.mncs", + "mncs/source/mnel/training.mncs", "mncs/source/mnel/transfer.mncs", - "mncs/source/mnel/verdict.mncs", "mncs/source/mnel/visibility.mncs" ], - "mncs_sources_sha256": "0e03b72be26a195415d66a9e7fccd6aae4ef651798af5726225afa122aa83240", + "mncs_sources_sha256": "0e5b61440462ad287a0821ef14adf40b74ee519d9eede37fd4a0c905c328f2e0", "oracle_kinds": { "reference-code": "expected values produced by executing MNEL classes", "derived-table": "expected values encode documented MNEL behavior with citations; MNEL enforces these structurally" diff --git a/mncs/corpora/mnel-training-reference.json b/mncs/corpora/mnel-training-reference.json new file mode 100644 index 0000000..03c3163 --- /dev/null +++ b/mncs/corpora/mnel-training-reference.json @@ -0,0 +1,1259 @@ +{ + "schema_version": "0.1", + "name": "mnel-training-reference-v1", + "cases": [ + { + "id": "clamp-one-5-10", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.dataset", + "function": "clamp_one" + }, + "arguments": [ + { + "integer": { + "value": 5, + "type": { + "bits": 64, + "signed": true + } + } + }, + { + "integer": { + "value": 10, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "integer": { + "value": 5, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.dataset.clamp_one: clamp to [-bound, bound] via comparisons" + } + }, + { + "id": "apply-transform-quad-identity-1-10", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.dataset", + "function": "apply_transform_quad" + }, + "arguments": [ + { + "record": { + "type_identity": "mncs:0.2:record-type:mnel.dataset::QuadI64::a%3Ai64%3Bb%3Ai64%3Bc%3Ai64%3Bd%3Ai64%3B", + "name": "QuadI64", + "fields": [ + [ + "a", + { + "integer": { + "value": 1, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "b", + { + "integer": { + "value": 2, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "c", + { + "integer": { + "value": 3, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "d", + { + "integer": { + "value": 4, + "type": { + "bits": 64, + "signed": true + } + } + } + ] + ] + } + }, + { + "finite": { + "type_identity": "mncs:0.2:finite-type:mnel.dataset::TransformKind", + "variant_identity": "mncs:0.2:finite-variant:mnel.dataset::TransformKind::IDENTITY", + "discriminant": 0 + } + }, + { + "integer": { + "value": 10, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "record": { + "type_identity": "mncs:0.2:record-type:mnel.dataset::QuadI64::a%3Ai64%3Bb%3Ai64%3Bc%3Ai64%3Bd%3Ai64%3B", + "name": "QuadI64", + "fields": [ + [ + "a", + { + "integer": { + "value": 1, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "b", + { + "integer": { + "value": 2, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "c", + { + "integer": { + "value": 3, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "d", + { + "integer": { + "value": 4, + "type": { + "bits": 64, + "signed": true + } + } + } + ] + ] + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.dataset.apply_transform_quad: per-lane IDENTITY vs CLIP" + } + }, + { + "id": "apply-transform-quad-clip-15-10", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.dataset", + "function": "apply_transform_quad" + }, + "arguments": [ + { + "record": { + "type_identity": "mncs:0.2:record-type:mnel.dataset::QuadI64::a%3Ai64%3Bb%3Ai64%3Bc%3Ai64%3Bd%3Ai64%3B", + "name": "QuadI64", + "fields": [ + [ + "a", + { + "integer": { + "value": 15, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "b", + { + "integer": { + "value": 20, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "c", + { + "integer": { + "value": 5, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "d", + { + "integer": { + "value": 0, + "type": { + "bits": 64, + "signed": true + } + } + } + ] + ] + } + }, + { + "finite": { + "type_identity": "mncs:0.2:finite-type:mnel.dataset::TransformKind", + "variant_identity": "mncs:0.2:finite-variant:mnel.dataset::TransformKind::CLIP", + "discriminant": 1 + } + }, + { + "integer": { + "value": 10, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "record": { + "type_identity": "mncs:0.2:record-type:mnel.dataset::QuadI64::a%3Ai64%3Bb%3Ai64%3Bc%3Ai64%3Bd%3Ai64%3B", + "name": "QuadI64", + "fields": [ + [ + "a", + { + "integer": { + "value": 10, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "b", + { + "integer": { + "value": 10, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "c", + { + "integer": { + "value": 5, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "d", + { + "integer": { + "value": 0, + "type": { + "bits": 64, + "signed": true + } + } + } + ] + ] + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.dataset.apply_transform_quad: per-lane IDENTITY vs CLIP" + } + }, + { + "id": "shuffle-quad-0-1", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.dataset", + "function": "shuffle_quad" + }, + "arguments": [ + { + "record": { + "type_identity": "mncs:0.2:record-type:mnel.dataset::QuadI64::a%3Ai64%3Bb%3Ai64%3Bc%3Ai64%3Bd%3Ai64%3B", + "name": "QuadI64", + "fields": [ + [ + "a", + { + "integer": { + "value": 1, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "b", + { + "integer": { + "value": 2, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "c", + { + "integer": { + "value": 3, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "d", + { + "integer": { + "value": 4, + "type": { + "bits": 64, + "signed": true + } + } + } + ] + ] + } + }, + { + "integer": { + "value": 0, + "type": { + "bits": 64, + "signed": false + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "record": { + "type_identity": "mncs:0.2:record-type:mnel.dataset::ShuffledQuad::data%3AQuadI64%3Bnext_seed%3Au64%3B", + "name": "ShuffledQuad", + "fields": [ + [ + "data", + { + "record": { + "type_identity": "mncs:0.2:record-type:mnel.dataset::QuadI64::a%3Ai64%3Bb%3Ai64%3Bc%3Ai64%3Bd%3Ai64%3B", + "name": "QuadI64", + "fields": [ + [ + "a", + { + "integer": { + "value": 4, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "b", + { + "integer": { + "value": 2, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "c", + { + "integer": { + "value": 3, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "d", + { + "integer": { + "value": 1, + "type": { + "bits": 64, + "signed": true + } + } + } + ] + ] + } + } + ], + [ + "next_seed", + { + "integer": { + "value": 11166244414315200793, + "type": { + "bits": 64, + "signed": false + } + } + } + ] + ] + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.dataset.shuffle_quad: deterministic LCG permutation over 4 lanes" + } + }, + { + "id": "split-counts-2-4", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.dataset", + "function": "split_counts" + }, + "arguments": [ + { + "integer": { + "value": 2, + "type": { + "bits": 64, + "signed": true + } + } + }, + { + "integer": { + "value": 4, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "record": { + "type_identity": "mncs:0.2:record-type:mnel.dataset::SplitCounts::test_count%3Ai64%3Btrain_count%3Ai64%3B", + "name": "SplitCounts", + "fields": [ + [ + "test_count", + { + "integer": { + "value": 2, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "train_count", + { + "integer": { + "value": 2, + "type": { + "bits": 64, + "signed": true + } + } + } + ] + ] + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.dataset.split_counts: train = floor(4*numer/denom) clamp [0,4]" + } + }, + { + "id": "validate-dataset-123-4", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.dataset", + "function": "validate_dataset_spec" + }, + "arguments": [ + { + "record": { + "type_identity": "mncs:0.2:record-type:mnel.dataset::DatasetSpec::clip_threshold%3Ai64%3Bpartition_seed%3Au64%3Bsource_identity%3Au64%3Btrain_denom%3Ai64%3Btrain_numer%3Ai64%3Btransform%3ATransformKind%3B", + "name": "DatasetSpec", + "fields": [ + [ + "clip_threshold", + { + "integer": { + "value": 10, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "partition_seed", + { + "integer": { + "value": 0, + "type": { + "bits": 64, + "signed": false + } + } + } + ], + [ + "source_identity", + { + "integer": { + "value": 123, + "type": { + "bits": 64, + "signed": false + } + } + } + ], + [ + "train_denom", + { + "integer": { + "value": 4, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "train_numer", + { + "integer": { + "value": 2, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + [ + "transform", + { + "finite": { + "type_identity": "mncs:0.2:finite-type:mnel.dataset::TransformKind", + "variant_identity": "mncs:0.2:finite-variant:mnel.dataset::TransformKind::IDENTITY", + "discriminant": 0 + } + } + ] + ] + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "boolean": { + "value": true + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.dataset.validate_dataset_spec: source !=0 and denom !=0" + } + }, + { + "id": "train-centroid-0-0-0-0", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.training", + "function": "train_centroid" + }, + "arguments": [ + { + "integer": { + "value": 0, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 0, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 0, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 0, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "integer": { + "value": 0, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.training.train_centroid via mncs.core.numeric.centroid4 wrapping reduce" + } + }, + { + "id": "train-centroid-4-8-12-16", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.training", + "function": "train_centroid" + }, + "arguments": [ + { + "integer": { + "value": 4, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 8, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 12, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 16, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.training.train_centroid via mncs.core.numeric.centroid4 wrapping reduce" + } + }, + { + "id": "sgd-step-10-20-1-2", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.training", + "function": "sgd_step" + }, + "arguments": [ + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 20, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 1, + "type": { + "bits": 64, + "signed": true + } + } + }, + { + "integer": { + "value": 2, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "integer": { + "value": 15, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.training.sgd_step: current +% ((sample-current)*numer/denom)" + } + }, + { + "id": "sgd-step-10-20-1-0", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.training", + "function": "sgd_step" + }, + "arguments": [ + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 20, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 1, + "type": { + "bits": 64, + "signed": true + } + } + }, + { + "integer": { + "value": 0, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.training.sgd_step: current +% ((sample-current)*numer/denom)" + } + }, + { + "id": "batch-centroid-1-42", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.training", + "function": "batch_centroid" + }, + "arguments": [ + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 20, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 30, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 40, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 42, + "type": { + "bits": 64, + "signed": false + } + } + }, + { + "integer": { + "value": 1, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.training.batch_centroid: shuffle then mean of first batch_size" + } + }, + { + "id": "l2-distance-10-3", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.training", + "function": "l2_distance_test" + }, + "arguments": [ + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 3, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "integer": { + "value": 7, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.training.l2_distance_test: abs(centroid-sample)" + } + }, + { + "id": "evaluate-centroid-10-10-10-0", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.training", + "function": "evaluate_centroid" + }, + "arguments": [ + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 0, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "finite": { + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::PASS", + "discriminant": 0 + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.training.evaluate_centroid: two LE gates joined by dominate" + } + }, + { + "id": "evaluate-centroid-10-20-10-5", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.training", + "function": "evaluate_centroid" + }, + "arguments": [ + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 20, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 10, + "type": { + "bits": 32, + "signed": true + } + } + }, + { + "integer": { + "value": 5, + "type": { + "bits": 32, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "finite": { + "type_identity": "mncs:0.2:finite-type:mncs.core.status.v1::Status", + "variant_identity": "mncs:0.2:finite-variant:mncs.core.status.v1::Status::FAIL", + "discriminant": 1 + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.training.evaluate_centroid: two LE gates joined by dominate" + } + }, + { + "id": "clamp-one-15-10", + "request": { + "schema_version": "0.1", + "target": { + "module": "mnel.dataset", + "function": "clamp_one" + }, + "arguments": [ + { + "integer": { + "value": 15, + "type": { + "bits": 64, + "signed": true + } + } + }, + { + "integer": { + "value": 10, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "step_budget": 512 + }, + "expected": [ + { + "integer": { + "value": 10, + "type": { + "bits": 64, + "signed": true + } + } + } + ], + "oracle": { + "kind": "reference-code", + "citation": "mnel.dataset.clamp_one: clamp to [-bound, bound] via comparisons" + } + } + ], + "provenance": { + "generator_identity": "mnel-training-corpus-generator/0.1", + "reference_package": "mnel (Machine-Native-Experimental-Learning)", + "mncs_sources": [ + "mncs/source/mnel/all.mncs", + "mncs/source/mnel/authority.mncs", + "mncs/source/mnel/core.mncs", + "mncs/source/mnel/dataset.mncs", + "mncs/source/mnel/gates.mncs", + "mncs/source/mnel/lifecycle.mncs", + "mncs/source/mnel/negative_memory.mncs", + "mncs/source/mnel/observation.mncs", + "mncs/source/mnel/probe.mncs", + "mncs/source/mnel/rejection.mncs", + "mncs/source/mnel/training.mncs", + "mncs/source/mnel/transfer.mncs", + "mncs/source/mnel/visibility.mncs" + ], + "mncs_sources_sha256": "0e5b61440462ad287a0821ef14adf40b74ee519d9eede37fd4a0c905c328f2e0", + "oracle_kinds": { + "reference-code": "expected values produced by Python oracle", + "derived-table": "expected values encode documented MNCS behavior" + }, + "determinism": "frozen inputs; no clock or randomness; sorted iteration" + } +} diff --git a/mncs/source/mnel/all.mncs b/mncs/source/mnel/all.mncs index 186ea9b..c43b683 100644 --- a/mncs/source/mnel/all.mncs +++ b/mncs/source/mnel/all.mncs @@ -1,4 +1,4 @@ -mncs 0.6; +mncs 0.8; // Aggregate root used by differential corpora: binds every mnel.* module so // one MNCS program carries the full slice. Declares nothing itself. @@ -6,12 +6,13 @@ module mnel.all; use mnel.authority; use mnel.core; +use mnel.dataset; use mnel.gates; use mnel.lifecycle; -use mnel.logic; use mnel.negative_memory; +use mnel.observation; use mnel.probe; use mnel.rejection; +use mnel.training; use mnel.transfer; -use mnel.verdict; use mnel.visibility; diff --git a/mncs/source/mnel/authority.mncs b/mncs/source/mnel/authority.mncs index 1e2251e..b090f50 100644 --- a/mncs/source/mnel/authority.mncs +++ b/mncs/source/mnel/authority.mncs @@ -7,7 +7,7 @@ mncs 0.6; module mnel.authority; use mnel.rejection; -use mnel.logic; +use mncs.core.logic.v1; record PlanFacts { governor_known: bool, @@ -39,14 +39,14 @@ fn validate_plan(facts: PlanFacts) -> (decision: PlanDecision) { if visibility_open_enough { let governor_ok: bool = facts.governor_known; let budget_ok: bool = facts.operations_budget > 0; - let admissible: bool = both(governor_ok, budget_ok); + let admissible: bool = bool_and(governor_ok, budget_ok); if admissible { return PlanDecision { accepted: true, reason: RejectionReason.NONE, }; } - let missing_budget: bool = not(budget_ok); + let missing_budget: bool = bool_not(budget_ok); if missing_budget { return PlanDecision { accepted: false, diff --git a/mncs/source/mnel/core.mncs b/mncs/source/mnel/core.mncs index aedea06..ed3a93c 100644 --- a/mncs/source/mnel/core.mncs +++ b/mncs/source/mnel/core.mncs @@ -1,9 +1,11 @@ mncs 0.6; // The reference experiment spine, mirroring MNEL's deterministic demo run: -// a validated plan advances through the lifecycle, the authorized evaluator +// a validated plan advances through the lifecycle, the observation is +// admitted against the preregistered budget, the authorized evaluator // derives the overall verdict from four preregistered gates, attribution is -// recorded, and a distillation proposal carries transfer-gated maturity. +// recorded from the verdict alone, and a distillation proposal carries +// transfer-gated maturity. // // Authority note: investigators and learned providers may propose knowledge. // They may not declare it true. An UNKNOWN verdict can reach DISTILLED_ @@ -14,19 +16,22 @@ module mnel.core; use mnel.authority; use mnel.gates; use mnel.lifecycle; -use mnel.logic; +use mnel.observation; +use mncs.core.status.v1; use mnel.rejection; use mnel.transfer; -use mnel.verdict; record ExperimentOutcome { final_state: ExperimentState, - verdict: Verdict, + verdict: Status, + disposition: Disposition, principle_maturity: Maturity, } fn run_reference_experiment( plan: PlanFacts, + observation: ObservationFacts, + limits: BudgetLimits, first: GateInput, second: GateInput, third: GateInput, @@ -46,35 +51,62 @@ fn run_reference_experiment( preregistration.next_state, LifecycleEvent.BEGIN_EXECUTION, ); - let observation: TransitionOutcome = transition( - execution_start.next_state, - LifecycleEvent.BUDGET_WITHIN_LIMITS, - ); - let overall: Verdict = evaluate_gates(first, second, third, fourth); - let evaluated: TransitionOutcome = transition( - observation.next_state, - LifecycleEvent.EVALUATOR_VERDICT, - ); - let attributed: TransitionOutcome = transition( - evaluated.next_state, - LifecycleEvent.RECORD_ATTRIBUTION, - ); - let distilled: TransitionOutcome = transition( - attributed.next_state, - LifecycleEvent.PROPOSE_DISTILLATION, - ); - let known_verdict: bool = verdict_is_known(overall); - let gated_request: Maturity = request_when_known(known_verdict, requested_maturity); - let maturity: Maturity = effective_maturity(gated_request, transfer); - return ExperimentOutcome { - final_state: distilled.next_state, - verdict: overall, - principle_maturity: maturity, - }; + let budget_decision: AdmissionDecision = + check_observation_budget(observation, limits); + if budget_decision.admitted { + let observation_step: TransitionOutcome = transition( + execution_start.next_state, + LifecycleEvent.BUDGET_WITHIN_LIMITS, + ); + let overall: Status = evaluate_gates(first, second, third, fourth); + let evaluated: TransitionOutcome = transition( + observation_step.next_state, + LifecycleEvent.EVALUATOR_VERDICT, + ); + let attribution: AttributionRecord = attribute(overall); + let attributed: TransitionOutcome = transition( + evaluated.next_state, + LifecycleEvent.RECORD_ATTRIBUTION, + ); + let distilled: TransitionOutcome = transition( + attributed.next_state, + LifecycleEvent.PROPOSE_DISTILLATION, + ); + let known_verdict: bool = is_decided(overall); + let gated_request: Maturity = + request_when_known(known_verdict, requested_maturity); + let maturity: Maturity = effective_maturity(gated_request, transfer); + return ExperimentOutcome { + final_state: distilled.next_state, + verdict: overall, + disposition: attribution.disposition, + principle_maturity: maturity, + }; + } + return budget_rejected(execution_start.next_state); } + return rejected_outcome(); +} + +// Over-budget observations never reach evaluation. The state machine walks +// the explicit BUDGET_EXCEEDED path to REJECTED; the verdict stays UNKNOWN +// because no gate ever ran, and nothing can be attributed. +fn budget_rejected(current: ExperimentState) -> (outcome: ExperimentOutcome) { + let exceeded: TransitionOutcome = + transition(current, LifecycleEvent.BUDGET_EXCEEDED); + return ExperimentOutcome { + final_state: exceeded.next_state, + verdict: Status.UNKNOWN, + disposition: Disposition.INCONCLUSIVE, + principle_maturity: Maturity.PROVISIONAL, + }; +} + +fn rejected_outcome() -> (outcome: ExperimentOutcome) { return ExperimentOutcome { final_state: ExperimentState.REJECTED, - verdict: Verdict.UNKNOWN, + verdict: Status.UNKNOWN, + disposition: Disposition.INCONCLUSIVE, principle_maturity: Maturity.PROVISIONAL, }; } diff --git a/mncs/source/mnel/dataset.mncs b/mncs/source/mnel/dataset.mncs new file mode 100644 index 0000000..6990148 --- /dev/null +++ b/mncs/source/mnel/dataset.mncs @@ -0,0 +1,199 @@ +mncs 0.8; + +// MNEL dataset construction: MNCS-owned filtering, transforms, +// deterministic sampling, and partitioning. +// +// Every decision here leaves an identity: source fingerprint, transform +// kind and parameters, partition seed, and resulting split counts. +// External runtimes may execute the transform, but MNCS owns the +// specification. +module mnel.dataset; + +use mncs.core.random.v1; +use mncs.core.status.v1; +use mnel.rejection; + +enum TransformKind { IDENTITY, CLIP } + +enum PartitionKind { TRAIN_TEST } + +record DatasetSpec { + source_identity: u64, + transform: TransformKind, + clip_threshold: i64, + partition_seed: u64, + train_numer: i64, + train_denom: i64, +} + +record DatasetFingerprint { + source: u64, + transform: TransformKind, + seed: u64, + train_numer: i64, + train_denom: i64, + threshold: i64, +} + +record SplitCounts { + train_count: i64, + test_count: i64, +} + +record QuadI64 { + a: i64, + b: i64, + c: i64, + d: i64, +} + +record ShuffledQuad { + data: QuadI64, + next_seed: u64, +} + +// Apply the declared transform to each lane. CLIP clamps to +// [-threshold, threshold]; IDENTITY passes through. +fn apply_transform_quad(data: QuadI64, kind: TransformKind, threshold: i64) -> (result: QuadI64) { + let t: i64 = threshold; + let out0: i64 = match kind { + IDENTITY => data.a, + CLIP => clamp_one(data.a, t), + }; + let out1: i64 = match kind { + IDENTITY => data.b, + CLIP => clamp_one(data.b, t), + }; + let out2: i64 = match kind { + IDENTITY => data.c, + CLIP => clamp_one(data.c, t), + }; + let out3: i64 = match kind { + IDENTITY => data.d, + CLIP => clamp_one(data.d, t), + }; + return QuadI64 { a: out0, b: out1, c: out2, d: out3 }; +} + + + +fn clamp_one(value: i64, bound: i64) -> (result: i64) { + let neg: i64 = 0 - bound; + if value < neg { + return neg; + } + if value > bound { + return bound; + } + return value; +} + +// Quad-based shuffle is the portable envelope: it avoids the +// sequence-typed boundary that scalar backends refuse and is exercised +// by the differential corpus for cross-backend agreement. +fn shuffle_quad(data: QuadI64, seed: u64) -> (result: ShuffledQuad) { + let step0: BoundedDraw = lcg_next_bounded(seed, 4); + let idx0: u64 = step0.value; + let s1: u64 = step0.next_state; + let after0: QuadI64 = swap_quad(data, 0, idx0); + + let step1: BoundedDraw = lcg_next_bounded(s1, 4); + let idx1: u64 = step1.value; + let s2: u64 = step1.next_state; + let after1: QuadI64 = swap_quad(after0, 1, idx1); + + let step2: BoundedDraw = lcg_next_bounded(s2, 4); + let idx2: u64 = step2.value; + let s3: u64 = step2.next_state; + let after2: QuadI64 = swap_quad(after1, 2, idx2); + + return ShuffledQuad { data: after2, next_seed: s3 }; +} + +fn swap_quad(base: QuadI64, a: u64, b: u64) -> (result: QuadI64) { + if a == b { + return base; + } + if a == 0 { + if b == 1 { + return QuadI64 { a: base.b, b: base.a, c: base.c, d: base.d }; + } + if b == 2 { + return QuadI64 { a: base.c, b: base.b, c: base.a, d: base.d }; + } + return QuadI64 { a: base.d, b: base.b, c: base.c, d: base.a }; + } + if a == 1 { + if b == 0 { + return QuadI64 { a: base.b, b: base.a, c: base.c, d: base.d }; + } + if b == 2 { + return QuadI64 { a: base.a, b: base.c, c: base.b, d: base.d }; + } + return QuadI64 { a: base.a, b: base.d, c: base.c, d: base.b }; + } + if a == 2 { + if b == 0 { + return QuadI64 { a: base.c, b: base.b, c: base.a, d: base.d }; + } + if b == 1 { + return QuadI64 { a: base.a, b: base.c, c: base.b, d: base.d }; + } + return QuadI64 { a: base.a, b: base.b, c: base.d, d: base.c }; + } + // a == 3 + if b == 0 { + return QuadI64 { a: base.d, b: base.b, c: base.c, d: base.a }; + } + if b == 1 { + return QuadI64 { a: base.a, b: base.d, c: base.c, d: base.b }; + } + if b == 2 { + return QuadI64 { a: base.a, b: base.b, c: base.d, d: base.c }; + } + return base; +} + + + +// Deterministic train/test split. After shuffling, the first +// train_count elements are the train split. Counts are derived from +// the ratio train_numer/train_denom over the fixed length 4. +fn split_counts(train_numer: i64, train_denom: i64) -> (counts: SplitCounts) { + if train_denom == 0 { + return SplitCounts { train_count: 0, test_count: 4 }; + } + if train_numer < 0 { + return SplitCounts { train_count: 0, test_count: 4 }; + } + if train_numer > train_denom { + return SplitCounts { train_count: 4, test_count: 0 }; + } + let train: i64 = (4 *% train_numer) / train_denom; + let test: i64 = 4 -% train; + return SplitCounts { train_count: train, test_count: test }; +} + +fn dataset_fingerprint(spec: DatasetSpec) -> (print: DatasetFingerprint) { + return DatasetFingerprint { + source: spec.source_identity, + transform: spec.transform, + seed: spec.partition_seed, + train_numer: spec.train_numer, + train_denom: spec.train_denom, + threshold: spec.clip_threshold, + }; +} + +// Admission check for a dataset spec: source must be non-zero and +// denominator must be non-zero; transform threshold is allowed to be +// any i64. +fn validate_dataset_spec(spec: DatasetSpec) -> (decision: bool) { + if spec.source_identity == 0 { + return false; + } + if spec.train_denom == 0 { + return false; + } + return true; +} diff --git a/mncs/source/mnel/gates.mncs b/mncs/source/mnel/gates.mncs index 258ca21..67cc1a8 100644 --- a/mncs/source/mnel/gates.mncs +++ b/mncs/source/mnel/gates.mncs @@ -4,8 +4,7 @@ mncs 0.6; // derive_verdict effect carries that authority through every caller. module mnel.gates; -use mnel.verdict; -use mnel.logic; +use mncs.core.status.v1; enum GateOperator { GE, GT, LE, LT, EQ } @@ -18,7 +17,7 @@ record GateInput { threshold: i64, } -fn evaluate_gate(input: GateInput) -> (verdict: Verdict) +fn evaluate_gate(input: GateInput) -> (verdict: Status) capability hard_gate_authority effect derive_verdict authorized_by hard_gate_authority { @@ -35,22 +34,22 @@ fn evaluate_gate(input: GateInput) -> (verdict: Verdict) EQ => input.observed == input.threshold, }; if holds { - return Verdict.PASS; + return Status.PASS; } - return Verdict.FAIL; + return Status.FAIL; } - return Verdict.UNKNOWN; + return Status.UNKNOWN; } fn aggregate_four( - first: Verdict, - second: Verdict, - third: Verdict, - fourth: Verdict, -) -> (overall: Verdict) { - let left_combined: Verdict = combine_verdict(first, second); - let right_combined: Verdict = combine_verdict(third, fourth); - return combine_verdict(left_combined, right_combined); + first: Status, + second: Status, + third: Status, + fourth: Status, +) -> (overall: Status) { + let left_combined: Status = dominate(first, second); + let right_combined: Status = dominate(third, fourth); + return dominate(left_combined, right_combined); } fn evaluate_gates( @@ -58,13 +57,13 @@ fn evaluate_gates( second: GateInput, third: GateInput, fourth: GateInput, -) -> (overall: Verdict) +) -> (overall: Status) capability hard_gate_authority effect derive_verdict authorized_by hard_gate_authority { - let first_verdict: Verdict = evaluate_gate(first); - let second_verdict: Verdict = evaluate_gate(second); - let third_verdict: Verdict = evaluate_gate(third); - let fourth_verdict: Verdict = evaluate_gate(fourth); + let first_verdict: Status = evaluate_gate(first); + let second_verdict: Status = evaluate_gate(second); + let third_verdict: Status = evaluate_gate(third); + let fourth_verdict: Status = evaluate_gate(fourth); return aggregate_four(first_verdict, second_verdict, third_verdict, fourth_verdict); } diff --git a/mncs/source/mnel/logic.mncs b/mncs/source/mnel/logic.mncs deleted file mode 100644 index 8e0598c..0000000 --- a/mncs/source/mnel/logic.mncs +++ /dev/null @@ -1,26 +0,0 @@ -mncs 0.6; - -// Shared boolean algebra over exhaustive matches. The source profiles define -// no boolean operators beyond their use as conditions. -module mnel.logic; - -fn both(left: bool, right: bool) -> (result: bool) { - if left { - return right; - } - return false; -} - -fn either(left: bool, right: bool) -> (result: bool) { - if left { - return true; - } - return right; -} - -fn not(value: bool) -> (result: bool) { - if value { - return false; - } - return true; -} diff --git a/mncs/source/mnel/negative_memory.mncs b/mncs/source/mnel/negative_memory.mncs index fcef229..9acbc27 100644 --- a/mncs/source/mnel/negative_memory.mncs +++ b/mncs/source/mnel/negative_memory.mncs @@ -4,7 +4,7 @@ mncs 0.6; // demotes retrieval scoring; it never deletes positive lineage. module mnel.negative_memory; -use mnel.logic; +use mncs.core.logic.v1; record ContextMembership { retrieval: bool, @@ -14,13 +14,13 @@ record ContextMembership { } fn negative_memory_conflicts(rule: ContextMembership, context: ContextMembership) -> (hit: bool) { - let retrieval_hit: bool = both(rule.retrieval, context.retrieval); - let planning_hit: bool = both(rule.planning, context.planning); - let transfer_hit: bool = both(rule.transfer, context.transfer); - let monitoring_hit: bool = both(rule.monitoring, context.monitoring); - let first_pair: bool = either(retrieval_hit, planning_hit); - let second_pair: bool = either(transfer_hit, monitoring_hit); - return either(first_pair, second_pair); + let retrieval_hit: bool = bool_and(rule.retrieval, context.retrieval); + let planning_hit: bool = bool_and(rule.planning, context.planning); + let transfer_hit: bool = bool_and(rule.transfer, context.transfer); + let monitoring_hit: bool = bool_and(rule.monitoring, context.monitoring); + let first_pair: bool = bool_or(retrieval_hit, planning_hit); + let second_pair: bool = bool_or(transfer_hit, monitoring_hit); + return bool_or(first_pair, second_pair); } // A conflicting negative memory subtracts six points from the candidate diff --git a/mncs/source/mnel/observation.mncs b/mncs/source/mnel/observation.mncs new file mode 100644 index 0000000..0ab60e9 --- /dev/null +++ b/mncs/source/mnel/observation.mncs @@ -0,0 +1,95 @@ +mncs 0.6; + +// Observation admission and causal attribution. +// +// Mirrors RecursionGovernor.check_budget and the ExperimentCoordinator +// attribution step (src/mnel/core.py): an observation is admitted only when +// its measured resource consumption stays within the preregistered budget, +// and the recorded disposition follows the evaluated verdict — never the +// investigator's preference. +// +// Layer note: the reference governor rejects an over-budget observation by +// raising inside coordinator.run(); this slice reports the same boundary as +// an explicit admission decision the caller must handle, so the rejection is +// a value that corpora can differentiate against. +module mnel.observation; + +use mnel.rejection; +use mncs.core.status.v1; + +enum OutcomeClass { SUCCESS, ERROR, NEUTRAL, ABSTENTION } + +record ObservationFacts { + outcome_class: OutcomeClass, + operations_used: i64, + wall_milli_seconds: i64, +} + +record BudgetLimits { + max_operations: i64, + max_wall_milli_seconds: i64, +} + +record AdmissionDecision { + admitted: bool, + reason: RejectionReason, +} + +fn check_observation_budget( + observation: ObservationFacts, + limits: BudgetLimits, +) -> (decision: AdmissionDecision) { + if observation.operations_used > limits.max_operations { + return AdmissionDecision { + admitted: false, + reason: RejectionReason.BUDGET_EXHAUSTED, + }; + } + if observation.wall_milli_seconds > limits.max_wall_milli_seconds { + return AdmissionDecision { + admitted: false, + reason: RejectionReason.BUDGET_EXHAUSTED, + }; + } + return AdmissionDecision { + admitted: true, + reason: RejectionReason.NONE, + }; +} + +enum Disposition { SUPPORTED_WITH_ALTERNATIVES, INCONCLUSIVE } + +record AttributionRecord { + disposition: Disposition, + credit_immediate: bool, + credit_retention: bool, + verdict_known: bool, +} + +// Attribution mirrors the coordinator step: only a PASS evaluation supports +// the intervention, and even then alternatives stay listed. UNKNOWN and FAIL +// attribute nothing; they are recorded as inconclusive so downstream +// consumers can never read promotion out of missing evidence. +fn attribute(verdict: Status) -> (attribution: AttributionRecord) { + let known: bool = is_decided(verdict); + return match verdict { + Status.PASS => AttributionRecord { + disposition: Disposition.SUPPORTED_WITH_ALTERNATIVES, + credit_immediate: true, + credit_retention: true, + verdict_known: known, + }, + Status.FAIL => AttributionRecord { + disposition: Disposition.INCONCLUSIVE, + credit_immediate: false, + credit_retention: false, + verdict_known: known, + }, + Status.UNKNOWN => AttributionRecord { + disposition: Disposition.INCONCLUSIVE, + credit_immediate: false, + credit_retention: false, + verdict_known: known, + }, + }; +} diff --git a/mncs/source/mnel/training.mncs b/mncs/source/mnel/training.mncs new file mode 100644 index 0000000..204d53d --- /dev/null +++ b/mncs/source/mnel/training.mncs @@ -0,0 +1,234 @@ +mncs 0.8; + +// MNCS-owned training specification and execution. +// +// This module is the canonical MNCS representation of an MNEL training run: +// source dataset, transforms, model architecture, optimizer, resource policy, +// checkpoints, stopping criteria, evaluation suite, and resulting artifact. +// External numerical backends may execute the arithmetic, but MNCS owns +// the semantic graph and records the lineage identities. +// +// The micro-model chosen for the first executable slice is a bounded +// tabular centroid: four i32 feature values are reduced to a single +// centroid (mean) via wrapping vector reduction. The centroid is the +// entire model. Evaluation compares held-out samples to the centroid +// under an L2 threshold. The slice is tiny but exercises vectors, +// masks, deterministic sampling, and hard-gate admission. +module mnel.training; + +use mnel.dataset; +use mnel.gates; +use mnel.rejection; +use mncs.core.numeric.v1; +use mncs.core.random.v1; +use mncs.core.status.v1; + +enum ModelFamily { TABULAR_CENTROID, TRANSITION_FREQUENCY, TINY_LINEAR } + +enum OptimizerKind { COUNTING, SGD_WRAP } + +enum Precision { P32, P64 } + +enum DeviceKind { CPU, WASM, NATIVE } + +record ModelSpec { + family: ModelFamily, + capacity_target: i64, + precision: Precision, +} + +record OptimizerSpec { + kind: OptimizerKind, + batch_size: i64, + learning_rate_numer: i64, + learning_rate_denom: i64, + seed: u64, +} + +record ResourcePolicy { + max_operations: i64, + max_wall_ms: i64, + device: DeviceKind, +} + +record CheckpointPolicy { + interval_epochs: i64, + keep_last: i64, +} + +record StoppingRule { + max_epochs: i64, + patience: i64, +} + +record EvaluationSpec { + gate_one: GateInput, + gate_two: GateInput, + gate_three: GateInput, + gate_four: GateInput, +} + +record TrainingSpec { + dataset: DatasetSpec, + model: ModelSpec, + optimizer: OptimizerSpec, + resource: ResourcePolicy, + checkpoint: CheckpointPolicy, + stopping: StoppingRule, + evaluation: EvaluationSpec, + parent_model_identity: u64, + training_code_identity: u64, +} + +record Checkpoint { + epoch: i64, + centroid: i32, + seed_state: u64, +} + +record ModelArtifact { + spec: TrainingSpec, + centroid: i32, + dataset_fingerprint: DatasetFingerprint, + final_checkpoint: Checkpoint, + evaluation_verdict: Status, + artifact_digest: u64, + lineage_parent: u64, +} + +// Wrapping centroid of four i32 feature lanes. This is the entire +// tabular-centroid training step: sum via vector reduction, divide by 4. +fn train_centroid(a: i32, b: i32, c: i32, d: i32) -> (centroid: i32) { + return centroid4(a, b, c, d); +} + +// One SGD-style update for the tiny linear model: centroid is moved +// toward the sample mean by learning_rate = numer/denom using wrapping +// arithmetic. The update is total; division by zero is defined as no +// update (returns the current centroid) so the step never fails. +fn sgd_step(current: i32, sample: i32, numer: i64, denom: i64) -> (updated: i32) { + if denom == 0 { + return current; + } + let diff: i32 = sample - current; + let scaled: i32 = (((diff as i64) *% numer) / denom) as i32; + return current +% scaled; +} + +// Deterministic batch centroid: shuffle the four samples with the +// optimizer seed, then take the first batch_size lanes as the batch +// and compute its centroid. Batching is reproducible from the seed. +fn batch_centroid(a: i32, b: i32, c: i32, d: i32, seed: u64, batch_size: i64) -> (centroid: i32) { + let data_quad: QuadI64 = QuadI64 { a: a as i64, b: b as i64, c: c as i64, d: d as i64 }; + let shuffled: ShuffledQuad = shuffle_quad(data_quad, seed); + let s: QuadI64 = shuffled.data; + if batch_size <= 1 { + return (s.a as i32); + } + if batch_size == 2 { + let v: i32 = (((s.a +% s.b) / 2) as i32); + return v; + } + if batch_size == 3 { + let v: i32 = (((s.a +% s.b +% s.c) / 3) as i32); + return v; + } + return centroid4(s.a as i32, s.b as i32, s.c as i32, s.d as i32); +} + +// Evaluate a centroid against two held-out samples using L2 distance. +// Distance <= threshold => PASS, else FAIL; absent metric => UNKNOWN +// is not used here because distances are always present. The overall +// verdict is the lattice join of the two distances via dominate. +fn evaluate_centroid(centroid: i32, test0: i32, test1: i32, threshold: i32) -> (verdict: Status) + capability hard_gate_authority + effect derive_verdict authorized_by hard_gate_authority +{ + let d0: i32 = l2_distance_test(centroid, test0); + let d1: i32 = l2_distance_test(centroid, test1); + let g0: GateInput = GateInput { + present: MetricPresence.PRESENT, + operator: GateOperator.LE, + observed: d0 as i64, + threshold: threshold as i64, + }; + let g1: GateInput = GateInput { + present: MetricPresence.PRESENT, + operator: GateOperator.LE, + observed: d1 as i64, + threshold: threshold as i64, + }; + // Pad to four gates with always-PASS sentinels so the 4-gate + // evaluator can be reused without changing its arity. + let g2: GateInput = GateInput { + present: MetricPresence.PRESENT, + operator: GateOperator.GE, + observed: 0, + threshold: 0, + }; + let g3: GateInput = GateInput { + present: MetricPresence.PRESENT, + operator: GateOperator.GE, + observed: 0, + threshold: 0, + }; + return evaluate_gates(g0, g1, g2, g3); +} + +fn l2_distance_test(centroid: i32, sample: i32) -> (distance: i32) { + let diff: i32 = centroid - sample; + // Absolute value via branchless select: keep diff if diff>=0 else -diff. + let neg: bool = diff < 0; + if neg { + return 0 - diff; + } + return diff; +} + +// Full training run: transform dataset, shuffle, compute centroid, +// checkpoint, evaluate, and emit a content-addressed artifact digest. +// The digest is a fold over centroid + dataset fingerprint + seed so +// it is reproducible and lineage traversable. +fn run_training(a: i32, b: i32, c: i32, d: i32, spec: TrainingSpec) -> (artifact: ModelArtifact) + capability hard_gate_authority + effect derive_verdict authorized_by hard_gate_authority +{ + let raw_quad: QuadI64 = QuadI64 { a: a as i64, b: b as i64, c: c as i64, d: d as i64 }; + let transformed: QuadI64 = apply_transform_quad(raw_quad, spec.dataset.transform, spec.dataset.clip_threshold); + let shuffled: ShuffledQuad = shuffle_quad(transformed, spec.dataset.partition_seed); + let centroid_val: i32 = train_centroid(shuffled.data.a as i32, shuffled.data.b as i32, shuffled.data.c as i32, shuffled.data.d as i32); + let print: DatasetFingerprint = dataset_fingerprint(spec.dataset); + // Simple fold-based digest: (centroid as u64 +% source) *% 31 +% seed + let base: u64 = (centroid_val as u64) +% print.source; + let mixed: u64 = (base *% 31) +% spec.optimizer.seed; + let digest: u64 = (mixed *% 31) +% spec.training_code_identity; + let ckpt: Checkpoint = Checkpoint { epoch: spec.stopping.max_epochs, centroid: centroid_val, seed_state: shuffled.next_seed }; + // Evaluate on the last two shuffled elements as held-out tests. + let verdict: Status = evaluate_centroid(centroid_val, shuffled.data.c as i32, shuffled.data.d as i32, 10); + return ModelArtifact { + spec: spec, + centroid: centroid_val, + dataset_fingerprint: print, + final_checkpoint: ckpt, + evaluation_verdict: verdict, + artifact_digest: digest, + lineage_parent: spec.parent_model_identity, + }; +} + +fn validate_training_spec(spec: TrainingSpec) -> (valid: bool) { + let dataset_ok: bool = validate_dataset_spec(spec.dataset); + if dataset_ok { + let budget_ok: bool = spec.resource.max_operations > 0; + let epochs_ok: bool = spec.stopping.max_epochs > 0; + let cap_ok: bool = spec.model.capacity_target > 0; + if budget_ok { + if epochs_ok { + if cap_ok { + return true; + } + } + } + } + return false; +} diff --git a/mncs/source/mnel/verdict.mncs b/mncs/source/mnel/verdict.mncs deleted file mode 100644 index 655e349..0000000 --- a/mncs/source/mnel/verdict.mncs +++ /dev/null @@ -1,31 +0,0 @@ -mncs 0.6; - -// The evidence lattice: FAIL dominates, UNKNOWN dominates PASS, PASS alone -// survives. Missing evidence can never be promoted to success by combining. -module mnel.verdict; - -enum Verdict { PASS, FAIL, UNKNOWN } - -fn combine_verdict(left: Verdict, right: Verdict) -> (result: Verdict) { - return match left { - PASS => right, - FAIL => Verdict.FAIL, - UNKNOWN => demote_pass(right), - }; -} - -fn demote_pass(value: Verdict) -> (result: Verdict) { - return match value { - PASS => Verdict.UNKNOWN, - FAIL => Verdict.FAIL, - UNKNOWN => Verdict.UNKNOWN, - }; -} - -fn verdict_is_known(value: Verdict) -> (known: bool) { - return match value { - PASS => true, - FAIL => true, - UNKNOWN => false, - }; -} diff --git a/mncs/source/negative/cross-module-authority.mncs b/mncs/source/negative/cross-module-authority.mncs index 251f64c..d4f8bea 100644 --- a/mncs/source/negative/cross-module-authority.mncs +++ b/mncs/source/negative/cross-module-authority.mncs @@ -7,6 +7,6 @@ module mnel.negative.cross_module_authority; use mnel.gates; -fn rogue(first: GateInput, second: GateInput, third: GateInput, fourth: GateInput) -> (verdict: Verdict) { +fn rogue(first: GateInput, second: GateInput, third: GateInput, fourth: GateInput) -> (verdict: Status) { return evaluate_gates(first, second, third, fourth); } diff --git a/tests/test_mncs_reconstruction.py b/tests/test_mncs_reconstruction.py index d2e8426..7501803 100644 --- a/tests/test_mncs_reconstruction.py +++ b/tests/test_mncs_reconstruction.py @@ -26,6 +26,15 @@ REPO_ROOT.parent / "mncs-language" / "target" / "debug" / "mncs" ) DEFAULT_SOURCE = REPO_ROOT / "mncs" / "source" / "mnel" / "all.mncs" +# The reconstruction binds to mncs.core.* modules shipped with the language +# repository; this root makes those sources resolvable during elaboration. +DEFAULT_LIBRARY_ROOT = REPO_ROOT.parent / "mncs-language" / "library" + + +def library_env() -> dict: + if DEFAULT_LIBRARY_ROOT.is_dir(): + return {**os.environ, "MNCS_LIBRARY_PATH": str(DEFAULT_LIBRARY_ROOT)} + return dict(os.environ) def mncs_bin() -> Path | None: @@ -47,6 +56,7 @@ def test_source_studies_cleanly_with_only_conservative_obligations(self) -> None capture_output=True, text=True, check=True, + env=library_env(), ) payload = json.loads(completed.stdout[completed.stdout.find("{"):]) errors = [ @@ -67,7 +77,9 @@ def test_differential_study_agrees_over_corpus_on_executing_backend(self) -> Non work = REPO_ROOT / "target" / "mncs-differential-unittest" completed = subprocess.run( ["python3", str(runner), "--mncs-bin", self.mncs, - "--backend", "mncs-research-bytecode", "--work-dir", str(work)], + "--backend", "mncs-research-bytecode", + "--backend", "mncs-portable-wasm-mvp", + "--work-dir", str(work)], cwd=str(REPO_ROOT), capture_output=True, text=True, @@ -79,6 +91,48 @@ def test_differential_study_agrees_over_corpus_on_executing_backend(self) -> Non ) self.assertEqual(evidence["comparison_status"], "AGREEMENT_OVER_CORPUS") + def test_mnel_consumes_canonical_standard_library(self) -> None: + """Phase-2 architecture check: mnel.gates must elaborate through a + real import of mncs.core.status.v1, not a local copy of the lattice.""" + if not DEFAULT_LIBRARY_ROOT.is_dir(): + self.skipTest("sibling mncs-language library tree unavailable") + gates = REPO_ROOT / "mncs" / "source" / "mnel" / "gates.mncs" + source = gates.read_text() + self.assertIn("use mncs.core.status.v1;", source) + self.assertNotIn("enum Verdict", source) + for retired in ("logic.mncs", "verdict.mncs"): + self.assertFalse( + (REPO_ROOT / "mncs" / "source" / "mnel" / retired).exists(), + f"{retired} should be replaced by standard-library consumption", + ) + # The imported module must resolve through the library path and + # elaborate cleanly together with its consumer. + completed = subprocess.run( + [self.mncs, "source-study", str(gates), "--node-id", "unittest-gates"], + capture_output=True, + text=True, + env=library_env(), + ) + payload = json.loads(completed.stdout[completed.stdout.find("{"):]) + errors = [ + d for d in payload.get("diagnostics", []) if d.get("severity") == "error" + ] + self.assertEqual(errors, []) + corpus = json.loads( + (REPO_ROOT / "mncs" / "corpora" / "mnel-core-reference.json").read_text() + ) + bindings = { + case_["request"]["target"]["module"] for case_ in corpus["cases"] + } + self.assertIn( + "mncs.core.status.v1", bindings, + "corpus must exercise the canonical status module directly", + ) + self.assertIn( + "mncs.core.logic.v1", bindings, + "corpus must exercise the canonical logic module directly", + ) + def test_negative_fixtures_are_rejected(self) -> None: checker = REPO_ROOT / "tools" / "check_mncs_negative_fixtures.py" completed = subprocess.run( diff --git a/tests/test_mncs_training.py b/tests/test_mncs_training.py new file mode 100644 index 0000000..26b9229 --- /dev/null +++ b/tests/test_mncs_training.py @@ -0,0 +1,66 @@ +"""MNCS training slice tests: dataset + training + evaluation.""" + +from __future__ import annotations + +import json +import os +import subprocess +import sys +import unittest +from pathlib import Path + +REPO_ROOT = Path(__file__).resolve().parents[1] +DEFAULT_MNCS = REPO_ROOT.parent / "mncs-language" / "target" / "debug" / "mncs" +DEFAULT_SOURCE = REPO_ROOT / "mncs" / "source" / "mnel" / "training.mncs" +DEFAULT_LIBRARY_ROOT = REPO_ROOT.parent / "mncs-language" / "library" + +def library_env() -> dict: + if DEFAULT_LIBRARY_ROOT.is_dir(): + return {**os.environ, "MNCS_LIBRARY_PATH": str(DEFAULT_LIBRARY_ROOT)} + return dict(os.environ) + +def mncs_bin() -> Path | None: + configured = os.environ.get("MNCS_BIN") + candidate = Path(configured) if configured else DEFAULT_MNCS + return candidate if candidate.exists() else None + +@unittest.skipIf(mncs_bin() is None, "mncs CLI binary not available") +class MncsTrainingTests(unittest.TestCase): + def setUp(self) -> None: + self.mncs = str(mncs_bin()) + self.source = Path(os.environ.get("MNCS_TRAINING_ENTRY", str(DEFAULT_SOURCE))) + self.assertTrue(self.source.exists(), f"entry source missing: {self.source}") + + def test_training_source_studies_cleanly(self) -> None: + completed = subprocess.run( + [self.mncs, "source-study", str(self.source), "--node-id", "unittest-training"], + capture_output=True, text=True, check=True, env=library_env(), + ) + payload = json.loads(completed.stdout[completed.stdout.find("{"):]) + errors = [d for d in payload.get("diagnostics", []) if d.get("severity") == "error"] + self.assertEqual(errors, []) + self.assertEqual(payload.get("compilation_status"), "completed_with_unresolved_obligations") + + def test_dataset_source_studies_cleanly(self) -> None: + dataset = REPO_ROOT / "mncs" / "source" / "mnel" / "dataset.mncs" + completed = subprocess.run( + [self.mncs, "source-study", str(dataset), "--node-id", "unittest-dataset"], + capture_output=True, text=True, check=True, env=library_env(), + ) + payload = json.loads(completed.stdout[completed.stdout.find("{"):]) + errors = [d for d in payload.get("diagnostics", []) if d.get("severity") == "error"] + self.assertEqual(errors, []) + + def test_training_differential_agrees(self) -> None: + runner = REPO_ROOT / "tools" / "run_mnel_training_differential.py" + work = REPO_ROOT / "target" / "mnel-training-differential-unittest" + completed = subprocess.run( + ["python3", str(runner), "--mncs-bin", self.mncs, "--backend", "mncs-research-bytecode", "--backend", "mncs-portable-wasm-mvp", "--work-dir", str(work)], + cwd=str(REPO_ROOT), capture_output=True, text=True, + ) + self.assertEqual(completed.returncode, 0, completed.stdout + completed.stderr) + evidence = json.loads((REPO_ROOT / "docs" / "mncs-reconstruction" / "evidence" / "mnel-training-differential-study.json").read_text()) + self.assertEqual(evidence["comparison_status"], "AGREEMENT_OVER_CORPUS") + +if __name__ == "__main__": + unittest.main() diff --git a/tools/check_mncs_negative_fixtures.py b/tools/check_mncs_negative_fixtures.py index 251a0bd..9279d65 100644 --- a/tools/check_mncs_negative_fixtures.py +++ b/tools/check_mncs_negative_fixtures.py @@ -10,6 +10,7 @@ import argparse import json +import os import subprocess import sys from pathlib import Path @@ -17,6 +18,11 @@ REPO_ROOT = Path(__file__).resolve().parents[1] NEGATIVE_DIR = REPO_ROOT / "mncs" / "source" / "negative" +# The cross-module fixture binds through mnel.gates, which consumes +# mncs.core.status.v1; resolution uses the sibling language checkout unless +# overridden. +DEFAULT_LIBRARY_ROOT = REPO_ROOT.parent / "mncs-language" / "library" + # fixture stem -> diagnostic codes that must appear among the errors EXPECTED_ERRORS = { "authority-expansion": ["MNE134"], @@ -28,6 +34,12 @@ def main() -> int: parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("mncs_bin", help="path to the mns CLI binary") + parser.add_argument( + "--library-path", + type=Path, + default=DEFAULT_LIBRARY_ROOT if DEFAULT_LIBRARY_ROOT.is_dir() else None, + help="MNCS_LIBRARY_PATH root exposing mncs.core.*", + ) args = parser.parse_args() failures = [] @@ -36,10 +48,14 @@ def main() -> int: if not source.exists(): failures.append(f"{stem}: fixture missing") continue + environment = None + if args.library_path: + environment = {**os.environ, "MNCS_LIBRARY_PATH": str(args.library_path)} completed = subprocess.run( [args.mncs_bin, "source-study", str(source), "--node-id", f"negative-{stem}"], capture_output=True, text=True, + env=environment, ) try: payload = json.loads(completed.stdout[completed.stdout.find("{"):]) diff --git a/tools/generate_mncs_core_corpus.py b/tools/generate_mncs_core_corpus.py index fb4b7db..f603863 100644 --- a/tools/generate_mncs_core_corpus.py +++ b/tools/generate_mncs_core_corpus.py @@ -53,7 +53,8 @@ # Home modules after the modularization of the reconstruction: every # declaration's identity is anchored to the module that declares it. MODULE_CORE = "mnel.core" -MODULE_VERDICT = "mnel.verdict" +MODULE_STATUS_STD = "mncs.core.status.v1" +MODULE_LOGIC_STD = "mncs.core.logic.v1" MODULE_GATES = "mnel.gates" MODULE_LIFECYCLE = "mnel.lifecycle" MODULE_VISIBILITY = "mnel.visibility" @@ -88,7 +89,7 @@ def encode_component(value: str) -> str: TYPE_HOME_MODULE = { - "Verdict": MODULE_VERDICT, + "Status": MODULE_STATUS_STD, "GateOperator": MODULE_GATES, "MetricPresence": MODULE_GATES, "GateInput": MODULE_GATES, @@ -107,8 +108,11 @@ def encode_component(value: str) -> str: } FUNCTION_HOME_MODULE = { - "combine_verdict": MODULE_VERDICT, - "verdict_is_known": MODULE_VERDICT, + "dominate": MODULE_STATUS_STD, + "is_decided": MODULE_STATUS_STD, + "bool_and": MODULE_LOGIC_STD, + "bool_or": MODULE_LOGIC_STD, + "bool_not": MODULE_LOGIC_STD, "evaluate_gate": MODULE_GATES, "evaluate_gates": MODULE_GATES, "access_granted": MODULE_VISIBILITY, @@ -264,7 +268,7 @@ def case(case_id: str, function: str, arguments: list, expected: list, *, oracle ] OUTCOME_FIELDS = [ ("final_state", "ExperimentState"), - ("verdict", "Verdict"), + ("verdict", "Status"), ("principle_maturity", "Maturity"), ] @@ -284,7 +288,7 @@ def gate_input(present: bool, op: str, observed: int, threshold: int) -> dict: def verdict_value(verdict_text: str) -> dict: - return finite("Verdict", verdict_text, VERDICT[verdict_text]) + return finite("Status", verdict_text, VERDICT[verdict_text]) def transition_outcome(advanced: bool, next_state: str, reason: str) -> dict: @@ -542,8 +546,8 @@ def build_cases() -> list[dict]: combined = right cases.append(case( f"combine-{left.lower()}-{right.lower()}", - "combine_verdict", - [finite("Verdict", left, VERDICT[left]), finite("Verdict", right, VERDICT[right])], + "dominate", + [finite("Status", left, VERDICT[left]), finite("Status", right, VERDICT[right])], [verdict_value(combined)], oracle=ORACLE_DERIVED_TABLE, oracle_citation="HardGateEvaluator aggregation rule " @@ -551,6 +555,43 @@ def build_cases() -> list[dict]: "UNKNOWN => UNKNOWN; else PASS.", )) + # --- Boolean algebra binding to mncs.core.logic.v1 ---------------------- + # The reconstruction previously carried local helpers `both`/`either`/`not` + # (mnel.logic, if/else truth tables). They are replaced by the canonical + # standard-library operations; these cases pin that replacement to the + # exact truth tables the reference modules used. + for a in (False, True): + for b in (False, True): + cases.append(case( + f"bool-and-{int(a)}-{int(b)}", + "bool_and", + [boolean(a), boolean(b)], + [boolean(a and b)], + oracle=ORACLE_DERIVED_TABLE, + oracle_citation="former mnel.logic.both " + "(mncs/source/mnel/logic.mncs before stdlib binding): " + "if left { right } else false.", + )) + cases.append(case( + f"bool-or-{int(a)}-{int(b)}", + "bool_or", + [boolean(a), boolean(b)], + [boolean(a or b)], + oracle=ORACLE_DERIVED_TABLE, + oracle_citation="former mnel.logic.either " + "(mncs/source/mnel/logic.mncs before stdlib binding): " + "if left { true } else right.", + )) + cases.append(case( + f"bool-not-{int(a)}-{b and 1 or 0}", + "bool_not", + [boolean(a)], + [boolean(not a)], + oracle=ORACLE_DERIVED_TABLE, + oracle_citation="former mnel.logic.not " + "(mncs/source/mnel/logic.mncs before stdlib binding).", + )) + # --- Hard gates (real evaluator) --------------------------------------- gate_specs = [ # (op, threshold, observed, present) diff --git a/tools/generate_mnel_training_corpus.py b/tools/generate_mnel_training_corpus.py new file mode 100644 index 0000000..3b44834 --- /dev/null +++ b/tools/generate_mnel_training_corpus.py @@ -0,0 +1,526 @@ +#!/usr/bin/env python3 +"""Generate deterministic MNCS execution corpora for the mnel.dataset + mnel.training slice. + +Each case is computed by driving a Python reference oracle that mirrors the MNCS +implementation. The corpora are then executed by the MNCS-language implementation +through the mncs compiler backends, and case-level agreement is reported. + +Oracle kinds: + - "reference-code": expected value produced by Python oracle function + - "derived-table": documented MNCS behavior with citation + +Determinism: no clocks, no randomness, sorted iteration. +""" + +from __future__ import annotations + +import hashlib +import json +import sys +from pathlib import Path + +REPO_ROOT = Path(__file__).resolve().parents[1] +SRC = REPO_ROOT / "src" +if str(SRC) not in sys.path: + sys.path.insert(0, str(SRC)) + +# Reference oracles are pure Python mirrors of MNCS logic +SOURCE_PATH = REPO_ROOT / "mncs" / "source" / "mnel" / "all.mncs" +SOURCES = sorted((REPO_ROOT / "mncs" / "source" / "mnel").glob("*.mncs")) +OUTPUT_PATH = REPO_ROOT / "mncs" / "corpora" / "mnel-training-reference.json" + +MODULE_DATASET = "mnel.dataset" +MODULE_TRAINING = "mnel.training" +MODULE_STATUS_STD = "mncs.core.status.v1" +MODULE_RANDOM_STD = "mncs.core.random.v1" +MODULE_NUMERIC_STD = "mncs.core.numeric.v1" + +STEP_BUDGET = 512 +GENERATOR_IDENTITY = "mnel-training-corpus-generator/0.1" +ORACLE_REFERENCE_CODE = "reference-code" +ORACLE_DERIVED_TABLE = "derived-table" + +# --------------------------------------------------------------------------- +# MNCS value encoding (mirrors crates/mncs-model/src/identity.rs) +# --------------------------------------------------------------------------- + +def encode_component(value: str) -> str: + out = [] + for byte in value.encode("utf-8"): + ch = chr(byte) + if ch.isascii() and (ch.isalnum() or ch in "_-."): + out.append(ch) + else: + out.append(f"%{byte:02X}") + return "".join(out) + +TYPE_HOME_MODULE = { + "Status": MODULE_STATUS_STD, + "TransformKind": MODULE_DATASET, + "DatasetSpec": MODULE_DATASET, + "DatasetFingerprint": MODULE_DATASET, + "SplitCounts": MODULE_DATASET, + "QuadI64": MODULE_DATASET, + "ShuffledQuad": MODULE_DATASET, + "ModelFamily": MODULE_TRAINING, + "OptimizerKind": MODULE_TRAINING, + "Precision": MODULE_TRAINING, + "DeviceKind": MODULE_TRAINING, + "ModelSpec": MODULE_TRAINING, + "OptimizerSpec": MODULE_TRAINING, + "ResourcePolicy": MODULE_TRAINING, + "CheckpointPolicy": MODULE_TRAINING, + "StoppingRule": MODULE_TRAINING, + "EvaluationSpec": MODULE_TRAINING, + "TrainingSpec": MODULE_TRAINING, + "Checkpoint": MODULE_TRAINING, + "ModelArtifact": MODULE_TRAINING, + "GateOperator": "mnel.gates", + "MetricPresence": "mnel.gates", + "GateInput": "mnel.gates", + "BoundedDraw": MODULE_RANDOM_STD, + "ShufflePick": MODULE_RANDOM_STD, +} + +FUNCTION_HOME_MODULE = { + "apply_transform_quad": MODULE_DATASET, + "shuffle_quad": MODULE_DATASET, + "split_counts": MODULE_DATASET, + "dataset_fingerprint": MODULE_DATASET, + "validate_dataset_spec": MODULE_DATASET, + "swap_quad": MODULE_DATASET, + "train_centroid": MODULE_TRAINING, + "sgd_step": MODULE_TRAINING, + "batch_centroid": MODULE_TRAINING, + "evaluate_centroid": MODULE_TRAINING, + "l2_distance_test": MODULE_TRAINING, + "validate_training_spec": MODULE_TRAINING, + "clamp_one": MODULE_DATASET, + "centroid4": MODULE_NUMERIC_STD, + "lcg_next": MODULE_RANDOM_STD, + "lcg_next_bounded": MODULE_RANDOM_STD, +} + +def finite_type_id(module_name: str, name: str) -> str: + return f"mncs:0.2:finite-type:{encode_component(module_name)}::{encode_component(name)}" + +def finite_variant_id(module_name: str, type_name: str, variant: str) -> str: + return ( + f"mncs:0.2:finite-variant:{encode_component(module_name)}" + f"::{encode_component(type_name)}::{encode_component(variant)}" + ) + +def record_type_id(module_name: str, name: str, fields: list[tuple[str, str]]) -> str: + canonical = sorted(fields) + joined = "".join(f"{fname}:{ftype};" for fname, ftype in canonical) + return ( + f"mncs:0.2:record-type:{encode_component(module_name)}" + f"::{encode_component(name)}::{encode_component(joined)}" + ) + +def type_module(type_name: str) -> str: + try: + return TYPE_HOME_MODULE[type_name] + except KeyError: + raise AssertionError(f"declare the home module for type {type_name}") + +def fn_module(function: str) -> str: + try: + return FUNCTION_HOME_MODULE[function] + except KeyError: + raise AssertionError(f"declare the home module for function {function}") + +def finite(type_name: str, variant: str, discriminant: int) -> dict: + home = type_module(type_name) + return { + "finite": { + "type_identity": finite_type_id(home, type_name), + "variant_identity": finite_variant_id(home, type_name, variant), + "discriminant": discriminant, + } + } + +def integer(value: int, bits: int = 64, signed: bool = True) -> dict: + return {"integer": {"value": value, "type": {"bits": bits, "signed": signed}}} + +def integer_i64(v: int) -> dict: + return integer(v, bits=64, signed=True) + +def integer_i32(v: int) -> dict: + return integer(v, bits=32, signed=True) + +def integer_u64(v: int) -> dict: + return integer(v, bits=64, signed=False) + +def boolean(value: bool) -> dict: + return {"boolean": {"value": value}} + +def record(name: str, fields: list[tuple[str, str]], values: dict) -> dict: + return { + "record": { + "type_identity": record_type_id(type_module(name), name, fields), + "name": name, + "fields": [[fname, values[fname]] for fname in sorted(values)], + } + } + +def case(case_id: str, function: str, arguments: list, expected: list, *, oracle: str, + oracle_citation: str, expected_status: str | None = None) -> dict: + request = { + "schema_version": "0.1", + "target": {"module": fn_module(function), "function": function}, + "arguments": arguments, + "step_budget": STEP_BUDGET, + } + entry = { + "id": case_id, + "request": request, + "expected": expected, + "oracle": {"kind": oracle, "citation": oracle_citation}, + } + if expected_status is not None: + entry["expected_status"] = expected_status + return entry + +# Enum discriminants: declaration order in source +TRANSFORM_KIND = {"IDENTITY": 0, "CLIP": 1} +MODEL_FAMILY = {"TABULAR_CENTROID": 0, "TRANSITION_FREQUENCY": 1, "TINY_LINEAR": 2} +OPTIMIZER_KIND = {"COUNTING": 0, "SGD_WRAP": 1} +PRECISION = {"P32": 0, "P64": 1} +DEVICE_KIND = {"CPU": 0, "WASM": 1, "NATIVE": 2} +GATE_OP = {"GE": 0, "GT": 1, "LE": 2, "LT": 3, "EQ": 4} +PRESENCE = {"PRESENT": 0, "ABSENT": 1} +STATUS = {"PASS": 0, "FAIL": 1, "UNKNOWN": 2} + +QUAD_FIELDS = [("a", "i64"), ("b", "i64"), ("c", "i64"), ("d", "i64")] +SHUFFLED_QUAD_FIELDS = [("data", "QuadI64"), ("next_seed", "u64")] +DATASET_SPEC_FIELDS = [("source_identity", "u64"), ("transform", "TransformKind"), ("clip_threshold", "i64"), ("partition_seed", "u64"), ("train_numer", "i64"), ("train_denom", "i64")] +DATASET_FPRINT_FIELDS = [("source", "u64"), ("transform", "TransformKind"), ("seed", "u64"), ("train_numer", "i64"), ("train_denom", "i64"), ("threshold", "i64")] +SPLIT_COUNTS_FIELDS = [("train_count", "i64"), ("test_count", "i64")] + +# helpers to encode Quad etc. + +def quad_i64(a: int, b: int, c: int, d: int) -> dict: + return record("QuadI64", QUAD_FIELDS, { + "a": integer_i64(a), + "b": integer_i64(b), + "c": integer_i64(c), + "d": integer_i64(d), + }) + +def shuffled_quad(quad: dict, next_seed: int) -> dict: + # quad is already encoded record dict's inner fields? We need to pass record value + # The field "data" expects a QuadI64 record value + return record("ShuffledQuad", SHUFFLED_QUAD_FIELDS, { + "data": quad, + "next_seed": integer_u64(next_seed), + }) + +def transform_kind(variant: str) -> dict: + return finite("TransformKind", variant, TRANSFORM_KIND[variant]) + +def model_family(variant: str) -> dict: + return finite("ModelFamily", variant, MODEL_FAMILY[variant]) + +def optimizer_kind(variant: str) -> dict: + return finite("OptimizerKind", variant, OPTIMIZER_KIND[variant]) + +def status_value(variant: str) -> dict: + return finite("Status", variant, STATUS[variant]) + +# --------------------------------------------------------------------------- +# Python oracles mirroring MNCS logic +# --------------------------------------------------------------------------- + +def oracle_clamp_one(value: int, bound: int) -> int: + neg = 0 - bound + if value < neg: + return neg + if value > bound: + return bound + return value + +def oracle_apply_transform_quad(quad: tuple[int,int,int,int], kind: str, threshold: int) -> tuple[int,int,int,int]: + a,b,c,d = quad + if kind == "IDENTITY": + return (a,b,c,d) + else: # CLIP + return (oracle_clamp_one(a, threshold), oracle_clamp_one(b, threshold), oracle_clamp_one(c, threshold), oracle_clamp_one(d, threshold)) + +def lcg_next(state: int) -> int: + # wrapping 64-bit: (state * A + C) % 2**64 + return ((state * 6364136223846793005) + 1442695040888963407) & 0xFFFFFFFFFFFFFFFF + +def lcg_next_bounded(state: int, bound: int) -> tuple[int,int]: + nxt = lcg_next(state) + if bound == 0: + return (nxt, 0) + return (nxt, nxt % bound) + +def oracle_swap_quad(quad: tuple[int,int,int,int], a: int, b: int) -> tuple[int,int,int,int]: + lst = list(quad) + if a == b: + return tuple(lst) + # swap positions a and b + lst[a], lst[b] = lst[b], lst[a] + return tuple(lst) + +def oracle_shuffle_quad(quad: tuple[int,int,int,int], seed: int) -> tuple[tuple[int,int,int,int], int]: + # Mirrors MNCS shuffle_quad: three steps swapping with bounded draws + step0_nxt, idx0 = lcg_next_bounded(seed, 4) + after0 = oracle_swap_quad(quad, 0, idx0) + step1_nxt, idx1 = lcg_next_bounded(step0_nxt, 4) + after1 = oracle_swap_quad(after0, 1, idx1) + step2_nxt, idx2 = lcg_next_bounded(step1_nxt, 4) + after2 = oracle_swap_quad(after1, 2, idx2) + return (after2, step2_nxt) + +def oracle_split_counts(numer: int, denom: int) -> tuple[int,int]: + if denom == 0: + return (0,4) + if numer < 0: + return (0,4) + if numer > denom: + return (4,0) + train = (4 * numer) // denom + test = 4 - train + return (train, test) + +def oracle_validate_dataset_spec(source: int, denom: int) -> bool: + return source != 0 and denom != 0 + +def oracle_train_centroid(a: int, b: int, c: int, d: int) -> int: + # centroid4 via wrapping sum then /4 - but with small values no wrap, use Python ints + # Use 32-bit wrapping for fidelity, but small values avoid overflow + # Emulate i32 wrapping sum: & 0xFFFFFFFF then interpret + s = (a + b + c + d) & 0xFFFFFFFF + # interpret as signed 32 + if s & 0x80000000: + s = s - 0x100000000 + return s // 4 # integer division trunc toward negative? MNCS uses / with signed i32: need to check. For small positive, // matches. + # For our small positive test values, this is fine. + +def oracle_sgd_step(current: int, sample: int, numer: int, denom: int) -> int: + if denom == 0: + return current + diff = sample - current + scaled = (diff * numer) // denom + # wrapping add in i32 + res = (current + scaled) & 0xFFFFFFFF + if res & 0x80000000: + res = res - 0x100000000 + return res + +def oracle_batch_centroid(a: int, b: int, c: int, d: int, seed: int, batch_size: int) -> int: + quad = (a,b,c,d) + shuffled, _ = oracle_shuffle_quad((a,b,c,d), seed) # but need i64? Use ints directly; shuffling uses same logic + # Actually shuffling should operate on i64 values, but ints are small so same. + # Use shuffled result + s = shuffled + if batch_size <= 1: + return s[0] + if batch_size == 2: + return (s[0] + s[1]) // 2 + if batch_size == 3: + return (s[0] + s[1] + s[2]) // 3 + return oracle_train_centroid(s[0], s[1], s[2], s[3]) + +def oracle_l2_distance(centroid: int, sample: int) -> int: + diff = centroid - sample + return abs(diff) + +def oracle_evaluate_centroid(centroid: int, test0: int, test1: int, threshold: int) -> str: + d0 = oracle_l2_distance(centroid, test0) + d1 = oracle_l2_distance(centroid, test1) + # two gates LE threshold + g0_pass = d0 <= threshold + g1_pass = d1 <= threshold + # overall via dominate: FAIL > UNKNOWN > PASS, but here only PASS/FAIL + if not g0_pass or not g1_pass: + return "FAIL" + return "PASS" + +# --------------------------------------------------------------------------- +# Corpus assembly +# --------------------------------------------------------------------------- + +def build_cases() -> list[dict]: + cases: list[dict] = [] + + # --- clamp_one --------------------------------------------------------- + for val, bound, expected in [(5, 10, 5), (15, 10, 10), (-15, 10, -10), (0, 5, 0)]: + cases.append(case( + f"clamp-one-{val}-{bound}", + "clamp_one", + [integer_i64(val), integer_i64(bound)], + [integer_i64(expected)], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.dataset.clamp_one: clamp to [-bound, bound] via comparisons", + )) + + # --- apply_transform_quad ---------------------------------------------- + for kind in ["IDENTITY", "CLIP"]: + for quad, thresh in [((1,2,3,4), 10), ((15, -20, 5, 0), 10), ((100, 200, -300, 5), 10)]: + expected = oracle_apply_transform_quad(quad, kind, thresh) + cases.append(case( + f"apply-transform-quad-{kind.lower()}-{quad[0]}-{thresh}", + "apply_transform_quad", + [quad_i64(*quad), transform_kind(kind), integer_i64(thresh)], + [quad_i64(*expected)], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.dataset.apply_transform_quad: per-lane IDENTITY vs CLIP", + )) + + # --- shuffle_quad ------------------------------------------------------- + for quad, seed in [((1,2,3,4), 0), ((10,20,30,40), 42), ((5,5,5,5), 12345), ((1,2,3,4), 999)]: + expected_quad, next_seed = oracle_shuffle_quad(quad, seed) + cases.append(case( + f"shuffle-quad-{seed}-{quad[0]}", + "shuffle_quad", + [quad_i64(*quad), integer_u64(seed)], + [shuffled_quad(quad_i64(*expected_quad), next_seed)], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.dataset.shuffle_quad: deterministic LCG permutation over 4 lanes", + )) + + # --- split_counts ------------------------------------------------------- + for numer, denom in [(2,4), (0,4), (4,4), (1,2), (3,0), (-1,4), (5,4)]: + exp_train, exp_test = oracle_split_counts(numer, denom) + cases.append(case( + f"split-counts-{numer}-{denom}", + "split_counts", + [integer_i64(numer), integer_i64(denom)], + [record("SplitCounts", SPLIT_COUNTS_FIELDS, {"train_count": integer_i64(exp_train), "test_count": integer_i64(exp_test)})], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.dataset.split_counts: train = floor(4*numer/denom) clamp [0,4]", + )) + + # --- validate_dataset_spec --------------------------------------------- + for source, denom, expected in [(123, 4, True), (0, 4, False), (123, 0, False), (0,0, False)]: + spec = record("DatasetSpec", DATASET_SPEC_FIELDS, { + "source_identity": integer_u64(source), + "transform": transform_kind("IDENTITY"), + "clip_threshold": integer_i64(10), + "partition_seed": integer_u64(0), + "train_numer": integer_i64(2), + "train_denom": integer_i64(denom), + }) + # monkey patch source + # need to override source_identity + spec["record"]["fields"] = [[k, v] for k,v in sorted({ + "source_identity": integer_u64(source), + "transform": transform_kind("IDENTITY"), + "clip_threshold": integer_i64(10), + "partition_seed": integer_u64(0), + "train_numer": integer_i64(2), + "train_denom": integer_i64(denom), + }.items())] + cases.append(case( + f"validate-dataset-{source}-{denom}", + "validate_dataset_spec", + [spec], + [boolean(expected)], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.dataset.validate_dataset_spec: source !=0 and denom !=0", + )) + + # --- train_centroid ----------------------------------------------------- + for quad in [(0,0,0,0), (4,8,12,16), (10,20,30,40), (1,2,3,4), (-4, -8, 12, 16)]: + expected = oracle_train_centroid(*quad) + cases.append(case( + f"train-centroid-{quad[0]}-{quad[1]}-{quad[2]}-{quad[3]}", + "train_centroid", + [integer_i32(quad[0]), integer_i32(quad[1]), integer_i32(quad[2]), integer_i32(quad[3])], + [integer_i32(expected)], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.training.train_centroid via mncs.core.numeric.centroid4 wrapping reduce", + )) + + # --- sgd_step ----------------------------------------------------------- + for cur, samp, numer, denom, expected in [ + (10, 20, 1, 2, 15), # diff 10 *0.5 =5 + (10, 20, 1, 1, 20), # diff 10 *1 =10 + (10, 20, 0, 1, 10), # lr 0 + (10, 20, 1, 0, 10), # denom 0 => no update + (0, 100, 1, 4, 25), + ]: + exp = oracle_sgd_step(cur, samp, numer, denom) + cases.append(case( + f"sgd-step-{cur}-{samp}-{numer}-{denom}", + "sgd_step", + [integer_i32(cur), integer_i32(samp), integer_i64(numer), integer_i64(denom)], + [integer_i32(exp)], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.training.sgd_step: current +% ((sample-current)*numer/denom)", + )) + + # --- batch_centroid ----------------------------------------------------- + for quad, seed, bsize in [((10,20,30,40), 42, 1), ((10,20,30,40), 42, 2), ((1,2,3,4), 0, 4), ((5,6,7,8), 999, 3)]: + expected = oracle_batch_centroid(*quad, seed, bsize) + cases.append(case( + f"batch-centroid-{bsize}-{seed}", + "batch_centroid", + [integer_i32(quad[0]), integer_i32(quad[1]), integer_i32(quad[2]), integer_i32(quad[3]), integer_u64(seed), integer_i64(bsize)], + [integer_i32(expected)], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.training.batch_centroid: shuffle then mean of first batch_size", + )) + + # --- l2_distance_test --------------------------------------------------- + for cent, samp in [(10, 3), (10, 15), (0, 0), (-5, 5)]: + expected = oracle_l2_distance(cent, samp) + cases.append(case( + f"l2-distance-{cent}-{samp}", + "l2_distance_test", + [integer_i32(cent), integer_i32(samp)], + [integer_i32(expected)], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.training.l2_distance_test: abs(centroid-sample)", + )) + + # --- evaluate_centroid -------------------------------------------------- + for cent, t0, t1, thresh, expected in [ + (10, 10, 10, 0, "PASS"), + (10, 12, 10, 5, "PASS"), + (10, 20, 10, 5, "FAIL"), + (10, 20, 20, 5, "FAIL"), + ]: + cases.append(case( + f"evaluate-centroid-{cent}-{t0}-{t1}-{thresh}", + "evaluate_centroid", + [integer_i32(cent), integer_i32(t0), integer_i32(t1), integer_i32(thresh)], + [status_value(expected)], + oracle=ORACLE_REFERENCE_CODE, + oracle_citation="mnel.training.evaluate_centroid: two LE gates joined by dominate", + )) + + return cases + +def main() -> int: + combined = b"".join(p.read_bytes() for p in SOURCES) + sources_digest = hashlib.sha256(combined).hexdigest() + cases = build_cases() + corpus = { + "schema_version": "0.1", + "name": "mnel-training-reference-v1", + "cases": cases, + "provenance": { + "generator_identity": GENERATOR_IDENTITY, + "reference_package": "mnel (Machine-Native-Experimental-Learning)", + "mncs_sources": [str(p.relative_to(REPO_ROOT)) for p in SOURCES], + "mncs_sources_sha256": sources_digest, + "oracle_kinds": { + "reference-code": "expected values produced by Python oracle", + "derived-table": "expected values encode documented MNCS behavior", + }, + "determinism": "frozen inputs; no clock or randomness; sorted iteration", + }, + } + OUTPUT_PATH.parent.mkdir(parents=True, exist_ok=True) + OUTPUT_PATH.write_text(json.dumps(corpus, indent=1, sort_keys=False) + "\n") + print(f"wrote {len(cases)} cases to {OUTPUT_PATH.relative_to(REPO_ROOT)}") + print(f"combined source sha256: {sources_digest}") + return 0 + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/run_mncs_differential.py b/tools/run_mncs_differential.py index 83f0214..6b8e22e 100644 --- a/tools/run_mncs_differential.py +++ b/tools/run_mncs_differential.py @@ -25,6 +25,7 @@ import argparse import hashlib import json +import os import subprocess import sys from pathlib import Path @@ -44,14 +45,27 @@ BACKENDS = { "mncs-research-bytecode": "bytecode", "mncs-portable-wasm-mvp": "wasm", + "mncs-c11": "c11", + "mncs-llvm-ir": "llvm", + "mncs-cranelift": "cranelift", + "mncs-riscv32": "riscv32", + "mncs-ebpf": "ebpf", + "mncs-ptx64": "ptx64", } +# The MNEL modules bind to mncs.core.* standard-library sources shipped in +# the sibling language repository; resolution degrades to an honest +# unresolvable-import failure when this default does not exist. +DEFAULT_LIBRARY_ROOT = REPO_ROOT.parent / "mncs-language" / "library" + def sha256_file(path: Path) -> str: return hashlib.sha256(path.read_bytes()).hexdigest() -def run_mncs(mncs_bin: list[str], backend: str, out_dir: Path) -> tuple[int, dict | None]: +def run_mncs( + mncs_bin: list[str], backend: str, out_dir: Path, library_path: str | None +) -> tuple[int, dict | None]: out_dir.mkdir(parents=True, exist_ok=True) command = [ *mncs_bin, @@ -65,7 +79,10 @@ def run_mncs(mncs_bin: list[str], backend: str, out_dir: Path) -> tuple[int, dic "--output-dir", str(out_dir), ] - completed = subprocess.run(command, capture_output=True, text=True) + environment = None + if library_path: + environment = {**os.environ, "MNCS_LIBRARY_PATH": library_path} + completed = subprocess.run(command, capture_output=True, text=True, env=environment) stdout = completed.stdout try: payload = json.loads(stdout[stdout.find("{"):]) @@ -115,6 +132,13 @@ def main() -> int: ) parser.add_argument("--backend", choices=sorted(BACKENDS), action="append", help="restrict to one backend (repeatable)") + parser.add_argument( + "--library-path", + type=Path, + default=DEFAULT_LIBRARY_ROOT if DEFAULT_LIBRARY_ROOT.is_dir() else None, + help="MNCS_LIBRARY_PATH root exposing mncs.core.* (default: sibling " + "mncs-language checkout)", + ) args = parser.parse_args() if not CORPUS_PATH.exists(): @@ -128,7 +152,8 @@ def main() -> int: disagreements = [] for backend in selected_backends: tag = BACKENDS[backend] - rc, payload = run_mncs(args.mncs_bin, backend, args.work_dir / tag) + library = str(args.library_path) if args.library_path else None + rc, payload = run_mncs(args.mncs_bin, backend, args.work_dir / tag, library) outcome, details_list, summary = classify_backend_result(rc, payload) observation = { "backend": backend, @@ -183,8 +208,13 @@ def main() -> int: "mncs_side": { "source": str(SOURCE_PATH.relative_to(REPO_ROOT)), "source_sha256": sha256_file(SOURCE_PATH), - "module": "mnel.core", - "language_profile": "0.5", + "module": "mnel.all", + "language_profile": "0.6", + "standard_library_bindings": [ + "mncs.core.status.v1", + "mncs.core.logic.v1", + ], + "library_path": str(args.library_path) if args.library_path else None, }, "backends": backend_observations, "comparison_status": comparison_status, diff --git a/tools/run_mnel_training_differential.py b/tools/run_mnel_training_differential.py new file mode 100644 index 0000000..be541dc --- /dev/null +++ b/tools/run_mnel_training_differential.py @@ -0,0 +1,168 @@ +#!/usr/bin/env python3 +"""Run the MNEL-training differential study: reference vs MNCS training slice. + +Pipeline: same frozen inputs (mncs/corpora/mnel-training-reference.json) executed +through the MNCS training modules (mnel.dataset + mnel.training) via compiler backends. + +Outputs a bounded-differential evidence record under docs/mncs-reconstruction/evidence/. +""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import os +import subprocess +import sys +from pathlib import Path + +REPO_ROOT = Path(__file__).resolve().parents[1] +CORPUS_PATH = REPO_ROOT / "mncs" / "corpora" / "mnel-training-reference.json" +SOURCE_PATH = REPO_ROOT / "mncs" / "source" / "mnel" / "training.mncs" +EVIDENCE_DIR = REPO_ROOT / "docs" / "mncs-reconstruction" / "evidence" + +RUNNER_IDENTITY = "mnel-mncs-differential-runner/0.1" +STUDY_IDENTITY = "mnel-training-slice" +INTERPRETATION = ( + "bounded_observational_agreement_over_declared_corpus; " + "not_universal_equivalence_not_conformance_not_assurance" +) + +BACKENDS = { + "mncs-research-bytecode": "bytecode", + "mncs-portable-wasm-mvp": "wasm", + "mncs-c11": "c11", + "mncs-llvm-ir": "llvm", + "mncs-cranelift": "cranelift", + "mncs-riscv32": "riscv32", + "mncs-ebpf": "ebpf", + "mncs-ptx64": "ptx64", +} + +DEFAULT_LIBRARY_ROOT = REPO_ROOT.parent / "mncs-language" / "library" + +def sha256_file(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + +def run_mncs(mncs_bin: list[str], backend: str, out_dir: Path, library_path: str | None) -> tuple[int, dict | None]: + out_dir.mkdir(parents=True, exist_ok=True) + command = [ + *mncs_bin, + "experiment", + "run", + str(SOURCE_PATH), + "--backend", + backend, + "--corpus", + str(CORPUS_PATH), + "--output-dir", + str(out_dir), + ] + environment = None + if library_path: + environment = {**os.environ, "MNCS_LIBRARY_PATH": library_path} + completed = subprocess.run(command, capture_output=True, text=True, env=environment) + stdout = completed.stdout + try: + payload = json.loads(stdout[stdout.find("{"):]) + except (ValueError, TypeError): + payload = None + return completed.returncode, payload + +def classify_backend_result(rc: int, payload: dict | None) -> tuple[str, list[dict], dict]: + if payload is None: + return "runner-error", [], {"exit_code": rc} + diagnostics = payload.get("diagnostics") or [] + refusal_codes = [d for d in diagnostics if str(d.get("code", "")).startswith(("CGN3", "CGR3"))] + cases = payload.get("cases") or [] + if refusal_codes and not cases: + return "backend-refused-out-of-envelope", refusal_codes, {"exit_code": rc, "compilation_status": payload.get("status")} + met = sum(1 for c in cases if c.get("expectation_met") is True) + unmet = [c for c in cases if c.get("expectation_met") is not True] + return "corpus-executed", unmet, {"exit_code": rc, "cases_total": len(cases), "cases_met": met, "experiment_status": payload.get("status"), "unresolved_reasons": payload.get("unresolved_reasons") or []} + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--mncs-bin", nargs="+", default=["cargo", "run", "--quiet", "-p", "mncs-cli", "--"], help="command prefix that runs the mncs CLI") + parser.add_argument("--work-dir", type=Path, default=REPO_ROOT / "target" / "mnel-training-differential", help="directory for per-backend outputs") + parser.add_argument("--backend", choices=sorted(BACKENDS), action="append", help="restrict to one backend (repeatable)") + parser.add_argument("--library-path", type=Path, default=DEFAULT_LIBRARY_ROOT if DEFAULT_LIBRARY_ROOT.is_dir() else None, help="MNCS_LIBRARY_PATH root") + args = parser.parse_args() + if not CORPUS_PATH.exists(): + print("corpus missing; run tools/generate_mnel_training_corpus.py first", file=sys.stderr) + return 2 + corpus = json.loads(CORPUS_PATH.read_text()) + selected_backends = args.backend or list(BACKENDS) + backend_observations = [] + disagreements = [] + for backend in selected_backends: + tag = BACKENDS[backend] + library = str(args.library_path) if args.library_path else None + rc, payload = run_mncs(args.mncs_bin, backend, args.work_dir / tag, library) + outcome, details_list, summary = classify_backend_result(rc, payload) + observation = {"backend": backend, "outcome": outcome, "summary": summary} + if outcome == "backend-refused-out-of-envelope": + observation["refusal_diagnostics"] = [{"code": d.get("code"), "message": d.get("message")} for d in details_list[:8]] + observation["interpretation"] = "fail-closed envelope refusal; absence of execution is not disagreement" + elif outcome == "corpus-executed": + for case in details_list: + disagreements.append({"backend": backend, "case_id": case.get("case_id"), "failure_reason": case.get("failure_reason")}) + backend_observations.append(observation) + executed = [b for b in backend_observations if b["outcome"] == "corpus-executed"] + if disagreements: + comparison_status = "MISMATCH_DETECTED" + elif executed: + comparison_status = "AGREEMENT_OVER_CORPUS" + else: + comparison_status = "NO_EXECUTING_BACKEND" + evidence = { + "schema_version": "0.1", + "identity_kind": "bounded-differential-study-record", + "study": STUDY_IDENTITY, + "runner_identity": RUNNER_IDENTITY, + "interpretation": INTERPRETATION, + "reference_side": { + "implementation": "Machine-Native-Experimental-Learning src/mnel (Python control plane)", + "corpus": str(CORPUS_PATH.relative_to(REPO_ROOT)), + "corpus_sha256": sha256_file(CORPUS_PATH), + "cases": len(corpus.get("cases", [])), + "oracle_kinds": sorted({c.get("oracle", {}).get("kind") for c in corpus.get("cases", []) if c.get("oracle")}), + }, + "mncs_side": { + "source": str(SOURCE_PATH.relative_to(REPO_ROOT)), + "source_sha256": sha256_file(SOURCE_PATH), + "module": "mnel.training", + "language_profile": "0.8", + "standard_library_bindings": ["mncs.core.status.v1", "mncs.core.random.v1", "mncs.core.numeric.v1"], + "library_path": str(args.library_path) if args.library_path else None, + }, + "backends": backend_observations, + "comparison_status": comparison_status, + "disagreements": disagreements, + "non_claims": [ + "observed agreement is not proof of semantic equivalence", + "the corpus covers a bounded slice of MNEL training concepts only", + "backend envelope refusals are recorded, not resolved", + "unresolved obligations remain UNKNOWN; nothing here certifies the MNCS implementation against the reference beyond the corpus", + ], + } + EVIDENCE_DIR.mkdir(parents=True, exist_ok=True) + out_path = EVIDENCE_DIR / "mnel-training-differential-study.json" + out_path.write_text(json.dumps(evidence, indent=1) + "\n") + print(f"comparison: {comparison_status}") + for b in backend_observations: + summary = b.get("summary", {}) + if "cases_met" in summary: + print(f" {b['backend']}: {summary['cases_met']}/{summary['cases_total']} (status={summary.get('experiment_status')})") + else: + print(f" {b['backend']}: {b['outcome']}") + print(f"evidence: {out_path.relative_to(REPO_ROOT)}") + if disagreements: + for d in disagreements[:20]: + print(f" DISAGREE {d['backend']} {d['case_id']}: {d['failure_reason']}") + return 1 + return 0 + +if __name__ == "__main__": + raise SystemExit(main())