feat(echo): echo types through the OCaml pipeline (typecheck + eval + parser) + TangleIR contract

compiler/lib/ast.ml

@@ -80,6 +80,18 @@ and expr =
   | Cup       of expr * expr
   | Twist     of expr
 
+  (* ---- Echo types (structured loss) — mirror the Lean spec in
+   *      proofs/Tangle.lean (Ty.echo / Ty.prod and the echo operations).
+   *      Typed by typecheck.ml; surface parser syntax is a follow-on. ---- *)
+  | EchoClose of expr                 (* echo-preserving closure (residue-retaining close) *)
+  | Lower     of expr                 (* project an echo to its result *)
+  | Residue   of expr                 (* project an echo to its residue (recover witness) *)
+  | Pair      of expr * expr          (* product introduction *)
+  | Fst       of expr                 (* first projection *)
+  | Snd       of expr                 (* second projection *)
+  | EchoAdd   of expr * expr          (* echo-preserving addition (residue = summand pair) *)
+  | EchoEq    of expr * expr          (* echo-preserving equality (residue = operand pair) *)
+
   (* ---- Literals ---- *)
   | BraidLit  of generator list
   | Identity

compiler/lib/eval.ml

@@ -42,6 +42,9 @@ type value =
   | VFun       of string list * expr * env  (** Closure: params, body, captured env *)
   | VUnit                             (** Unit / void result *)
   | VInvariant of string * string     (** Invariant name, result string *)
+  | VEcho      of value * value       (** Formed echo: residue, result —
+                                          mirrors [echoVal] in proofs/Tangle.lean *)
+  | VPair      of value * value       (** Product value *)
 
 (** Runtime environment: association list of name-value bindings. *)
 and env = (string * value) list
@@ -77,7 +80,7 @@ let pp_braid (gens : gen list) : string =
   | _  -> "braid[" ^ String.concat ", " (List.map pp_gen gens) ^ "]"
 
 (** Pretty-print a value. *)
-let pp_value (v : value) : string =
+let rec pp_value (v : value) : string =
   match v with
   | VInt n        -> string_of_int n
   | VFloat f      -> Printf.sprintf "%g" f
@@ -89,6 +92,10 @@ let pp_value (v : value) : string =
   | VFun _        -> "<function>"
   | VUnit         -> "()"
   | VInvariant (name, result) -> Printf.sprintf "%s = %s" name result
+  | VEcho (res, result) ->
+    "echo(" ^ pp_value res ^ ", " ^ pp_value result ^ ")"
+  | VPair (a, b) ->
+    "(" ^ pp_value a ^ ", " ^ pp_value b ^ ")"
 
 (* ================================================================== *)
 (*  Environment operations                                             *)
@@ -429,6 +436,68 @@ let rec eval_expr (env : env) (e : expr) : value =
     in
     try_arms arms
 
+  (* ---- Echo types (structured loss) ----
+   * Mirror the small-step Step rules in proofs/Tangle.lean:
+   *   echoCloseWord : echoClose(braidLit gs) ⟶ echoVal (braidLit gs) identity
+   *   lowerVal      : lower (echoVal r v)     ⟶ v
+   *   residueVal    : residue (echoVal r v)   ⟶ r
+   *   fstPair       : fst (pair a b)          ⟶ a
+   *   sndPair       : snd (pair a b)          ⟶ b
+   *   echoAddNums   : echoAdd (num a) (num b) ⟶ echoVal (pair a b) (num (a+b))
+   *   echoEqNums    : echoEq  a       b       ⟶ echoVal (pair a b) (boolLit (a==b))
+   * The result component of a closure echo is the identity value (Word[0]),
+   * matching the [closeId]/[closeWord] reduct used elsewhere in this file. *)
+
+  | EchoClose e1 ->
+    (* echo-preserving closure: residue retains the witness; the result is the
+       identity value (Word[0]), the same point the empty/identity close yields. *)
+    let v = eval_expr env e1 in
+    VEcho (v, VBraid [])
+
+  | Lower e1 ->
+    begin match eval_expr env e1 with
+    | VEcho (_, r) -> r
+    | v -> eval_error "lower expects an echo value, got %s" (pp_value v)
+    end
+
+  | Residue e1 ->
+    begin match eval_expr env e1 with
+    | VEcho (res, _) -> res
+    | v -> eval_error "residue expects an echo value, got %s" (pp_value v)
+    end
+
+  | Pair (e1, e2) ->
+    (* Force left-to-right evaluation (Lean pairLeft reduces e1 first). *)
+    let a = eval_expr env e1 in
+    let b = eval_expr env e2 in
+    VPair (a, b)
+
+  | Fst e1 ->
+    begin match eval_expr env e1 with
+    | VPair (a, _) -> a
+    | v -> eval_error "fst expects a pair, got %s" (pp_value v)
+    end
+
+  | Snd e1 ->
+    begin match eval_expr env e1 with
+    | VPair (_, b) -> b
+    | v -> eval_error "snd expects a pair, got %s" (pp_value v)
+    end
+
+  | EchoAdd (e1, e2) ->
+    (* Residue = the summand pair; result = their sum (reuse the Add logic). *)
+    let v1 = eval_expr env e1 in
+    let v2 = eval_expr env e2 in
+    let sum = eval_binop Add v1 v2 in
+    VEcho (VPair (v1, v2), sum)
+
+  | EchoEq (e1, e2) ->
+    (* Residue = the operand pair; result = their equality (reuse the Eq logic). *)
+    let v1 = eval_expr env e1 in
+    let v2 = eval_expr env e2 in
+    let b = eval_binop Eq v1 v2 in
+    VEcho (VPair (v1, v2), b)
+
 (** Evaluate a binary operation on two values. *)
 and eval_binop (op : binop) (v1 : value) (v2 : value) : value =
   match op with

