From 0716aec7462fc4da6bc7e42edc20d2d57b11fbfe Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 27 Apr 2026 12:39:33 +0100
Subject: [PATCH 1/3] proof(formal): close 1 of 2 preservation admits + 2
 reusable region lemmas
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

**Build unblock (pre-existing duplicate-merge-artifacts on main):**
- Typing.v L43-59: remove duplicate Fixpoint free_regions (added by
  squash-rebuild 68cdb41b vs PR #29 merge dbf4bdd0 within same day)
- Semantics.v L2092-2095, L2377-2380: remove duplicate T_Region_Active
  proof branches using stale 2-arg constructor form

**New structural lemmas:**
- region_membership_eq_preserves_typing: typing depends on R only via
  In-membership, so any R'/R agreeing on In transports a derivation
- region_extension_preserves_typing_when_free: symmetric counterpart
  to existing region_shrink_preserves_typing — adding r to R preserves
  typing of expressions free of r

**L3009 closed (Qed):** region_shrink_preserves_typing T_Region_Active
shadowing case (r = r0). Discharge via case-split on
in_dec String.string_dec r (remove_first r R):
- multiplicity > 1: T_Region_Active + membership-eq transport
- multiplicity = 1: T_Region (re-binds r) + membership-eq transport

**L3118 still open** (preservation S_Region_Step + T_Region_Active
Case B). Investigation revealed the originally-sketched step-induction
shape doesn't carry through recursive _Step rules; requires either a
typing-derivation-wide r-freedom invariant or a strengthened
preservation theorem. Documented at
.desktop-tools/inbox/ephapax_l3118_region_extension_proof_opportunity.md
with revised difficulty (2-4h focused metatheory, not the original
1.5-2h estimate).

Admit count: 2 → 1.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 formal/Semantics.v | 205 ++++++++++++++++++++++++++++++++++++++++++---
 formal/Typing.v    |  17 ----
 2 files changed, 192 insertions(+), 30 deletions(-)

diff --git a/formal/Semantics.v b/formal/Semantics.v
index 1e998840..a52ee748 100644
--- a/formal/Semantics.v
+++ b/formal/Semantics.v
@@ -2089,11 +2089,6 @@ Proof.
     eexists. split; [eapply T_Region_Active; [assumption | assumption | exact Ht]|].
     split; [assumption | split; [assumption | exact Hc]].
 
-  (* T_Region_Active: same structure, uses T_Region_Active in conclusion *)
-  - destruct (IHHtype G2 Hagree Hfp) as [G2' [Ht [Ha [Hf Hc]]]].
-    eexists. split; [eapply T_Region_Active; [assumption | exact Ht]|].
-    split; [assumption | split; [assumption | exact Hc]].
-
   (* T_Borrow: G'=G *)
   - assert (Hlk2: ctx_lookup G2 i = Some (T, false)) by (apply Hfp; assumption).
     eexists. split; [econstructor; exact Hlk2|].
@@ -2379,11 +2374,6 @@ Proof.
     + assumption.
     + apply IHHtype. assumption.
 
-  (* T_Region_Active *)
-  - eapply T_Region_Active.
-    + assumption.
-    + apply IHHtype. assumption.
-
   (* T_Borrow *)
   - destruct (Nat.leb_spec k i).
     + replace (i + 1) with (S i) by lia.
@@ -2956,6 +2946,162 @@ Proof.
   apply remove_first_subset with (r := r). exact Hin.
 Qed.
 
+(** [region_membership_eq_preserves_typing]: typing depends on the region
+    environment only via [In]-membership of region names. So if [R'] agrees
+    with [R] on which names are present, every typing derivation transports
+    from [R] to [R']. Used to close the T_Region_Active shadowing case in
+    [region_shrink_preserves_typing], where [R] and [remove_first r R]
+    (or [r :: remove_first r R]) agree on [In]-membership. *)
+Lemma region_membership_eq_preserves_typing :
+  forall R G e T G',
+    R; G |- e : T -| G' ->
+    forall R',
+      (forall r0, In r0 R <-> In r0 R') ->
+      R'; G |- e : T -| G'.
+Proof.
+  intros R G e T G' Htype.
+  induction Htype; intros R' Heq.
+  - apply T_Unit.
+  - apply T_Bool.
+  - apply T_I32.
+  - eapply T_Var_Lin; eassumption.
+  - eapply T_Var_Unr; eassumption.
+  - apply T_Loc. unfold region_active in *. apply Heq. exact H.
+  - apply T_StringNew. unfold region_active in *. apply Heq. exact H.
+  - eapply T_StringConcat;
+      [apply IHHtype1; exact Heq | apply IHHtype2; exact Heq].
+  - eapply T_StringLen. apply IHHtype. exact Heq.
+  - eapply T_Let;
+      [apply IHHtype1; exact Heq | apply IHHtype2; exact Heq].
+  - eapply T_LetLin;
+      [exact H | apply IHHtype1; exact Heq | apply IHHtype2; exact Heq].
+  - eapply T_Lam. apply IHHtype. exact Heq.
+  - eapply T_App;
+      [apply IHHtype1; exact Heq | apply IHHtype2; exact Heq].
+  - eapply T_Pair;
+      [apply IHHtype1; exact Heq | apply IHHtype2; exact Heq].
+  - eapply T_Fst; [apply IHHtype; exact Heq | assumption].
+  - eapply T_Snd; [apply IHHtype; exact Heq | assumption].
+  - eapply T_Inl. apply IHHtype. exact Heq.
+  - eapply T_Inr. apply IHHtype. exact Heq.
+  - eapply T_Case;
+      [apply IHHtype1; exact Heq
+      | apply IHHtype2; exact Heq
+      | apply IHHtype3; exact Heq].
+  - eapply T_If;
+      [apply IHHtype1; exact Heq
+      | apply IHHtype2; exact Heq
+      | apply IHHtype3; exact Heq].
+  - (* T_Region *)
+    eapply T_Region.
+    + intros Hin. apply H. apply Heq. exact Hin.
+    + exact H0.
+    + apply IHHtype. intros r1. simpl.
+      split; intros [Heq'|Hin]; [left; exact Heq' | right; apply Heq; exact Hin
+                                | left; exact Heq' | right; apply Heq; exact Hin].
+  - (* T_Region_Active *)
+    eapply T_Region_Active.
+    + apply Heq. exact H.
+    + exact H0.
+    + apply IHHtype. exact Heq.
+  - eapply T_Borrow. exact H.
+  - eapply T_Borrow_Val; [exact H | apply IHHtype; exact Heq].
+  - eapply T_Drop; [exact H | apply IHHtype; exact Heq].
+  - eapply T_Copy; [exact H | apply IHHtype; exact Heq].
+Qed.
+
+(** [region_extension_preserves_typing_when_free]: the symmetric
+    counterpart of [region_shrink_preserves_typing]. If an expression is
+    typed at [R] and makes no syntactic reference to region [r], then its
+    typing survives prepending [r] to [R]. Used by the preservation proof
+    for the S_Region_Step + T_Region_Active case where the inner step
+    drops the only occurrence of [r] from the env. *)
+Lemma region_extension_preserves_typing_when_free :
+  forall R G e T G' r,
+    R; G |- e : T -| G' ->
+    expr_free_of_region r e ->
+    (r :: R); G |- e : T -| G'.
+Proof.
+  intros R G e T G' r Htype.
+  induction Htype; intros Hfree; simpl in Hfree.
+  - apply T_Unit.
+  - apply T_Bool.
+  - apply T_I32.
+  - eapply T_Var_Lin; eassumption.
+  - eapply T_Var_Unr; eassumption.
+  - apply T_Loc. unfold region_active in *. right. exact H.
+  - apply T_StringNew. unfold region_active in *. right. exact H.
+  - destruct Hfree as [Hf1 Hf2].
+    eapply T_StringConcat;
+      [apply IHHtype1; exact Hf1 | apply IHHtype2; exact Hf2].
+  - eapply T_StringLen. apply IHHtype. exact Hfree.
+  - destruct Hfree as [Hf1 Hf2].
+    eapply T_Let;
+      [apply IHHtype1; exact Hf1 | apply IHHtype2; exact Hf2].
+  - destruct Hfree as [Hf1 Hf2].
+    eapply T_LetLin;
+      [exact H | apply IHHtype1; exact Hf1 | apply IHHtype2; exact Hf2].
+  - eapply T_Lam. apply IHHtype. exact Hfree.
+  - destruct Hfree as [Hf1 Hf2].
+    eapply T_App;
+      [apply IHHtype1; exact Hf1 | apply IHHtype2; exact Hf2].
+  - destruct Hfree as [Hf1 Hf2].
+    eapply T_Pair;
+      [apply IHHtype1; exact Hf1 | apply IHHtype2; exact Hf2].
+  - eapply T_Fst; [apply IHHtype; exact Hfree | assumption].
+  - eapply T_Snd; [apply IHHtype; exact Hfree | assumption].
+  - eapply T_Inl. apply IHHtype. exact Hfree.
+  - eapply T_Inr. apply IHHtype. exact Hfree.
+  - destruct Hfree as [Hf1 [Hf2 Hf3]].
+    eapply T_Case;
+      [apply IHHtype1; exact Hf1
+      | apply IHHtype2; exact Hf2
+      | apply IHHtype3; exact Hf3].
+  - destruct Hfree as [Hf1 [Hf2 Hf3]].
+    eapply T_If;
+      [apply IHHtype1; exact Hf1
+      | apply IHHtype2; exact Hf2
+      | apply IHHtype3; exact Hf3].
+  - (* T_Region: original env R, extends to r0 :: R *)
+    destruct (String.eqb r r0) eqn:Heq.
+    + (* sub-case a: r = r0. ERegion r e is shadowing. Hfree = True (trivial).
+         Original Htype : (r :: R); G |- e : T -| G'. Apply T_Region_Active. *)
+      apply String.eqb_eq in Heq. subst r0.
+      eapply T_Region_Active.
+      * left. reflexivity.
+      * exact H0.
+      * exact Htype.
+    + (* sub-case b: r ≠ r0. Apply T_Region; swap (r :: r0 :: R) <-> (r0 :: r :: R) via membership-eq. *)
+      apply String.eqb_neq in Heq.
+      eapply T_Region.
+      * intros [Heq' | HinR];
+          [apply Heq; exact Heq' | apply H; exact HinR].
+      * exact H0.
+      * eapply region_membership_eq_preserves_typing.
+        -- apply IHHtype. exact Hfree.
+        -- intros r2. simpl. tauto.
+  - (* T_Region_Active: original env R, In r0 R, no extension *)
+    destruct (String.eqb r r0) eqn:Heq.
+    + (* sub-case a: r = r0. Use membership-eq to transport from R to (r :: R)
+         since In r R already. *)
+      apply String.eqb_eq in Heq. subst r0.
+      eapply region_membership_eq_preserves_typing.
+      * eapply T_Region_Active; [exact H | exact H0 | exact Htype].
+      * intros r2. simpl. split.
+        -- intros HinR. right. exact HinR.
+        -- intros [Heq' | HinR]; [subst; exact H | exact HinR].
+    + (* sub-case b: r ≠ r0. Apply T_Region_Active; In r0 (r :: R) via right-disj. *)
+      apply String.eqb_neq in Heq.
+      eapply T_Region_Active.
+      * right. exact H.
+      * exact H0.
+      * apply IHHtype. exact Hfree.
+  - eapply T_Borrow. exact H.
+  - eapply T_Borrow_Val; [exact H | apply IHHtype; exact Hfree].
+  - eapply T_Drop; [exact H | apply IHHtype; exact Hfree].
+  - eapply T_Copy; [exact H | apply IHHtype; exact Hfree].
+Qed.
+
 Lemma region_shrink_preserves_typing :
   forall R G e T G' r,
     R; G |- e : T -| G' ->
@@ -3005,8 +3151,41 @@ Proof.
   - (* T_Region_Active *)
     destruct (String.eqb r r0) eqn:Heq.
     + apply String.eqb_eq in Heq. subst r0.
-      (* r = r0 active. Same weakening issue. Admit. *)
-      admit.
+      (* r = r0 active: outer ERegion r e shadows the outer r. Hfree is
+         trivially True. Case-split on whether r still appears in
+         (remove_first r R) (multiplicity > 1) or not (= 1). Both branches
+         transport Htype via region_membership_eq_preserves_typing, since
+         R and {remove_first r R | r :: remove_first r R} agree on
+         In-membership in their respective cases. *)
+      destruct (in_dec String.string_dec r (remove_first r R)) as [Hin | Hnin].
+      * (* multiplicity > 1: r still active after one removal. Apply T_Region_Active. *)
+        eapply T_Region_Active.
+        -- exact Hin.
+        -- exact H0.
+        -- eapply region_membership_eq_preserves_typing; [exact Htype|].
+           intros r1.
+           destruct (String.eqb r r1) eqn:Hreq.
+           ++ apply String.eqb_eq in Hreq. subst r1.
+              split; intros _; assumption.
+           ++ apply String.eqb_neq in Hreq.
+              apply region_shrink_in_preserves. exact Hreq.
+      * (* multiplicity = 1: r removed. Apply T_Region (re-binds r afresh). *)
+        eapply T_Region.
+        -- exact Hnin.
+        -- exact H0.
+        -- eapply region_membership_eq_preserves_typing; [exact Htype|].
+           intros r1. simpl.
+           destruct (String.eqb r r1) eqn:Hreq.
+           ++ apply String.eqb_eq in Hreq. subst r1.
+              split; [intros _; left; reflexivity | intros _; exact H].
+           ++ apply String.eqb_neq in Hreq.
+              assert (Hsh : In r1 R <-> In r1 (remove_first r R)).
+              { apply region_shrink_in_preserves. exact Hreq. }
+              split.
+              ** intros HinR. right. apply Hsh. exact HinR.
+              ** intros [HeqR1|HinRem].
+                 --- exfalso. apply Hreq. exact HeqR1.
+                 --- apply Hsh. exact HinRem.
     + eapply T_Region_Active.
       * apply region_shrink_in_preserves.
         -- intros ->. rewrite String.eqb_refl in Heq. discriminate.
@@ -3017,7 +3196,7 @@ Proof.
   - eapply T_Borrow_Val; [exact H|apply IHHtype; exact Hfree].
   - eapply T_Drop; [exact H|apply IHHtype; exact Hfree].
   - eapply T_Copy; [exact H|apply IHHtype; exact Hfree].
-Admitted.
+Qed.
 
 Theorem preservation :
   forall mu R e mu' R' e',
diff --git a/formal/Typing.v b/formal/Typing.v
index 9487980c..6271b3d7 100644
--- a/formal/Typing.v
+++ b/formal/Typing.v
@@ -41,23 +41,6 @@ Fixpoint free_regions (T : ty) : list region_name :=
   | TBorrow T'       => free_regions T'
   end.
 
-(** ** Free Regions in Types
-
-    Compute the set of regions mentioned in a type. Used to enforce
-    the "region does not escape" invariant in T_Region and T_Region_Active. *)
-
-Fixpoint free_regions (T : ty) : list region_name :=
-  match T with
-  | TBase _ => []
-  | TRef _ T => free_regions T
-  | TFun T1 T2 => free_regions T1 ++ free_regions T2
-  | TProd T1 T2 => free_regions T1 ++ free_regions T2
-  | TSum T1 T2 => free_regions T1 ++ free_regions T2
-  | TString r => [r]
-  | TRegion r T => r :: free_regions T
-  | TBorrow T => free_regions T
-  end.
-
 (* Note: We don't need a separate determinism lemma for free_regions
    since In_dec is built-in for list types in Coq. *)
 

From 0f7694f96a062840cd664195c82d4787cfa3d2ef Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 27 Apr 2026 13:02:08 +0100
Subject: [PATCH 2/3] =?UTF-8?q?chore(contractiles):=20k9=20=E2=86=92=20svc?=
 =?UTF-8?q?/,=20remove=20lust=20dir=20(ADR-001=202026-04-18)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
---
 .machine_readable/svc/README.adoc                | 16 ++++++++++++++++
 .../svc}/k9/ephapax-metadata.k9.ncl              |  0
 2 files changed, 16 insertions(+)
 create mode 100644 .machine_readable/svc/README.adoc
 rename {contractiles => .machine_readable/svc}/k9/ephapax-metadata.k9.ncl (100%)

diff --git a/.machine_readable/svc/README.adoc b/.machine_readable/svc/README.adoc
new file mode 100644
index 00000000..8e87e1d5
--- /dev/null
+++ b/.machine_readable/svc/README.adoc
@@ -0,0 +1,16 @@
+= `.machine_readable/svc/` — Service components for ephapax
+:toc:
+
+Service-layer components that sit alongside the contractile trident
+but are not themselves verbs. Per **ADR-001 (2026-04-18)**, K9 lives
+here rather than under `contractiles/` so the contractile directory
+stays a pure six-verb set (intend, trust, must, bust, adjust, dust).
+
+== Contents
+
+* `k9/` — K9 self-validating templates and validators.
+
+== Pointer
+
+For the verb contractiles themselves, see
+`.machine_readable/contractiles/`.
diff --git a/contractiles/k9/ephapax-metadata.k9.ncl b/.machine_readable/svc/k9/ephapax-metadata.k9.ncl
similarity index 100%
rename from contractiles/k9/ephapax-metadata.k9.ncl
rename to .machine_readable/svc/k9/ephapax-metadata.k9.ncl

From 630e64780c8b96aaeccee9b59a8681ebcf9195cf Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 27 Apr 2026 13:17:58 +0100
Subject: [PATCH 3/3] fix(deps): bump openssl 0.10.76 -> 0.10.78

Closes 5 dependabot alerts (4 HIGH + 1 LOW): rust-openssl memory-safety
issues including buffer overflows in derive/digest_final, OOB read in
PEM password callback, incorrect bounds in AES key wrap, and unchecked
callback length leaking memory to peer.

All five fixed in upstream openssl 0.10.78.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 Cargo.lock | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 5337368c..2625552c 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1949,9 +1949,9 @@ checksum = "d6790f58c7ff633d8771f42965289203411a5e5c68388703c06e14f24770b41e"
 
 [[package]]
 name = "openssl"
-version = "0.10.76"
+version = "0.10.78"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "951c002c75e16ea2c65b8c7e4d3d51d5530d8dfa7d060b4776828c88cfb18ecf"
+checksum = "f38c4372413cdaaf3cc79dd92d29d7d9f5ab09b51b10dded508fb90bb70b9222"
 dependencies = [
  "bitflags 2.11.0",
  "cfg-if",
@@ -1987,9 +1987,9 @@ checksum = "7c87def4c32ab89d880effc9e097653c8da5d6ef28e6b539d313baaacfbafcbe"
 
 [[package]]
 name = "openssl-sys"
-version = "0.9.112"
+version = "0.9.114"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "57d55af3b3e226502be1526dfdba67ab0e9c96fc293004e79576b2b9edb0dbdb"
+checksum = "13ce1245cd07fcc4cfdb438f7507b0c7e4f3849a69fd84d52374c66d83741bb6"
 dependencies = [
  "cc",
  "libc",
