fix(corpus): run conformance programs, and correct a second false assertion

compiler/test/test_eval.ml

@@ -205,6 +205,32 @@ let test_reverse () =
     eval (Reverse (BraidLit [sigma 1; sigma 2]))
       = VBraid [rgen 2 (-1); rgen 1 (-1)]);
 
+  (* Reverse is the INVERSE braid: order reversed AND exponents negated.
+     Two separate corpus programs (examples/trefoil.tangle and
+     conformance/valid/v16) asserted that it merely reverses order. Both were
+     mathematically false and both went undetected for want of anything that
+     ran them. These pin the semantics so the misunderstanding cannot return. *)
+  test "reverse is the INVERSE, not just order-reversal" (fun () ->
+    (* reverse(s1 s2) = s2^-1 s1^-1, NOT s2 s1 *)
+    eval (Reverse (BraidLit [sigma 1; sigma 2]))
+      <> VBraid [rgen 2 1; rgen 1 1]);
+
+  test "reverse composed with itself is the identity map" (fun () ->
+    (* (w^-1)^-1 = w — a property that only holds if reverse really inverts. *)
+    let w = BraidLit [sigma 1; sigma 2; sigma_inv 1] in
+    eval (Reverse (Reverse w)) = eval w);
+
+  test "reverse negates writhe (the invariant that disproved the false claims)" (fun () ->
+    match eval (BraidLit [sigma 1; sigma 1; sigma 1]),
+          eval (Reverse (BraidLit [sigma 1; sigma 1; sigma 1])) with
+    | VBraid a, VBraid b -> writhe a = 3 && writhe b = -3
+    | _ -> false);
+
+  test "mirror negates IN PLACE, unlike reverse" (fun () ->
+    (* The contrast that makes the two easy to confuse. *)
+    eval (Mirror (BraidLit [sigma 1; sigma 2]))
+      = VBraid [rgen 1 (-1); rgen 2 (-1)]);
+
   (* Reverse identity is identity *)
   test "Reverse identity" (fun () ->
     eval (Reverse Identity) = VBraid []);

conformance/valid/v16_close_mirror_reverse.tangle

@@ -3,7 +3,18 @@
 
 def trefoil = braid[s1, s1, s1]
 
+# mirror negates each exponent IN PLACE, preserving order.
 assert mirror(trefoil) == braid[s1^-1, s1^-1, s1^-1]
-assert reverse(braid[s1, s2]) == braid[s2, s1]
+
+# reverse reverses the word AND negates each exponent — it yields the INVERSE
+# braid, so reverse(s1 s2) = s2^-1 s1^-1, not s2 s1.
+#
+# This file previously asserted `== braid[s2, s1]`, which is false:
+# writhe(reverse(braid[s1,s2])) = -2 but writhe(braid[s2,s1]) = +2, and writhe
+# is invariant under the braid relations, so they cannot be the same element.
+# The same wrong assumption about `reverse` was also in examples/trefoil.tangle.
+# Neither was caught because nothing ever RAN these programs — the conformance
+# gate only checked that they parsed.
+assert reverse(braid[s1, s2]) == braid[s2^-1, s1^-1]
 
 compute writhe(close(trefoil))

docs/spec/FORMAL-SEMANTICS.md

@@ -57,7 +57,7 @@ e  ::=  x                                    -- variable reference
      |  cap                                  -- cap primitive
      |  cup                                  -- cup primitive
      |  mirror(e)                            -- mirror image
-     |  reverse(e)                           -- reverse word
+     |  reverse(e)                           -- inverse braid (see §Reverse)
      |  simplify(e)                          -- Reidemeister simplification
      |  f(e₁, ..., eₖ)                      -- function application
      |  match e with arm₁ | ... | armₖ end  -- pattern matching
@@ -372,7 +372,22 @@ With explicit strand types (in weave context):
 Γ ⊢ mirror(e) : Word[n]
 ```
 
-**Reverse** — inverts all generators in a word:
+**Reverse** — the INVERSE braid. It reverses the word **and** negates every
+exponent:
+
+```
+reverse(g₁ g₂ … gₙ)  =  gₙ⁻¹ … g₂⁻¹ g₁⁻¹        i.e.  reverse(w) = w⁻¹
+```
+
+So `reverse(braid[s1, s2]) = braid[s2^-1, s1^-1]` — NOT `braid[s2, s1]`.
+
+This is easy to get wrong, and was: both `examples/trefoil.tangle` and
+`conformance/valid/v16_close_mirror_reverse.tangle` asserted that `reverse`
+merely reverses order, which is false. `writhe` disproves it — writhe is the
+exponent sum and is invariant under the braid relations, so `w` and `w⁻¹`
+differ in writhe by twice the writhe of `w` and cannot be equal unless the
+writhe is 0. Contrast **mirror**, which negates exponents *in place* and
+leaves the order alone.
 
 ```
 Γ ⊢ e : Word[n]

scripts/check-corpus.sh

@@ -73,6 +73,18 @@ CONFORMANCE_KNOWN_UNPARSED=(
   v11_add_block.tangle
 )
 
+# conformance/valid programs that PARSE but do not yet TYPECHECK+EVALUATE.
+#   v09_twist : `(~a)` — twisting a named strand inside a weave. spec/grammar.ebnf
+#               says "In weave context: (~a) twists named strand a", but
+#               infer_expr rejects any strand name used as an expression, so the
+#               construct is specified and unimplemented. Tracked in #96.
+#   v11       : does not parse at all (see above); listed here too so the eval
+#               loop does not double-report it.
+CONFORMANCE_KNOWN_UNRUNNABLE=(
+  v09_twist.tangle
+  v11_add_block.tangle
+)
+
 fail=0
 note() { printf '  %-34s %s\n' "$1" "$2"; }
 
@@ -149,6 +161,36 @@ for f in "${ROOT}"/conformance/valid/*.tangle; do
     fi
   fi
 done
+# conformance/valid must also RUN, not merely parse.
+# Parsing alone was never enough: `examples/trefoil.tangle` and
+# `conformance/valid/v16_close_mirror_reverse.tangle` BOTH asserted
+# `reverse(w) == <w with order reversed>`, forgetting that `reverse` also
+# negates exponents and so yields the inverse braid. Both were mathematically
+# false — disproved by writhe, which is invariant under the braid relations —
+# and both sat undetected because the gate only checked that they parsed.
+echo "== conformance: valid programs must EVALUATE =="
+for f in "${ROOT}"/conformance/valid/*.tangle; do
+  n="$(basename "$f")"
+  if "${BIN}" --eval "$f" >/dev/null 2>&1; then
+    if in_list "$n" "${CONFORMANCE_KNOWN_UNRUNNABLE[@]}"; then
+      note "valid/$n" "NOW RUNS"
+      echo "::error::conformance/valid/${n} now evaluates — drop it from CONFORMANCE_KNOWN_UNRUNNABLE."
+      fail=1
+    else
+      note "valid/$n" "evaluates ok"
+    fi
+  else
+    if in_list "$n" "${CONFORMANCE_KNOWN_UNRUNNABLE[@]}"; then
+      note "valid/$n" "still not runnable (expected)"
+    else
+      note "valid/$n" "EVAL FAILED"
+      echo "::error::conformance/valid/${n} parses but does not evaluate:"
+      "${BIN}" --eval "$f" 2>&1 | head -3
+      fail=1
+    fi
+  fi
+done
+
 for f in "${ROOT}"/conformance/invalid/*.tangle; do
   n="$(basename "$f")"
   if "${BIN}" "$f" >/dev/null 2>&1; then