compiler/lib/lexer.mll

@@ -45,6 +45,15 @@
     | "cap"       -> CAP
     | "cup"       -> CUP
     | "braid"     -> BRAID
+    (* Echo / product forms — surface syntax mirrors pretty.ml output. *)
+    | "echoClose" -> ECHOCLOSE
+    | "lower"     -> LOWER
+    | "residue"   -> RESIDUE
+    | "pair"      -> PAIR
+    | "fst"       -> FST
+    | "snd"       -> SND
+    | "echoAdd"   -> ECHOADD
+    | "echoEq"    -> ECHOEQ
     | "jones"     -> JONES
     | "alexander" -> ALEXANDER
     | "homfly"    -> HOMFLY

compiler/lib/parser.mly

@@ -32,6 +32,9 @@
 %token IDENTITY TRUE FALSE
 %token CLOSE MIRROR REVERSE SIMPLIFY CAP CUP BRAID
 
+(* Echo / product forms — surface syntax mirrors pretty.ml output *)
+%token ECHOCLOSE LOWER RESIDUE PAIR FST SND ECHOADD ECHOEQ
+
 (* Invariant names *)
 %token JONES ALEXANDER HOMFLY KAUFFMAN WRITHE LINKING
 
@@ -263,6 +266,18 @@ unary_expr:
     { Cap (e1, e2) }
   | CUP LPAREN e1 = expr COMMA e2 = expr RPAREN
     { Cup (e1, e2) }
+  (* ---- Echo / product forms (mirror pretty.ml output) ---- *)
+  | ECHOCLOSE LPAREN e = expr RPAREN   { EchoClose e }
+  | LOWER     LPAREN e = expr RPAREN   { Lower e }
+  | RESIDUE   LPAREN e = expr RPAREN   { Residue e }
+  | FST       LPAREN e = expr RPAREN   { Fst e }
+  | SND       LPAREN e = expr RPAREN   { Snd e }
+  | PAIR LPAREN e1 = expr COMMA e2 = expr RPAREN
+    { Pair (e1, e2) }
+  | ECHOADD LPAREN e1 = expr COMMA e2 = expr RPAREN
+    { EchoAdd (e1, e2) }
+  | ECHOEQ LPAREN e1 = expr COMMA e2 = expr RPAREN
+    { EchoEq (e1, e2) }
   | t = twist_expr                     { t }
   | MINUS e = primary_expr             { UnaryOp (Neg, e) }
   | e = primary_expr                   { e }

compiler/lib/pretty.ml

@@ -171,6 +171,52 @@ let rec pp_expr ctx = function
     pp_expr ctx e;
     emit ctx ")"
 
