From e7917e5d2033c43ea588bdc8543a5888fc19c4b9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 12 Jun 2026 23:42:12 +0000 Subject: [PATCH 1/2] WIP: English emit target (operator-requested, output ASAP): make the Controll --- src/v4/extdeps/languages/english.dag | 47 +++++++++++++++++++++++++--- 1 file changed, 42 insertions(+), 5 deletions(-) diff --git a/src/v4/extdeps/languages/english.dag b/src/v4/extdeps/languages/english.dag index ee13d2417e5..b41db0de2fe 100644 --- a/src/v4/extdeps/languages/english.dag +++ b/src/v4/extdeps/languages/english.dag @@ -1,13 +1,43 @@ // src/v4/extdeps/languages/english.dag -// Scope: Controlled English (CE) formal-subset language model β€” wave-1 structural carriers + wave-2a lex rules and grammar productions for article-led SVO and copula sentence forms. -// Status: T-4.19 (ratified 2026-05-27); wave-1 type carriers + wave-2a lex + grammar + probe; fail-closed on out-of-subset prose. +// Scope: Controlled English (CE) formal-subset language model β€” wave-1 structural carriers + wave-2a lex rules and grammar productions for article-led SVO and copula sentence forms + wave-3 emit-target rows (add slice) through the dissolved 06_translate fold. +// Status: T-4.19 (ratified 2026-05-27); wave-1 type carriers + wave-2a lex + grammar + probe; fail-closed on out-of-subset prose. Wave-3: English is an EMIT target β€” the add slice renders as rigid controlled-English prose, every sentence licensed by the wave-2a grammar. // Anchor: Attempto Controlled English (ACE) grammar β€” http://attempto.ifi.uzh.ch/site/docs/ace_nutshell.html // 🟑 feature:english-wave2-vocabulary β€” scaffold:T-4.19-wave2; dissolve-on: closed vocabulary declared; ^english_token_word catch-all replaced with per-word keyword rules or typed word set. module v4.extdeps.languages.english import v4.extdeps.languages.fidelity { FidelityDisposition } +import v4.std.algebra { Empty, fold_list, list_append, list_snoc_item } +import v4.std.collection { List, Map, empty_map, map_insert } +import v4.std.compilers.target_model { + BoundToken, + ConcreteSyntaxToken, + FixedToken, + TargetModel, + concrete_syntax_token_class, + concrete_syntax_token_to_node, + grammar_relation_field_emitted, + grammar_relation_field_production, + grammar_relation_field_tokens, + target_model_edge_declared_inhabitants, + target_model_edge_selection_policy, + target_model_edge_serialize_source, + target_model_edge_translation_rules +} +import v4.std.node { + Arrow, + Atom, + Conj, + Edge, + Named, + Node, + Positional, + SyntheticOccurrence, + TypeNode +} +import v4.std.text { String } import v4.std.grammar { + FormalGrammarSymbol, FormalProduction, GrammarExpr, GrammarProduction, @@ -25,7 +55,10 @@ import v4.std.grammar { grammar_empty_sync_tokens, grammar_formal_nonterminal, grammar_formal_nonterminal_occurrence, - grammar_formal_terminal + grammar_formal_production, + grammar_formal_terminal, + grammar_relation_tokens_node, + formal_production_to_node } import v4.std.compilers.lexing { CharClassPattern, @@ -204,7 +237,7 @@ fn english_copula_sentence_expr() -> GrammarExpr { ) } -fn english_wave1_grammar() -> ParseGrammar { +fn english_wave1_productions() -> List { let article = GrammarProduction { name: ^english_production_article, expression: english_article_expr(), @@ -228,10 +261,14 @@ fn english_wave1_grammar() -> ParseGrammar { }, emitted: grammar_atom(identity: ^english_surface_sentence) } + [sentence, article, svo, copula] +} + +fn english_wave1_grammar() -> ParseGrammar { ModeledGrammar { root: GrammarRoot { start: ^english_production_sentence, - productions: [sentence, article, svo, copula], + productions: english_wave1_productions(), sync_tokens: grammar_empty_sync_tokens() } } From 6a145fd222977901dd6758490441dbde7c0c8b13 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 12 Jun 2026 23:52:36 +0000 Subject: [PATCH 2/2] =?UTF-8?q?feat(english):=20English=20as=20an=20emit?= =?UTF-8?q?=20target=20=E2=80=94=20add=20slice=20renders=20as=20controlled?= =?UTF-8?q?-English=20prose?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Wave-3 rows in english.dag only: BoundToken relation row + serialize source + binding spellings + TargetModel bundle through the dissolved 06_translate fold. Zero stage edits; zero target_model.dag edits. Every emitted sentence is licensed by the unchanged wave-2a sentence grammar; layout rides binding spellings (T-6 interim, homomorphic with go/rust/python literal-text layout). Emitted (executed witness english_emit_add_prose_holds=true): the add is a function. the add takes the x. the add takes the y. the add returns the sum. the sum adds the x. the sum adds the y. Claim: manual/english_emit_add.dag (prose + grammar-inverse + emit->ingest round trip via tokenize/parse paragraph-of-six-sentences grammar). Also: english_ingest_fail_closed.dag header updated to the live two-regime position per operator steer (fail-closed boundary claims unchanged). Co-Authored-By: Claude Fable 5 --- src/v4/extdeps/languages/english.dag | 402 ++++++++++++++++++ .../boundary/english_ingest_fail_closed.dag | 24 +- src/v4/test/claim/manual/english_emit_add.dag | 284 +++++++++++++ 3 files changed, 699 insertions(+), 11 deletions(-) create mode 100644 src/v4/test/claim/manual/english_emit_add.dag diff --git a/src/v4/extdeps/languages/english.dag b/src/v4/extdeps/languages/english.dag index b41db0de2fe..cf742f59824 100644 --- a/src/v4/extdeps/languages/english.dag +++ b/src/v4/extdeps/languages/english.dag @@ -367,3 +367,405 @@ fn english_ingest_grammar_probe() -> GrammarSchemaProbeBinding { } } } + + +// === Wave-3: English as an EMIT target (add slice) === +// +// The add slice renders as rigid controlled-English prose through the same +// dissolved 06_translate fold every code target uses: data rows only (relation +// row + serialize source + binding spellings + TargetModel bundle), zero stage +// edits. Word choice is deterministic and every emitted sentence is licensed by +// the wave-2a sentence grammar above β€” parseability beats fluency everywhere. +// +// Realization scheme (one licensed sentence form per connective, legalese-rigid): +// fn item -> copula: "the add is a function." +// each param -> SVO: "the add takes the x." / "the add takes the y." +// result -> SVO: "the add returns the sum." +// body + (per operand) -> SVO: "the sum adds the x." / "the sum adds the y." + +// 🟑 gated β€” feature:T-6-token-layout-trivia-policy β€” layout whitespace is baked into +// the BoundToken binding spellings below ("the ", "takes ", ". ") as the interim trivia +// policy, homomorphic with the go/rust/python wave-1 literal-text layout (same T-6 +// dissolve trigger). The wave-2a ingest lex above stays untouched: emitted spaces lex +// back as trivia, keywords/words keep their token classes. +data english_add_fn_source_text: String = "the add is a function. the add takes the x. the add takes the y. the add returns the sum. the sum adds the x. the sum adds the y." + +fn english_named_edge(name: Symbol, target: Node) -> Edge { + Edge { label: Named { name: name }, target: target } +} + +fn english_inhabitant_atom(id: Symbol) -> Node { + Node { + kind: TypeNode { connective: Atom { identity: id } }, + children: [], + occurrence_id: SyntheticOccurrence +} +} + +// Controlled English realizes a typed-term mention as an article-led noun phrase; +// the sole wave-3 declared inhabitant is the common-noun category behind that form. +fn english_noun_facts_node() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + english_named_edge( + name: ^english_facts_field_surface_spelling, + target: english_inhabitant_atom(id: ^english_surface_spelling_noun) + ), + english_named_edge( + name: ^english_facts_field_grammar_category, + target: english_inhabitant_atom(id: ^english_category_formal_noun_phrase) + ) + ], + occurrence_id: SyntheticOccurrence +} +} + +fn english_noun_inhabitant_node() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + english_named_edge( + name: ^english_inhabitant_field_atom, + target: english_inhabitant_atom(id: ^english_inhabitant_noun) + ), + english_named_edge( + name: ^english_inhabitant_field_facts, + target: english_noun_facts_node() + ) + ], + occurrence_id: SyntheticOccurrence +} +} + +fn english_add_fn_emitted_node() -> Node { + Node { + kind: TypeNode { connective: Arrow }, + children: [ + Edge { label: Positional, target: english_noun_inhabitant_node() }, + Edge { label: Positional, target: english_noun_inhabitant_node() }, + Edge { label: Positional, target: english_noun_inhabitant_node() } + ], + occurrence_id: SyntheticOccurrence +} +} + +// 🟑 gated β€” feature:english-per-connective-realization β€” whole-form token row for the +// add slice, mirroring ^python_production_mvp1_fn_add / ^go_production_mvp1_fn_add; +// dissolve-on: value-expression projection rows (target_model value tier) realize the +// fn-item/param/body connectives compositionally and this whole-form row is deleted. +fn english_add_fn_concrete_tokens() -> List { + [ + // "the add is a function." + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_fn_add }, + BoundToken { token_class: ^english_token_copula, binding: ^english_binding_copula_is }, + BoundToken { token_class: ^english_token_indefinite_article, binding: ^english_binding_article_a }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_noun_function }, + BoundToken { token_class: ^english_token_period, binding: ^english_binding_sentence_separator }, + // "the add takes the x." + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_fn_add }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_verb_takes }, + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_param_x }, + BoundToken { token_class: ^english_token_period, binding: ^english_binding_sentence_separator }, + // "the add takes the y." + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_fn_add }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_verb_takes }, + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_param_y }, + BoundToken { token_class: ^english_token_period, binding: ^english_binding_sentence_separator }, + // "the add returns the sum." + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_fn_add }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_verb_returns }, + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_noun_sum }, + BoundToken { token_class: ^english_token_period, binding: ^english_binding_sentence_separator }, + // "the sum adds the x." + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_noun_sum_subject }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_verb_adds }, + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_param_x }, + BoundToken { token_class: ^english_token_period, binding: ^english_binding_sentence_separator }, + // "the sum adds the y." + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_noun_sum_subject }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_verb_adds }, + BoundToken { token_class: ^english_token_definite_article, binding: ^english_binding_article_the }, + BoundToken { token_class: ^english_token_word, binding: ^english_binding_param_y }, + FixedToken { token_class: ^english_token_period } + ] +} + +// Deterministic word choice: one spelling per binding, zero synonym variation. +// Trailing layout rides the spelling (T-6 interim, see mark above); object nouns in +// sentence-final position carry none, the medial sentence separator carries ". ". +fn english_add_fn_binding_spellings() -> Map { + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + map_insert(empty_map(), ^english_binding_article_the, "the "), + ^english_binding_article_a, + "a " + ), + ^english_binding_copula_is, + "is " + ), + ^english_binding_fn_add, + "add " + ), + ^english_binding_noun_function, + "function" + ), + ^english_binding_verb_takes, + "takes " + ), + ^english_binding_param_x, + "x" + ), + ^english_binding_param_y, + "y" + ), + ^english_binding_verb_returns, + "returns " + ), + ^english_binding_noun_sum, + "sum" + ), + ^english_binding_noun_sum_subject, + "sum " + ), + ^english_binding_verb_adds, + "adds " + ), + ^english_binding_sentence_separator, + ". " + ) +} + +fn english_concrete_token_node(token: ConcreteSyntaxToken) -> Node { + // T-11: serialize through the single shared morphism (no parallel wire authority). + concrete_syntax_token_to_node(token: token) +} + +fn english_add_fn_formal_rhs() -> List { + fold_list( + xs: english_add_fn_concrete_tokens(), + empty: Empty, + cons: fn(acc, token) { + list_snoc_item( + xs: acc, + item: grammar_formal_terminal(identity: concrete_syntax_token_class(token: token)) + ) + } + ) +} + +fn english_add_fn_formal_production() -> FormalProduction { + grammar_formal_production( + lhs: ^english_production_add_fn_paragraph, + rhs: english_add_fn_formal_rhs() + ) +} + +// 🟒 grounded. +type EnglishGrammarRelationRow { + production: FormalProduction + emitted: Node + tokens: List +} + +fn english_add_fn_relation_row() -> EnglishGrammarRelationRow { + EnglishGrammarRelationRow { + production: english_add_fn_formal_production(), + emitted: english_add_fn_emitted_node(), + tokens: english_add_fn_concrete_tokens() + } +} + +fn english_grammar_relation_row_node(row: EnglishGrammarRelationRow) -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + english_named_edge( + name: grammar_relation_field_production, + target: formal_production_to_node(production: row.production) + ), + english_named_edge(name: grammar_relation_field_emitted, target: row.emitted), + english_named_edge( + name: grammar_relation_field_tokens, + target: grammar_relation_tokens_node( + tokens: row.tokens, + token_to_node: english_concrete_token_node + ) + ) + ], + occurrence_id: SyntheticOccurrence +} +} + +fn english_add_fn_translation_rules_node() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + english_named_edge( + name: ^english_relation_rule_add_fn, + target: english_grammar_relation_row_node(row: english_add_fn_relation_row()) + ) + ], + occurrence_id: SyntheticOccurrence +} +} + +fn english_add_fn_serialize_source_node() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + english_named_edge( + name: ^serialize_source_field_source_text, + target: english_inhabitant_atom(id: ^english_add_fn_source_literal) + ), + english_named_edge( + name: ^serialize_source_field_source_grammar, + target: english_inhabitant_atom(id: ^english_production_add_fn_paragraph) + ), + english_named_edge( + name: grammar_relation_field_tokens, + target: grammar_relation_tokens_node( + tokens: english_add_fn_concrete_tokens(), + token_to_node: english_concrete_token_node + ) + ) + ], + occurrence_id: SyntheticOccurrence +} +} + +// Zip-fold support nodes derived from the noun inhabitant constructors β€” not parallel fixture data. +// 🟑 gated β€” feature:W-T-10-mvp1-exact-zip-closure β€” bind gunbc#4760 β€” dissolve-on: find_witness enumerates inside declared_inhabitants without fixture zip-fold support edges. +fn english_add_fn_zip_fold_closure_edges() -> List { + [ + english_named_edge( + name: ^english_inhabitant_field_add_fn, + target: english_add_fn_emitted_node() + ), + english_named_edge( + name: ^english_coercion_field_noun_inhabitant_atom, + target: english_inhabitant_atom(id: ^english_inhabitant_noun) + ), + english_named_edge( + name: ^english_coercion_field_noun_facts, + target: english_noun_facts_node() + ), + english_named_edge( + name: ^english_coercion_field_noun_spelling, + target: english_inhabitant_atom(id: ^english_surface_spelling_noun) + ), + english_named_edge( + name: ^english_coercion_field_noun_category, + target: english_inhabitant_atom(id: ^english_category_formal_noun_phrase) + ) + ] +} + +fn english_declared_inhabitants_root() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: list_append( + left: [ + english_named_edge( + name: ^english_inhabitant_field_noun, + target: english_noun_inhabitant_node() + ) + ], + right: english_add_fn_zip_fold_closure_edges() + ), + occurrence_id: SyntheticOccurrence +} +} + +fn english_selection_policy_node() -> Node { + english_noun_inhabitant_node() +} + +fn english_add_fn_target_model_node() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + english_named_edge(name: target_model_edge_selection_policy, target: english_selection_policy_node()), + english_named_edge(name: target_model_edge_declared_inhabitants, target: english_declared_inhabitants_root()), + english_named_edge(name: target_model_edge_translation_rules, target: english_add_fn_translation_rules_node()), + english_named_edge(name: target_model_edge_serialize_source, target: english_add_fn_serialize_source_node()) + ], + occurrence_id: SyntheticOccurrence +} +} + +fn english_add_fn_target_model() -> TargetModel { + TargetModel { + bundle: english_add_fn_target_model_node(), + lex: english_wave1_lex(), + binding_spellings: english_add_fn_binding_spellings(), + authority_source_text: english_add_fn_source_text + } +} + +fn english_sentence_nonterminal() -> GrammarExpr { + Nonterminal { production: ^english_production_sentence } +} + +// Round-trip ingest grammar for the emitted add prose: a paragraph of exactly six +// sentences, each licensed by the UNCHANGED wave-2a sentence productions above. The +// sentence grammar stays the licensing authority; this production only fixes arity. +fn english_add_fn_paragraph_expr() -> GrammarExpr { + Sequence { + left: english_sentence_nonterminal(), + right: Sequence { + left: english_sentence_nonterminal(), + right: Sequence { + left: english_sentence_nonterminal(), + right: Sequence { + left: english_sentence_nonterminal(), + right: Sequence { + left: english_sentence_nonterminal(), + right: english_sentence_nonterminal() + } + } + } + } + } +} + +fn english_add_fn_paragraph_production() -> GrammarProduction { + GrammarProduction { + name: ^english_production_add_fn_paragraph, + expression: english_add_fn_paragraph_expr(), + emitted: english_add_fn_emitted_node() + } +} + +fn english_add_fn_paragraph_grammar() -> ParseGrammar { + ModeledGrammar { + root: GrammarRoot { + start: ^english_production_add_fn_paragraph, + productions: list_append( + left: [english_add_fn_paragraph_production()], + right: english_wave1_productions() + ), + sync_tokens: grammar_empty_sync_tokens() + } + } +} diff --git a/src/v4/test/claim/boundary/english_ingest_fail_closed.dag b/src/v4/test/claim/boundary/english_ingest_fail_closed.dag index d0d6eb88ed4..ade0007384e 100644 --- a/src/v4/test/claim/boundary/english_ingest_fail_closed.dag +++ b/src/v4/test/claim/boundary/english_ingest_fail_closed.dag @@ -1,16 +1,18 @@ // src/v4/test/claim/boundary/english_ingest_fail_closed.dag // -// Scope: TestClaim β€” the English boundary-honesty probe (T-4.11). English -// is NOT a language model (natural language has no formal grammar -// β€” ratified fork). It is a boundary-honesty probe with -// two demonstrable wins: -// (a) Shape B emit: a `.dag` program walking typed values β†’ -// English prose (this is the existing T-16 Markdown/docs -// artifact; no new substrate). -// (b) the honest win: pointing `ingest` at arbitrary English -// prose produces a PRECISE Diagnostic β€” never a fabricated -// parse. This is the no-engine / no-fallback thesis made -// visible: the architecture refusing to lie IS the result. +// Scope: TestClaim β€” the English boundary-honesty probe. English is two +// regimes: +// (a) arbitrary natural English has no formal grammar and is NOT +// a language model β€” pointing `ingest` at it produces a +// PRECISE Diagnostic, never a fabricated parse (this probe; +// the no-engine / no-fallback thesis made visible). +// (b) the rigid Controlled-English subset (T-4.19, +// extdeps/languages/english.dag: article-led SVO and copula +// sentence forms) IS a modeled language and an emit target; +// its prose lexes, parses, and round-trips through the +// shared pipeline like any other target. +// The fail-closed boundary in this file guards regime (a) only; +// regime (b) is claimed by manual/english_emit_add.dag. // Anchor: THESIS no-fallback + C5 (ingest = emit⁻¹ on the lossless core; // outside it β‡’ fail-closed Diagnostic) + feedback_no_engine // Prerequisites (sequencing β€” NOT parallel to an unfilled verification diff --git a/src/v4/test/claim/manual/english_emit_add.dag b/src/v4/test/claim/manual/english_emit_add.dag new file mode 100644 index 00000000000..4a64cea847b --- /dev/null +++ b/src/v4/test/claim/manual/english_emit_add.dag @@ -0,0 +1,284 @@ +// src/v4/test/claim/manual/english_emit_add.dag +// Scope: English emit-target receipt β€” emit(add) renders the canonical controlled-English +// prose through the dissolved 06_translate fold, and the prose round-trips: tokenize with +// the UNCHANGED wave-2a English lex, parse as a six-sentence paragraph whose sentences are +// the UNCHANGED wave-2a sentence productions, and recover the emitted node (structural +// identity). Mirrors mvp1_python_add_translate.dag (emit path) + mvp1_dag_add_round_trip.dag +// (round-trip shape); the ingest direction here is the text-level tokenize+parse path. +// Anchor: Β§3 emit-breadth MoA β€” a new target is data rows through the same fold; operator +// design steer β€” rigid legalese grammar, round-trip is the acceptance. + +module v4.test.claim.manual.english_emit_add + +import v4.compiler.emit { emit } +import v4.compiler.infer { InferredFacts, InferredTree } +import v4.compiler.parse { grammar_production_identity_node_projection, parse } +import v4.compiler.target_carriers { TargetSource } +import v4.compiler.tokenize { tokenize } +import v4.compiler.translate { + grammar_inverse_source_validated, + target_serialize_source_from_model +} +import v4.extdeps.languages.english { + english_add_fn_emitted_node, + english_add_fn_paragraph_grammar, + english_add_fn_source_text, + english_add_fn_target_model, + english_inhabitant_atom, + english_noun_facts_node, + english_noun_inhabitant_node, + english_wave1_lex +} +import v4.test.claim.lens_common.infer_fixture { claim_inferred_facts_witness } +import v4.std.algebra { fold_list } +import v4.std.cardinality { termination_proof_witness_for_node } +import v4.std.collection { Map } +import v4.std.constraints { + CanonicalGrounding, + CanonicalGroundingWitness +} +import v4.std.diagnostic { + Accepted, + Diagnostic, + ExternalContractUnknown, + None, + Outcome, + Rejected, + Unavailable, + node_locus +} +import v4.std.grammar { ParseTree } +import v4.std.logic { Bool } +import v4.std.node { Edge, Named, Node, Positional } +import v4.std.compilers.target_model { TargetModel } +import v4.std.verification { + BoolWitness, + BoolWitnessClaim, + UnifiedTestClaim +} +import v4.std.witness { Holds, StructuralPropertyWitness, Violates, Witness } + +data english_emit_add_emitted_root: Node = english_add_fn_emitted_node() + +data english_emit_add_target_model: TargetModel = english_add_fn_target_model() + +data english_emit_add_noun_inhabitant: Node = english_noun_inhabitant_node() + +data english_emit_add_noun_facts_node: Node = english_noun_facts_node() + +fn english_emit_add_canonical_grounding( + node: Node, + algebra: Node +) -> CanonicalGrounding { + CanonicalGrounding { + node: node, + witness: CanonicalGroundingWitness { + structural: StructuralPropertyWitness { + property: ^constraint_property_being_canonical, + evidence: algebra + }, + closedness: StructuralPropertyWitness { + property: ^constraint_property_candidate_set_closedness, + evidence: node + } + } + } +} + +// 🟑 gated β€” feature:W-T-10-mvp1-inferred-tree-grounding β€” bind gunbc#4760 β€” dissolve-on: infer-authored facts replace hand-enumerated MVP fixture grounding. +fn english_emit_add_canonical_grounding_for(node: Node) -> Witness { + if node == english_emit_add_emitted_root { + Holds { + value: english_emit_add_canonical_grounding( + node: node, + algebra: node + ) + } + } else if node == english_emit_add_noun_inhabitant { + Holds { + value: english_emit_add_canonical_grounding( + node: node, + algebra: english_emit_add_noun_facts_node + ) + } + } else if node == english_inhabitant_atom(id: ^english_inhabitant_noun) { + Holds { + value: english_emit_add_canonical_grounding( + node: node, + algebra: english_emit_add_noun_inhabitant + ) + } + } else if node == english_emit_add_noun_facts_node { + Holds { + value: english_emit_add_canonical_grounding( + node: node, + algebra: node + ) + } + } else if node == english_inhabitant_atom(id: ^english_surface_spelling_noun) { + Holds { + value: english_emit_add_canonical_grounding( + node: node, + algebra: english_emit_add_noun_facts_node + ) + } + } else if node == english_inhabitant_atom(id: ^english_category_formal_noun_phrase) { + Holds { + value: english_emit_add_canonical_grounding( + node: node, + algebra: english_emit_add_noun_facts_node + ) + } + } else { + Violates { + diagnostic: Diagnostic { + reason: ^english_emit_add_grounding_miss, + at: node_locus(node: node), + correction: Unavailable { reason: ExternalContractUnknown } + } + } + } +} + +fn english_emit_add_inferred_facts_for(node: Node) -> Witness { + match english_emit_add_canonical_grounding_for(node: node) { + Violates { diagnostic: d } => Violates { diagnostic: d } + Holds { value: grounding } => + match termination_proof_witness_for_node(n: node) { + Violates { diagnostic: d } => Violates { diagnostic: d } + Holds { value: proof } => + Holds { + value: claim_inferred_facts_witness( + grounding: grounding, + descent: Holds { value: proof } + ) + } + } + } +} + +fn english_emit_add_facts_lookup(key: Node) -> Witness { + english_emit_add_inferred_facts_for(node: key) +} + +data english_emit_add_inferred_tree: InferredTree = InferredTree { + root: english_emit_add_emitted_root, + facts: Map { + lookup: english_emit_add_facts_lookup + } +} + +fn anchor_english_emit_add_accepts() -> Outcome { + emit(tree: english_emit_add_inferred_tree, target: english_emit_add_target_model) +} + +data english_emit_add_receipt: Outcome = anchor_english_emit_add_accepts() + +// Execution witness β€” emit(add) must produce the canonical controlled-English prose. +fn english_emit_add_prose_holds() -> Bool { + match english_emit_add_receipt { + Accepted { value: source, diagnostics: d } => + (source == english_add_fn_source_text) && (d == None) + Rejected { diagnostics: _ } => false + } +} + +// emit(add) must match the grammar-inverse serialize (shared 06_translate path). +fn english_emit_add_matches_serialize_holds() -> Bool { + match target_serialize_source_from_model( + target: english_emit_add_target_model, + emitted: english_emit_add_emitted_root + ) { + Accepted { value: authority, diagnostics: ad } => + match english_emit_add_receipt { + Accepted { value: source, diagnostics: d } => + (source == authority) && (d == None) && (ad == None) + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +fn english_emit_add_grammar_inverse_holds() -> Bool { + match grammar_inverse_source_validated( + target: english_emit_add_target_model, + emitted: english_emit_add_emitted_root + ) { + Accepted { value: _, diagnostics: d } => d == None + Rejected { diagnostics: _ } => false + } +} + +// Ingest direction: tokenize the EMITTED prose with the unchanged wave-2a English lex, +// parse as the six-sentence paragraph (sentences = unchanged wave-2a productions). +fn english_emit_add_ingest_parse(source: TargetSource) -> Outcome { + match tokenize( + text: source, + file: ^english_emit_add_round_trip_fixture_file, + rules: english_wave1_lex() + ) { + Rejected { diagnostics: diags } => Rejected { diagnostics: diags } + Accepted { value: tokens, diagnostics: _ } => + parse(tokens: tokens, grammar: english_add_fn_paragraph_grammar()) + } +} + +// The parse wraps the matched production's emitted node under the production-identity +// projection edge; structural identity holds when that node is the emitted add-fn root. +fn english_emit_add_identity_edge_matches(e: Edge, expected: Node) -> Bool { + match e.label { + Named { name: n } => + (n == grammar_production_identity_node_projection) && (e.target == expected) + Positional => false + } +} + +fn english_emit_add_parse_identity_matches(root: Node, expected: Node) -> Bool { + fold_list( + xs: root.children, + empty: false, + cons: fn(acc, e) { + acc || english_emit_add_identity_edge_matches(e: e, expected: expected) + } + ) +} + +// Round trip: emit(add) -> tokenize -> parse -> recovered node == emitted root. +fn english_emit_add_ingest_round_trip_holds() -> Bool { + match english_emit_add_receipt { + Rejected { diagnostics: _ } => false + Accepted { value: source, diagnostics: _ } => + match english_emit_add_ingest_parse(source: source) { + Accepted { value: tree, diagnostics: d } => + english_emit_add_parse_identity_matches( + root: tree, + expected: english_emit_add_emitted_root + ) && (d == None) + Rejected { diagnostics: _ } => false + } + } +} + +// Combined acceptance: exact licensed prose + grammar-inverse + emit->ingest identity. +fn english_emit_add_emit_ingest_round_trip_holds() -> Bool { + english_emit_add_prose_holds() + && english_emit_add_matches_serialize_holds() + && english_emit_add_grammar_inverse_holds() + && english_emit_add_ingest_round_trip_holds() +} + +// Consolidation #4553 Phase 2 distributed BoolWitnessClaim markers. +// Co-located with the witnesses so glob discovery finds them without the central roster. +data unified_claim_english_emit_add_prose: UnifiedTestClaim = BoolWitnessClaim { + witness: BoolWitness { + entry: "src/v4/test/claim/manual/english_emit_add.dag", + function: english_emit_add_prose_holds + } +} + +data unified_claim_english_emit_add_round_trip: UnifiedTestClaim = BoolWitnessClaim { + witness: BoolWitness { + entry: "src/v4/test/claim/manual/english_emit_add.dag", + function: english_emit_add_emit_ingest_round_trip_holds + } +}