Merge branch 'main' into claude/modest-cori-kzjtcy

Author: hyperpolymath

.hypatia-ignore

@@ -45,3 +45,9 @@ cicd_rules/banned_language_file:tools/res-to-affine/test/fixtures/phase3c.res
 # an inert no-op under the scanner's `grep -qxF` whole-line match.
 cicd_rules/vlang_detected:formal/K1_CodegenPreservation.v
 cicd_rules/banned_language_file:formal/K1_CodegenPreservation.v
+cicd_rules/vlang_detected:formal/K1Let_CodegenPreservation.v
+cicd_rules/banned_language_file:formal/K1Let_CodegenPreservation.v
+cicd_rules/vlang_detected:formal/F1_TransformerPreservation.v
+cicd_rules/banned_language_file:formal/F1_TransformerPreservation.v
+cicd_rules/vlang_detected:formal/Siblings_Stated.v
+cicd_rules/banned_language_file:formal/Siblings_Stated.v

docs/PROOF-NEEDS.adoc

@@ -68,9 +68,11 @@ than the prose corpus suggests:
   `TypeSafety.v` is example lemmas about list length, not AffineScript. Not
   core-metatheory.
 * **`formal/`** — the directory #513 names as the mechanized-proof target now
-  **exists** (Coq/Rocq 8.18). It holds the Wave-0 **K-1 seed**
-  (`formal/K1_CodegenPreservation.v`) — a complete, axiom-free
-  codegen-preservation proof for a minimal nat/bool fragment (see <<outstanding>>).
+  **exists** (Coq/Rocq 8.18), axiom-free throughout: `K1_CodegenPreservation.v`
+  (K-1, minimal fragment) + `K1Let_CodegenPreservation.v` (K-1 grown with
+  variables/`let`/environment) + `F1_TransformerPreservation.v` (F-1, composing
+  on K-1) are mechanized; `Siblings_Stated.v` states P-2/P-3/F-3/F-4 as
+  parametric propositions (see <<outstanding>>, <<faces>>).
 * **Research tracks** (not core soundness): `docs/academic/tropical-session-types/`
   (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`,
   `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue,
@@ -230,8 +232,8 @@ cover them.
   well-typed face-`F` programs `p`. This is the *front-end* analogue of the
   backend keystone K-1; together they give end-to-end "same cube". Needs the
   AffineScript AST + wasm semantics formalised.
-| XL | `absent`
-| new
+| XL | `partial`
+| mechanized fragment: `formal/F1_TransformerPreservation.v` (composes on K-1)
 
 | F-2
 | **Same-cube cross-face agreement (observational).** Any two faces compiling
@@ -250,8 +252,8 @@ cover them.
   jaffa→Js, pseudo→Pseudocode, lucid→Lucid, cafe→Cafe, +brand names) is a
   *function* (no name maps to two faces); and dispatch `--face` > pragma >
   extension is confluent (same source ⇒ same face). Face analogue of P-7.
-| M | `absent`
-| new; `lib/face_pragma.ml`
+| M | `stated`
+| Coq statement: `formal/Siblings_Stated.v` (F3); `lib/face_pragma.ml`
 
 | F-4
 | **Error-vocabulary faithfulness (simulation).** Each `Face.format_*_for_face`
@@ -260,8 +262,8 @@ cover them.
   is a total simulation of the canonical error algebra (exhaustiveness is
   OCaml-checked; *semantic* faithfulness is not), so a face can never make error
   *X* read as a different error *Y*.
-| M | `absent`
-| new; `lib/face.ml`
+| M | `stated`
+| Coq statement: `formal/Siblings_Stated.v` (F4); `lib/face.ml`
 
 | F-5
 | **`render_ty` faithfulness / non-collision.** The per-face type renaming
@@ -325,10 +327,10 @@ F-1 (full transformer preservation) is non-trivial rather than a formality.
 | Wave | Items | Gates
 
 | 0
