docs(survey): v2 architecture + ultracode completion plan, with evidence

docs/reports/2026-11-04-v2-survey/evidence/README.adoc

@@ -0,0 +1,53 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Evidence for the 2026-11-04 v2 survey
+
+These files back the findings in `../EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc`. They are deliberately *outside* `formal/_CoqProject` and the Cargo workspace, so they change no build.
+
+== Coq witnesses
+
+`SurveyCounterexamples.v` is checked against the current `formal/` build:
+
+[source,sh]
+----
+cd formal
+coq_makefile -f _CoqProject -o Makefile.coq && make -f Makefile.coq -j4
+coqc -R . Ephapax ../docs/reports/2026-11-04-v2-survey/evidence/SurveyCounterexamples.v
+----
+
+Expected `Print Assumptions` output with coqc 8.18.0. This was first checked at `800030f`, then re-checked after `main` (including #418) was merged into the branch at `10339b3`, with identical results:
+
+[cols="2,3",options="header"]
+|===
+|Lemma |Assumptions
+|`legacy_inconsistent` |axiom `Semantics.preservation` (legacy, `Admitted` by directive)
+|`env_inconsistent_preservation_l1` |axiom `preservation_l1` (the `Admitted.` lemma)
+|`env_inconsistent_step_pop` |axiom `step_pop_disjoint_from_type_l1` (the `Admitted.` lemma)
+|`preservation_l1_FALSE_closed` |Closed under the global context
+|`preservation_l1_FALSE_echo_crosspath` |Closed under the global context
+|`observe_stuck` |Closed under the global context
+|`pair_dup_linear_string` |Closed under the global context
+|`echo_copyable_linear_mode` |Closed under the global context
+|===
+
+NOTE: These results describe `main` before the D0/D0b retirement in hyperpolymath/ephapax#422 (owner-ratified 2026-11-05). After #422 merges, the three refuted statements are `Prop` definitions rather than `Admitted` lemmas. `legacy_inconsistent`, `env_inconsistent_preservation_l1` and `env_inconsistent_step_pop` then fail to compile, which is the intended result: the environment no longer derives `False`. The other five lemmas compile unchanged on top of #422 and stay "Closed under the global context" (checked with coqc 8.18.0 after removing F0/F1); P2 moves them into `formal/regress/`.
+
+The first three rows mean the global environment can derive `False`. The L1 pair needs the P0 retirement in the plan. The legacy row needs decision D0b in the plan, because the legacy theorem is fenced. Both are owner decisions. The `Admitted.` must not be closed, and no side-condition may be added.
+
+== Rust checker probes
+
+`probes/*.eph.txt` (stored with a `.txt` suffix so the repo-wide `eph_corpus_gate` ignores them; copy to `.eph` to re-run) were run with `target/debug/ephapax check` from a `cargo build --workspace` of the same commit. The table below records each exit code and the last output line. For dup2, dup4, pairdup and lamcap, exit 0 is a *soundness hole*, because each one reuses a linear value. For rec1, exit 134 is a crash.
+
+[cols="1,1,4",options="header"]
+|===
+|Probe |`check` exit |Last output line
+|`dup2` |0 |✓ 1 file(s) checked successfully
+|`dup4` |0 |✓ 1 file(s) checked successfully
+|`pairdup` |0 |✓ 1 file(s) checked successfully
+|`lamcap` |0 |✓ 1 file(s) checked successfully
+|`rec1` |134 |fatal runtime error: stack overflow, aborting
+|`i64` |0 |✓ 1 file(s) checked successfully
+|`perform` |0 |✓ 1 file(s) checked successfully
+|`g5` |0 |✓ 1 file(s) checked successfully
+|`gen_angle` |1 |Error: 1 file(s) checked, 1 error(s)
+|===

docs/reports/2026-11-04-v2-survey/evidence/SurveyCounterexamples.v

@@ -0,0 +1,185 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
+(** * Survey evidence, 2026-11-04 — NOT part of formal/_CoqProject.
+
+    Re-checkable witnesses for the findings in
+    docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc.
+    Apart from F0, every lemma here is against the CURRENT v2 judgment
+    ([has_type_l1], [step]). F0 is the single exception: it *uses* the
+    legacy [Semantics.preservation] (Admitted by owner directive) together
+    with [Counterexample.v] to witness the legacy inconsistency. Nothing
+    here closes, edits or extends the legacy theorem or Semantics.v.
+
+    Check (from repo root, after building formal/):
+      cd formal && coq_makefile -f _CoqProject -o Makefile.coq \
+        && make -f Makefile.coq -j4 \
+        && coqc -R . Ephapax ../docs/reports/2026-11-04-v2-survey/evidence/SurveyCounterexamples.v
+*)
+
+From Ephapax Require Import Syntax Typing TypingL1 Semantics Semantics_L1
+  Modality Counterexample Counterexample_PreservationL1 Counterexample_StepPop.
+Require Import Coq.Lists.List Coq.Strings.String. Import ListNotations.
+Open Scope string_scope.
+
+(** ** F0. The legacy [Semantics.preservation] is [Admitted] (kept by
+    owner directive) and refuted by [Counterexample.v], so loading both
+    also derives [False]. This does not ask for the legacy theorem to
+    be closed or edited. It records that it must never appear in a
+    headline theorem's assumptions. *)
+Lemma legacy_inconsistent : False.
+Proof.
+  destruct (Semantics.preservation _ _ _ _ _ _ (Counterexample.bad_step nil)
+              _ _ _ Counterexample.bad_typable) as [G_out H].
+  exact (Counterexample.bad_post_untypable _ _ H).
+Qed.
+
+(** ** F1. The global environment is inconsistent.
+    [preservation_l1] and [step_pop_disjoint_from_type_l1] are
+    [Admitted] (hence axioms) and are refuted by Qed, axiom-free
+    files that are built in the same project. *)
+Lemma env_inconsistent_preservation_l1 : False.
+Proof. exact (preservation_l1_FALSE preservation_l1). Qed.
+
+Lemma env_inconsistent_step_pop : False.
+Proof. exact (step_pop_disjoint_from_type_l1_FALSE step_pop_disjoint_from_type_l1). Qed.
+
+(** ** F2. preservation_l1 is false with a closed context ([G = []]).
+    An un-entered same-name [ERegion] exits immediately and pops the
+    ambient occurrence of [rv] that the sibling [ELoc 0 rv] needs. *)
+Definition rv : region_name := "rv".
+
+Definition closed_pre : expr :=
+  EStringConcat (ELoc 0 rv) (EFst (EPair (ELoc 1 rv) (ERegion rv (EI32 0)))).
+Definition closed_post : expr :=
+  EStringConcat (ELoc 0 rv) (EFst (EPair (ELoc 1 rv) (EI32 0))).
+
+Lemma closed_pre_typed :
+  has_type_l1 Linear [rv] [] closed_pre (TString rv) [] [].
+Proof.
+  unfold closed_pre.
+  eapply T_StringConcat_L1.
+  - apply T_Loc_L1. simpl; auto.
+  - apply (T_Fst_L1 Linear [rv] [] [] [] _ (TString rv) (TBase TI32)); [| reflexivity].
+    eapply T_Pair_L1.
+    + apply T_Loc_L1. simpl; auto.
+    + change (@nil region_name) with (remove_first_L1 rv [rv]).
+      eapply T_Region_Active_L1.
+      * simpl; auto.
+      * simpl; intros [].
+      * simpl; auto.
+      * apply T_I32_L1.
+Qed.
+
+Lemma closed_step :
+  step ([], [rv], closed_pre) ([], [], closed_post).
+Proof.
+  unfold closed_pre, closed_post.
+  apply S_StringConcat_Step2; [constructor |].
+  apply S_Fst_Step.
+  apply S_Pair_Step2; [constructor |].
+  change (@nil region_name) with (remove_first rv [rv]).
+  change (@nil mem_cell) with (mem_free_region [] rv).
+  apply S_Region_Exit; [constructor | simpl; auto | simpl; auto].
+Qed.
+
+Lemma closed_post_untypable :
+  forall T Rf G', ~ has_type_l1 Linear [] [] closed_post T Rf G'.
+Proof.
+  intros T Rf G' H. unfold closed_post in H.
+  inversion H; subst.
+  match goal with
+  | Hl : has_type_l1 _ [] [] (ELoc 0 rv) _ _ _ |- _ => inversion Hl; subst
+  end.
+  match goal with Hin : In _ [] |- _ => inversion Hin end.
+Qed.
+
+Theorem preservation_l1_FALSE_closed :
+  ~ (forall m mu R e mu' R' e',
+       step (mu, R, e) (mu', R', e') ->
+       forall G T R_final G',
+         has_type_l1 m R G e T R_final G' ->
+         has_type_l1 m R' G e' T R_final G').
+Proof.
+  intro Hp.
+  eapply closed_post_untypable.
+  eapply (Hp Linear [] [rv] closed_pre [] [] closed_post closed_step);
+    exact closed_pre_typed.
+Qed.
+
+(** ** F3. preservation_l1 is false for a reason unrelated to regions:
+    [S_Drop] and [S_Drop_Echo] both fire on the same term, so [step]
+    is nondeterministic, and the echo path leaves a [T_Drop_L1]
+    derivation untypable. *)
+Lemma drop_typed :
+  has_type_l1 Linear [rv] [] (EDrop (ELoc 0 rv)) (TBase TUnit) [rv] [].
+Proof. apply (T_Drop_L1 Linear [rv] [rv] [] [] (ELoc 0 rv) (TString rv)); [reflexivity | apply T_Loc_L1; simpl; auto]. Qed.
+
+Lemma drop_echo_step :
+  step ([], [rv], EDrop (ELoc 0 rv)) ([], [rv], EEcho (TString rv) (ELoc 0 rv)).
+Proof.
+  change (@nil mem_cell) with (mem_write [] 0 CFree) at 2.
+  apply S_Drop_Echo.
+Qed.
+
+Lemma echo_not_unit :
+  forall R G Rf G' T, ~ has_type_l1 Linear R G (EEcho T (ELoc 0 rv)) (TBase TUnit) Rf G'.
+Proof. intros R G Rf G' T H. inversion H. Qed.
+
+Theorem preservation_l1_FALSE_echo_crosspath :
+  ~ (forall m mu R e mu' R' e',
+       step (mu, R, e) (mu', R', e') ->
+       forall G T R_final G',
+         has_type_l1 m R G e T R_final G' ->
+         has_type_l1 m R' G e' T R_final G').
+Proof.
+  intro Hp.
+  eapply echo_not_unit.
+  eapply (Hp Linear [] [rv] _ [] [rv] _ drop_echo_step); exact drop_typed.
+Qed.
+
+(** ** F4. progress fails: [EObserve] has a typing rule but no step rule. *)
+Lemma observe_typed :
+  has_type_l1 Linear [] [] (EObserve (EEcho (TBase TUnit) EUnit)) (TBase TUnit) [] [].
+Proof. apply (T_Observe_L1 Linear [] [] [] [] _ (TBase TUnit)). apply T_Echo_L1; [constructor | apply T_Unit_L1]. Qed.
+
+Lemma observe_not_value : ~ is_value (EObserve (EEcho (TBase TUnit) EUnit)).
+Proof. intro H; inversion H. Qed.
+
+Lemma observe_stuck :
+  forall mu c', ~ step (mu, [], EObserve (EEcho (TBase TUnit) EUnit)) c'.
+Proof. intros mu c' H. inversion H. Qed.
+
+(** ** F5. Compound linearity hole: a pair variable whose first
+    component is a linear [TString] is treated as unrestricted
+    ([is_linear_ty (TProd _ _) = false]), so Linear mode duplicates
+    the string. *)
+Lemma pair_dup_linear_string : forall r,
+  has_type_l1 Linear [r] [(TProd (TString r) (TBase TI32), false)]
+    (EPair (EFst (EVar 0)) (EFst (EVar 0)))
+    (TProd (TString r) (TString r)) [r] [(TProd (TString r) (TBase TI32), false)].
+Proof.
+  intros r. eapply T_Pair_L1;
+  (eapply T_Fst_L1; [eapply T_Var_Unr_L1; reflexivity | reflexivity]).
+Qed.
+
+(** ** F6. A drop-echo residue of a linear String can be copied in
+    Linear mode ([is_linear_ty (TEcho _) = false]). *)
+Lemma echo_copyable_linear_mode :
+  forall l r R G, In r R ->
+  has_type_l1 Linear R G (ECopy (EEcho (TString r) (ELoc l r)))
+              (TProd (TEcho (TString r)) (TEcho (TString r))) R G.
+Proof.
+  intros l r R G Hin. apply T_Copy_L1; [reflexivity|].
+  apply T_Echo_L1; [constructor | now apply T_Loc_L1].
+Qed.
+
+(** Assumption audit. Expected: F0/F1 lemmas list the refuted axiom;
+    every other lemma is "Closed under the global context". *)
+Print Assumptions legacy_inconsistent.
+Print Assumptions env_inconsistent_preservation_l1.
+Print Assumptions env_inconsistent_step_pop.
+Print Assumptions preservation_l1_FALSE_closed.
+Print Assumptions preservation_l1_FALSE_echo_crosspath.
+Print Assumptions observe_stuck.
+Print Assumptions pair_dup_linear_string.
+Print Assumptions echo_copyable_linear_mode.

docs/reports/2026-11-04-v2-survey/evidence/probes/dup2.eph.txt

@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: MPL-2.0
+// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it.
+fn main(): I32 =
+  let! x = 5
+  let a = x
+  let b = x
+  a + b

docs/reports/2026-11-04-v2-survey/evidence/probes/dup4.eph.txt

@@ -0,0 +1,5 @@
+// SPDX-License-Identifier: MPL-2.0
+// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it.
+fn use2(x: I32, y: I32): I32 = x + y
+fn main(): I32 =
+  let! x = 5 in use2(x, x)

docs/reports/2026-11-04-v2-survey/evidence/probes/g5.eph.txt

@@ -0,0 +1,4 @@
+// SPDX-License-Identifier: MPL-2.0
+// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it.
+fn t(): I64 =
+  __ffi("foo", 1)

docs/reports/2026-11-04-v2-survey/evidence/probes/gen_angle.eph.txt

@@ -0,0 +1,4 @@
+// SPDX-License-Identifier: MPL-2.0
+// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it.
+fn id<a>(x: a): a = x
+fn main(): I32 = id(3)

docs/reports/2026-11-04-v2-survey/evidence/probes/i64.eph.txt

@@ -0,0 +1,4 @@
+// SPDX-License-Identifier: MPL-2.0
+// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it.
+fn f(x: I64): I64 = x + x
+fn main(): I32 = 0

docs/reports/2026-11-04-v2-survey/evidence/probes/lamcap.eph.txt

@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: MPL-2.0
+// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it.
+fn main(): I32 =
+  region r {
+    let! s = String.new@r("hi") in
+    let f = fn(u: ()) -> s in
+    let a = f(()) in
+    let b = f(()) in
+    drop(a);
+    drop(b);
+    0
+  }

docs/reports/2026-11-04-v2-survey/evidence/probes/pairdup.eph.txt

@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: MPL-2.0
+// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it.
+fn main(): I32 =
+  region r {
+    let! s = String.new@r("hi") in
+    let p = (s, 1) in
+    let a = fst(p) in
+    let b = fst(p) in
+    drop(a);
+    drop(b);
+    0
+  }

docs/reports/2026-11-04-v2-survey/evidence/probes/perform.eph.txt

@@ -0,0 +1,7 @@
+// SPDX-License-Identifier: MPL-2.0
+// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it.
+fn main(): I32 =
+  handle perform ask() with
+  | return(x) => x
+  | ask(resume) => 42
+  end

docs/reports/2026-11-04-v2-survey/evidence/probes/rec1.eph.txt

@@ -0,0 +1,5 @@
+// SPDX-License-Identifier: MPL-2.0
+// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it.
+data L = Nil | Cons(I32, L)
+fn f(l: L): I32 = 0
+fn main(): I32 = 0