+  | EchoClose e ->
+    emit ctx "echoClose(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | Lower e ->
+    emit ctx "lower(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | Residue e ->
+    emit ctx "residue(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | Pair (e1, e2) ->
+    emit ctx "pair(";
+    pp_expr ctx e1;
+    emit ctx ", ";
+    pp_expr ctx e2;
+    emit ctx ")"
+
+  | Fst e ->
+    emit ctx "fst(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | Snd e ->
+    emit ctx "snd(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | EchoAdd (e1, e2) ->
+    emit ctx "echoAdd(";
+    pp_expr ctx e1;
+    emit ctx ", ";
+    pp_expr ctx e2;
+    emit ctx ")"
+
+  | EchoEq (e1, e2) ->
+    emit ctx "echoEq(";
+    pp_expr ctx e1;
+    emit ctx ", ";
+    pp_expr ctx e2;
+    emit ctx ")"
+
   | BraidLit gens ->
     emit ctx "braid[";
     List.iteri (fun i g ->

compiler/lib/token.ml

@@ -52,6 +52,15 @@ and token =
   | CAP
   | CUP
   | BRAID
+  (* Echo / product forms *)
+  | ECHOCLOSE
+  | LOWER
+  | RESIDUE
+  | PAIR
+  | FST
+  | SND
+  | ECHOADD
+  | ECHOEQ
 
   (* ---- Invariant names ---- *)
   | JONES

compiler/lib/typecheck.ml

@@ -41,6 +41,9 @@ type ty =
   | TNum                            (** Num — integers and floats *)
   | TBool                           (** Bool — booleans *)
   | TStr                            (** Str — strings *)
+  | TProd   of ty * ty              (** ρ × σ — product / residue carrier for lossy ops *)
+  | TEcho   of ty * ty              (** Echo[ρ, τ] — structured loss: residue ρ, result τ.
+                                        Mirrors Ty.echo in proofs/Tangle.lean. *)
 
 (** Function signature: (param_types) -> return_type. *)
 type fun_sig = {
@@ -89,12 +92,14 @@ let pp_boundary (b : boundary) : string =
     "[" ^ String.concat ", " (List.map pp_strand_type b) ^ "]"
 
 (** Pretty-print a type. *)
-let pp_ty = function
+let rec pp_ty = function
   | TWord n        -> Printf.sprintf "Word[%d]" n
   | TTangle (a, b) -> Printf.sprintf "Tangle[%s, %s]" (pp_boundary a) (pp_boundary b)
   | TNum           -> "Num"
   | TBool          -> "Bool"
   | TStr           -> "Str"
+  | TProd (a, b)   -> Printf.sprintf "(%s * %s)" (pp_ty a) (pp_ty b)
+  | TEcho (r, t)   -> Printf.sprintf "Echo[%s, %s]" (pp_ty r) (pp_ty t)
 
 (* ================================================================== *)
 (*  Environment operations                                             *)
@@ -373,6 +378,66 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty =
     ) arm_types;
     result_ty
 
+  (* ---- Echo types (structured loss) ----
+   * Mirror the HasType rules in proofs/Tangle.lean:
+   *   [T-Echo-Close] echoClose e : Echo[Word[n], Word[0]]   when e : Word[n]
+   *   [T-Lower]      lower e      : τ                        when e : Echo[ρ, τ]
+   *   [T-Residue]    residue e    : ρ                        when e : Echo[ρ, τ]
+   *   [T-Pair]/[T-Fst]/[T-Snd]    product intro + projections
+   *   [T-Echo-Add]   echoAdd a b  : Echo[Num × Num, Num]
+   *   [T-Echo-Eq]    echoEq a b   : Echo[ρ × ρ, Bool]        for ρ ∈ {Num, Str, Word[n]}
+   *)
+  | EchoClose e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TWord n -> TEcho (TWord n, TWord 0)
+    | t -> type_error "echoClose requires Word[n], got %s" (pp_ty t)
+    end
+
+  | Lower e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TEcho (_, t) -> t
+    | t -> type_error "lower requires Echo[_, _], got %s" (pp_ty t)
+    end
+
+  | Residue e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TEcho (r, _) -> r
+    | t -> type_error "residue requires Echo[_, _], got %s" (pp_ty t)
+    end
+
+  | Pair (e1, e2) ->
+    let t1 = infer_expr gamma sigma e1 in
+    let t2 = infer_expr gamma sigma e2 in
+    TProd (t1, t2)
+
+  | Fst e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TProd (a, _) -> a
+    | t -> type_error "fst requires a product, got %s" (pp_ty t)
+    end
+
+  | Snd e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TProd (_, b) -> b
+    | t -> type_error "snd requires a product, got %s" (pp_ty t)
+    end
+
+  | EchoAdd (e1, e2) ->
+    begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with
+    | TNum, TNum -> TEcho (TProd (TNum, TNum), TNum)
+    | t1, t2 -> type_error "echoAdd requires Num, Num, got %s, %s" (pp_ty t1) (pp_ty t2)
+    end
+
+  | EchoEq (e1, e2) ->
+    begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with
+    | TNum, TNum -> TEcho (TProd (TNum, TNum), TBool)
+    | TStr, TStr -> TEcho (TProd (TStr, TStr), TBool)
+    | TWord n, TWord m when n = m -> TEcho (TProd (TWord n, TWord n), TBool)
+    | t1, t2 ->
+      type_error "echoEq requires matching Num/Str/Word[n] operands, got %s, %s"
+        (pp_ty t1) (pp_ty t2)
+    end
+
 (** Infer the type of a binary operation given operand types.
  *  Implements rules from sections 3.4, 3.5, 3.6.
  *)