-| *In progress.* DONE: `formal/` stood up (Coq/Rocq); **K-1 seed mechanized**
-  (`K1_CodegenPreservation.v`, axiom-free). NEXT: *state* P-2, P-3 (rejecting
-  #554), F-1, F-3, F-4 as signatures, mirroring solo-core; cross-link
-  `CAPABILITY-MATRIX.adoc` rows (K-4).
+| *Substantially done.* `formal/` stood up (Coq); **K-1 mechanized** + **grown**
+  (variables/`let`); **F-1 mechanized** (composes on K-1); **P-2/P-3/F-3/F-4
+  stated** as Coq signatures. All axiom-free. NEXT: grow K-1 with `if`;
+  discharge a stated sibling; cross-link `CAPABILITY-MATRIX.adoc` rows (K-4).
 | —
 
 | 1

formal/F1_TransformerPreservation.v

@@ -0,0 +1,129 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   F1_TransformerPreservation.v
+   ════════════════════════════
+   Wave-0 seed of obligation **F-1** from docs/PROOF-NEEDS.adoc: the *real*
+   same-cube theorem — each face's surface→canonical transform `T_F` preserves
+   the typed-WASM denotation. F-1 is the front-end twin of K-1; this file
+   *composes on top of* K-1 (it `Require`s it) exactly as the inventory says.
+
+   A "face" is an alternate surface syntax (rattle/jaffa/pseudo/lucid/cafe/…)
+   whose parser yields a surface AST `fexp`; `elaborate : fexp -> sexp` is the
+   transform `T_F` into the canonical AST that K-1's `compile` consumes. We give
+   the face its OWN big-step semantics `feval` (what a reader of that surface
+   expects) and prove the transform preserves it — then chain K-1 to get
+   end-to-end codegen preservation, and state the cross-face "same cube".
+
+   Like K-1, everything here is complete and axiom-free (no `Admitted`).
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+
+   Check:  coqc -Q . ASFormal F1_TransformerPreservation.v   (after K-1)
+*)
+
+Require Import List.
+Import ListNotations.
+Require Import ASFormal.K1_CodegenPreservation.
+
+(* ═══════════ A face surface: canonical forms + parser sugar ═══════════════ *)
+
+(* `FSum3`/`FAll3` are surface sugar a face parser may emit (n-ary fold spelt
+   as one node) — they stand in for any derived surface form that elaborates
+   to a tree of canonical operations. *)
+Inductive fexp : Type :=
+| FNat  (n : nat)
+| FBool (b : bool)
+| FAdd  (a b : fexp)
+| FAnd  (a b : fexp)
+| FSum3 (a b c : fexp)    (* sugar for  a + (b + c)  *)
+| FAll3 (a b c : fexp).   (* sugar for  a && (b && c) *)
+
+(* The transform T_F : surface AST -> canonical AST (`sexp` from K-1). *)
+Fixpoint elaborate (f : fexp) : sexp :=
+  match f with
+  | FNat n     => SNat n
+  | FBool b    => SBool b
+  | FAdd a b   => SAdd (elaborate a) (elaborate b)
+  | FAnd a b   => SAnd (elaborate a) (elaborate b)
+  | FSum3 a b c => SAdd (elaborate a) (SAdd (elaborate b) (elaborate c))
+  | FAll3 a b c => SAnd (elaborate a) (SAnd (elaborate b) (elaborate c))
+  end.
+
+(* The face's own big-step semantics — what a reader of this surface expects,
+   defined directly (not via elaboration), so that agreement is a theorem. *)
+Fixpoint feval (f : fexp) : option sval :=
+  match f with
+  | FNat n  => Some (VNat n)
+  | FBool b => Some (VBool b)
+  | FAdd a b =>
+      match feval a, feval b with
+      | Some (VNat x), Some (VNat y) => Some (VNat (x + y))
+      | _, _ => None
+      end
+  | FAnd a b =>
+      match feval a, feval b with
+      | Some (VBool x), Some (VBool y) => Some (VBool (andb x y))
+      | _, _ => None
+      end
+  | FSum3 a b c =>
+      match feval a, feval b, feval c with
+      | Some (VNat x), Some (VNat y), Some (VNat z) => Some (VNat (x + (y + z)))
+      | _, _, _ => None
+      end
+  | FAll3 a b c =>
+      match feval a, feval b, feval c with
+      | Some (VBool x), Some (VBool y), Some (VBool z) => Some (VBool (andb x (andb y z)))
+      | _, _, _ => None
+      end
+  end.
+
+(* ════════════ F-1: the transform preserves meaning ═══════════════════════ *)
+
+(* Transform semantics-preservation: the face's own semantics agrees, on the
+   nose, with elaborating-then-evaluating canonically. *)
+Theorem f1_transform_preserves_eval : forall f, feval f = seval (elaborate f).
+Proof.
+  induction f as [ n | b | a IHa b IHb | a IHa b IHb
+                 | a IHa b IHb c IHc | a IHa b IHb c IHc ]; simpl.
+  - reflexivity.
+  - reflexivity.
+  - rewrite IHa, IHb; reflexivity.
+  - rewrite IHa, IHb; reflexivity.
+  - (* FSum3: flat 3-way match vs nested — destruct to align *)
+    rewrite IHa, IHb, IHc;
+    destruct (seval (elaborate a)) as [[x | ] | ];
+    destruct (seval (elaborate b)) as [[y | ] | ];
+    destruct (seval (elaborate c)) as [[z | ] | ]; reflexivity.
+  - rewrite IHa, IHb, IHc;
+    destruct (seval (elaborate a)) as [[ | x] | ];
+    destruct (seval (elaborate b)) as [[ | y] | ];
+    destruct (seval (elaborate c)) as [[ | z] | ]; reflexivity.
+Qed.
+
+(* End-to-end (the F-1 "same cube" at the value level): compiling the
+   elaborated face program agrees with the face's own semantics — obtained by
+   chaining the transform lemma with K-1's backend theorem. *)
+Theorem f1_codegen_preservation : forall f v,
+  feval f = Some v ->
+  wexec (compile (elaborate f)) [] = Some [obs v].
+Proof.
+  intros f v Hf.
+  apply k1_preservation_holds.
+  rewrite <- f1_transform_preserves_eval.
+  exact Hf.
+Qed.
+
+(* Cross-face same-cube: two faces whose transforms land on the same canonical
+   AST emit byte-identical code (hence the same wasm). The observational
+   version for the trailing-statement/tail split is mechanized separately in
+   invariant-path/proofs/SameCube.agda (F-2). *)
+Corollary f1_same_cube : forall f1 f2,
+  elaborate f1 = elaborate f2 ->
+  compile (elaborate f1) = compile (elaborate f2).
+Proof.
+  intros f1 f2 H; rewrite H; reflexivity.
+Qed.
+
+Print Assumptions f1_transform_preserves_eval.
+Print Assumptions f1_codegen_preservation.

formal/K1Let_CodegenPreservation.v

@@ -0,0 +1,179 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+
+(*
+   K1Let_CodegenPreservation.v
+   ═══════════════════════════
+   K-1, GROWN. Extends the minimal K1_CodegenPreservation fragment with the
+   first real binder: de Bruijn **variables** and **`let`**, evaluated under an
+   environment. The target machine gains a **locals** register alongside the
+   operand stack; compilation balances `IBind`/`IUnbind` so locals scope
+   correctly. The codegen-preservation theorem is re-proven for this richer
+   fragment — still complete and axiom-free (no `Admitted`).
+
+   This is a step of the K-1 obligation toward the real AST (binders →
+   environments). `if`/control-flow is the next increment (it needs structured
+   target control + a termination measure, deliberately out of this step).
+
+   `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore.
+   Check:  coqc -Q . ASFormal K1Let_CodegenPreservation.v
+*)
+
+Require Import List.
+Import ListNotations.
+
+(* ════════════════════════ Source (env-based, with let) ═══════════════════ *)
+
+Inductive sval : Type := VNat (n : nat) | VBool (b : bool).
+
+Inductive sexp : Type :=
+| SNat (n : nat)
+| SBool (b : bool)
+| SVar (i : nat)             (* de Bruijn index into the environment *)
+| SAdd (a b : sexp)
+| SAnd (a b : sexp)
+| SLet (e1 e2 : sexp).       (* let x = e1 in e2 ; x is index 0 in e2 *)
+
+Definition senv := list sval.
+
+Fixpoint seval (env : senv) (e : sexp) : option sval :=
+  match e with
+  | SNat n  => Some (VNat n)
+  | SBool b => Some (VBool b)
+  | SVar i  => nth_error env i
+  | SAdd a b =>
+      match seval env a, seval env b with
+      | Some (VNat x), Some (VNat y) => Some (VNat (x + y))
+      | _, _ => None
+      end
+  | SAnd a b =>
+      match seval env a, seval env b with
+      | Some (VBool x), Some (VBool y) => Some (VBool (andb x y))
+      | _, _ => None
+      end
+  | SLet e1 e2 =>
+      match seval env e1 with
+      | Some v => seval (v :: env) e2
+      | None   => None
+      end
+  end.
+
+(* ═══════════════ Target: stack machine + a locals register ════════════════ *)
+
+Inductive wval : Type := WNat (n : nat) | WBool (b : bool).
+
+Definition obs (v : sval) : wval :=
+  match v with VNat n => WNat n | VBool b => WBool b end.
+
+Inductive instr : Type :=
+| IPushN (n : nat)
+| IPushB (b : bool)
+| IGet   (i : nat)   (* push locals[i] onto the stack *)
+| IAdd
+| IAnd
+| IBind              (* pop stack top, push it onto locals (new index 0) *)
+| IUnbind.           (* drop locals[0]; operand stack unchanged *)
+
+Definition code   := list instr.
+Definition locals := list wval.
+Definition stack  := list wval.
+
+Definition wstep (i : instr) (l : locals) (s : stack) : option (locals * stack) :=
+  match i, l, s with
+  | IPushN n, l, s                   => Some (l, WNat n :: s)
+  | IPushB b, l, s                   => Some (l, WBool b :: s)
+  | IGet k, l, s                     =>
+      match nth_error l k with
+      | Some w => Some (l, w :: s)
+      | None   => None
+      end
+  | IAdd, l, WNat b :: WNat a :: s'  => Some (l, WNat (a + b) :: s')
+  | IAnd, l, WBool b :: WBool a :: s' => Some (l, WBool (andb a b) :: s')
+  | IBind, l, w :: s'                => Some (w :: l, s')
+  | IUnbind, _ :: l', s              => Some (l', s)
+  | _, _, _                          => None
+  end.
+
+Fixpoint wexec (c : code) (l : locals) (s : stack) : option (locals * stack) :=
+  match c with
+  | []        => Some (l, s)
+  | i :: rest =>
+      match wstep i l s with
+      | Some (l', s') => wexec rest l' s'
+      | None          => None
+      end
+  end.
+
+Fixpoint compile (e : sexp) : code :=
+  match e with
+  | SNat n     => [IPushN n]
+  | SBool b    => [IPushB b]
+  | SVar i     => [IGet i]
+  | SAdd a b   => compile a ++ compile b ++ [IAdd]
+  | SAnd a b   => compile a ++ compile b ++ [IAnd]
+  | SLet e1 e2 => compile e1 ++ [IBind] ++ compile e2 ++ [IUnbind]
+  end.
+
+(* ═════════════════════════ preservation (no Admitted) ════════════════════ *)
+
+(* Execution distributes over code concatenation — the workhorse that lets the
+   `let` case step its `IBind`/`IUnbind` cleanly without continuation juggling. *)
+Lemma wexec_app : forall c1 c2 l s,
+  wexec (c1 ++ c2) l s =
+  match wexec c1 l s with
+  | Some (l', s') => wexec c2 l' s'
+  | None          => None
+  end.
+Proof.
+  induction c1 as [| i c1 IH]; intros c2 l s; simpl.
+  - reflexivity.
+  - destruct (wstep i l s) as [[l' s'] |]; [apply IH | reflexivity].
+Qed.
+
+(* Codegen preservation, generalized over the operand stack `s` and carrying
+   the environment/locals correspondence `l = map obs env`. `IUnbind` restores
+   locals, so the machine returns to the same `l` it started with. *)
+Lemma compile_correct : forall e env v l s,
+  seval env e = Some v ->
+  l = map obs env ->
+  wexec (compile e) l s = Some (l, obs v :: s).
+Proof.
+  induction e as [n | b | i | a IHa b IHb | a IHa b IHb | e1 IH1 e2 IH2];
+    intros env v l s Hev Hl; simpl in Hev; subst l.
+  - (* SNat *)  inversion Hev; subst; reflexivity.
+  - (* SBool *) inversion Hev; subst; reflexivity.
+  - (* SVar *)
+    apply (map_nth_error obs) in Hev; simpl; rewrite Hev; reflexivity.
+  - (* SAdd *)
+    destruct (seval env a) as [[x | xb] |] eqn:Ha; try discriminate;
+    destruct (seval env b) as [[y | yb] |] eqn:Hb; try discriminate;
+    inversion Hev; subst; clear Hev; simpl compile;
+    rewrite wexec_app, (IHa env (VNat x) (map obs env) s Ha eq_refl); simpl;
+    rewrite wexec_app, (IHb env (VNat y) (map obs env) (WNat x :: s) Hb eq_refl); simpl;
+    reflexivity.
+  - (* SAnd *)
+    destruct (seval env a) as [[xn | x] |] eqn:Ha; try discriminate;
+    destruct (seval env b) as [[yn | y] |] eqn:Hb; try discriminate;
+    inversion Hev; subst; clear Hev; simpl compile;
+    rewrite wexec_app, (IHa env (VBool x) (map obs env) s Ha eq_refl); simpl;
+    rewrite wexec_app, (IHb env (VBool y) (map obs env) (WBool x :: s) Hb eq_refl); simpl;
+    reflexivity.
+  - (* SLet *)
+    destruct (seval env e1) as [v1 |] eqn:H1; try discriminate; simpl in Hev;
+    simpl compile;
+    rewrite wexec_app, (IH1 env v1 (map obs env) s H1 eq_refl); simpl;
+    rewrite wexec_app, (IH2 (v1 :: env) v (obs v1 :: map obs env) s Hev eq_refl); simpl;
+    reflexivity.
+Qed.
+
+(* For a closed program (empty env) the locals balance back to empty and the
+   result is the single wasm value on the operand stack. *)
+Theorem k1let_preservation_holds : forall e v,
+  seval [] e = Some v ->
+  wexec (compile e) [] [] = Some ([], [obs v]).
+Proof.
+  intros e v H.
+  exact (compile_correct e [] v [] [] H eq_refl).
+Qed.
+
+Print Assumptions k1let_preservation_holds.