Engine fixes

bugs/README.md

@@ -0,0 +1,96 @@
+# Fixed: induction over computational goals (symbolic-fixpoint reduction)
+
+The three examples here exercise induction over a goal stated with a `Fixpoint`.
+Two of them (`segfault_apply_fixpoint_motive.me`, `segfault_exact_eliminator_fixpoint.me`)
+used to crash the engine with SIGSEGV (exit 139); the third
+(`note_clean_conversion_failure.me`) used to fail cleanly with a type error. **All
+three now run to completion** (exit 0). They are kept as minimal reproducers and
+regression notes.
+
+All involve the same shape: an induction principle whose motive applies a fixpoint
+(`add`) to a *symbolic* recursive argument, so type-checking the step case must
+convert `add (S n) O` to `S (add n O)` with `n` a variable.
+
+Run them with:
+
+```bash
+./build/mengine -q bugs/segfault_apply_fixpoint_motive.me      # exit 0
+./build/mengine -q bugs/segfault_exact_eliminator_fixpoint.me  # exit 0
+./build/mengine -q bugs/note_clean_conversion_failure.me       # exit 0
+```
+
+A complete worked proof of `forall n, add n O = n` by induction now lives in
+`examples/computational_eliminator.me` as permanent regression coverage.
+
+**Follow-on (stdlib-benchmark branch):** the reproducers here use `apply`/`exact`
+of the eliminator with `f_equal`-style step cases.  The standard stdlib idiom —
+`rewrite` on the induction hypothesis, including a *quantified* IH whose type is
+the eliminator's beta-redex `(motive) n` — also works now; see
+`examples/computational_induction_rewrite.me` (`add_succ_r`, `add_comm`) and the
+`Nat` module of `benchmarks/stdlib/`.  The extra fixes that idiom needed are
+listed in `benchmarks/stdlib/README.md` (symbolic-fixpoint reductions stay
+constant-headed; the rewrite path whnf-normalizes a redex-typed IH; the
+eliminator index hole is recorded during `fill_hole`).
+
+## Root cause
+
+The shared root cause was non-termination when a fixpoint is unfolded on a
+*symbolic* (variable) recursive argument. Three issues conspired:
+
+1. **Unconditional fix reduction.** `conversion_whnf` / `normalize_whnf` / `cbv`
+   reduced a fixpoint application regardless of its decreasing argument. With `n`
+   a variable, `add n O` unfolded to `match n with O => O | S p => S (add p O)`;
+   `conversion_derivable` then recursed into the `S` branch (`add p O`), which
+   unfolded again, forever — a stack overflow / SIGSEGV in the eliminator paths.
+
+2. **A fixpoint constant was delta-reducible to its eta-expanded lambda form.**
+   `Fixpoint add …` registered the recursive variable's body as
+   `λn. λm. body`, so `add` unfolded unconditionally via delta+beta and a fix
+   node never actually appeared during reduction — the guard in (3) had nothing to
+   bite on.
+
+3. **`fix_reduce` captured shared binders.** It substituted the fix node inline
+   for the recursive variable, but the fix shares its argument binders with the
+   body, so re-wrapping them in lambdas double-bound those variables.
+
+## The fix
+
+- `src/kernel/fix_reduction.c` adds `fix_reduce_app`, the guarded fix rule: an
+  application whose head is a fix reduces only once its decreasing argument is in
+  constructor head normal form. `conversion_whnf`, `normalize_whnf`, and `cbv`
+  call it instead of reducing fixpoints unconditionally; a bare fix is now a
+  value. So `add n O` (symbolic `n`) stays stuck and conversion compares it
+  structurally — terminating.
+
+- `src/kernel/expression.c` registers the **fix node itself** as the recursive
+  variable's definitional body (not the eta-expanded lambda). Unfolding the
+  constant now yields a fix node, so the guard governs it. Recursive calls inside
+  the body resolve through the recursive variable (via delta), so `fix_reduce`
+  no longer substitutes inline — it just strips the fix to its lambda abstraction,
+  avoiding the binder capture in (3).
+
+- `src/commandlanguage/command_exec.c` makes the `Definition` command accept a
+  declared type that is *convertible* (not merely structurally congruent) to the
+  inferred type, so computational types such as `add O O = O` are accepted.
+
+All 431 kernel tests and every `examples/*.me` still pass.
+
+## Previously fixed on this branch (related, but distinct)
+
+Two adjacent crashes/limitations were fixed earlier to unblock the Rocq-stdlib
+benchmark (`benchmarks/stdlib/`); they are independent of the symbolic-fixpoint
+crash above:
+
+1. **`cbv` did not reduce applied fixpoints.** `_normalize_cbv` only tried beta
+   on an application spine, so `cbv`/`Eval` left `add (S O) O` stuck even though
+   the conversion checker could reduce it. `src/kernel/normalize.c` now unfolds
+   `(fix …) arg` in the APP case, mirroring `normalize_whnf`.
+
+2. **GC double-free on *ground* computational eliminators.** Type-checking a
+   fully ground eliminator whose motive needs reduction (e.g. `destruct b` on
+   `negb (negb b) = b`) produced a correct proof term but crashed at shutdown:
+   `MatchBranch` arrays are shared by pointer across arena nodes (normalize/
+   conversion rebuild a match with a new scrutinee but reuse its branches), and
+   `expression_gc_shutdown` freed them per-node. It now frees each shared
+   allocation exactly once (`src/kernel/expression.c`). This is shutdown-only
+   memory hygiene and cannot affect proof soundness.

bugs/note_clean_conversion_failure.me

@@ -0,0 +1,17 @@
+(* FIXED (now exit 0). This used to fail cleanly (exit 1) with a type error.
+
+   It showed the underlying limitation behind the two segfaults: a Fixpoint applied
+   to a constructor-headed *symbolic* argument, `add (S n) O`, must reduce to
+   `S (add n O)` with `n` a variable. The `Definition` command also now accepts a
+   declared type convertible (not merely structurally congruent) to the inferred
+   one, so this is checked by reduction; see bugs/README.md.
+
+   Run: ./build/mengine -q bugs/note_clean_conversion_failure.me *)
+
+Inductive nat : Type := | O : nat | S : forall (_: nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+Definition step_conv : forall (n : nat), eq nat (add (S n) O) (S (add n O)) :=
+  fun (n : nat) => eq_refl nat (S (add n O)).

bugs/note_dangling_options_pointer.md

@@ -0,0 +1,90 @@
+# Fixed: dangling `MEngineOptions *` (use-after-return under ASan)
+
+**Status:** **fixed** — `mengine_runtime_new` now owns a private copy of the
+options (`src/runtime/runtime.c`).  Discovered while validating the
+parametric-list kernel fixes under AddressSanitizer; pre-existing and unrelated to
+those fixes.  Kept as a note because the symptom is subtle (benign without ASan)
+and the by-reference API was a footgun.
+
+## Symptom
+
+`make check` built with AddressSanitizer aborts partway through the integration
+suite:
+
+```
+==…==ERROR: AddressSanitizer: stack-use-after-return on address 0x…
+    #0 debug_print_token        src/common/lexer.c:48
+    #1 lexer_next_token         src/common/lexer.c:254
+    #2 parser_init              src/common/parser_base.c:12
+    #3 mengine_runtime_exec_string  src/runtime/runtime.c:127
+    #4 run_ok                   tests/engine/test_integration.c:14
+    #5 test_axiom_and_check     tests/engine/test_integration.c:30
+  …
+  #0 …                          tests/engine/test_integration.c:5   (the freed frame)
+```
+
+Reproduce (no clang needed — gcc has ASan too):
+
+```bash
+make clean
+make CC=gcc CFLAGS="-Wall -Wextra -O0 -g -I. -fsanitize=address -fno-omit-frame-pointer" \
+         LDFLAGS="-fsanitize=address" check
+```
+
+The **default (non-ASan) build is unaffected** — all 431 tests pass — because the
+freed stack slot still happens to hold the old option bytes, so the reads return
+plausible values.  It is a genuine use-after-return, just a normally-benign one.
+
+## Root cause
+
+`mengine_runtime_new` **borrows** its options by pointer rather than copying them:
+
+```c
+// src/runtime/runtime.c
+MEngineRuntime *mengine_runtime_new(MEngineOptions *options) {
+    …
+    rt->options = options;   // stores the caller's pointer, no copy
+    …
+}
+```
+
+The runtime then keeps reading through that pointer for the rest of its life
+(`runtime.c:124` `lexer_init(&lx, source, rt->options)` → `lexer_next_token` →
+`debug_print_token`, which dereferences `lx->options->debug` at `lexer.c:48`).
+
+The integration-test helper hands it a pointer to a **stack local** and then
+returns:
+
+```c
+// tests/engine/test_integration.c
+static MEngineRuntime *make_rt(void) {
+    MEngineOptions opts = {0};        // lives only in this frame
+    opts.quiet = true;
+    return mengine_runtime_new(&opts);  // runtime keeps &opts after make_rt returns
+}
+```
+
+When `make_rt` returns, `opts` is gone, but `rt->options` still points at that
+reclaimed frame.  The next lex/parse dereferences it → stack-use-after-return.
+
+`src/main.c` avoids the trap only by luck of lifetime: its options struct lives in
+`main`'s frame, which outlives the runtime, so the borrowed pointer never dangles.
+
+## The fix
+
+Option 1 (own the options) was taken: `mengine_runtime_new` allocates
+`rt->options = malloc(sizeof(MEngineOptions))` and copies the caller's struct into
+it (`*rt->options = *options`), and `mengine_runtime_free` frees it.  This removes
+the lifetime footgun for every caller — the runtime no longer depends on the
+caller keeping the options struct alive.  The transient mutations through
+`rt->options` (the `quiet` toggle while loading the prelude, `execution_type`)
+were already internal to the runtime, so copying does not change observable
+behaviour; `main.c` passes options by value and never reads them back.
+
+The alternative (give the test's options a lifetime ≥ the runtime) was rejected as
+narrower — it would have left the by-reference API as a trap for the next caller.
+
+Verified: `make check` built with AddressSanitizer now runs to completion (431/431,
+no `stack-use-after-return`).  No `.me` reproducer — this is a C-level lifetime bug
+in the runtime, not a kernel or proof-checking bug, and it cannot affect proof
+soundness.

bugs/segfault_apply_fixpoint_motive.me

@@ -0,0 +1,18 @@
+(* FIXED (now exit 0). This used to SIGSEGV (exit 139).
+
+   Applying an induction principle whose motive mentions a Fixpoint crashed the
+   `apply` tactic while it unified the principle with the goal and built the
+   subgoals — the natural route an induction proof of `add n O = n` takes. The
+   guarded fix rule (src/kernel/fix_reduction.c) now keeps the conversion
+   terminating; see bugs/README.md.
+
+   Run: ./build/mengine -q bugs/segfault_apply_fixpoint_motive.me *)
+
+Inductive nat : Type := | O : nat | S : forall (_: nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+Theorem add_O_r : forall (n : nat), eq nat (add n O) n.
+intro n.
+apply (nat_ind (fun (k : nat) => eq nat (add k O) k)).

bugs/segfault_exact_eliminator_fixpoint.me

@@ -0,0 +1,20 @@
+(* FIXED (now exit 0). This used to SIGSEGV (exit 139).
+
+   Type-checking a fully explicit eliminator proof term crashed in the step case,
+   where `add (S n) O` must convert to `S (add n O)` under the `n` binder. Fix
+   reduction is now guarded on the decreasing argument being constructor-headed,
+   so `add n O` (symbolic `n`) stays stuck instead of unfolding forever; see
+   bugs/README.md.
+
+   Run: ./build/mengine -q bugs/segfault_exact_eliminator_fixpoint.me *)
+
+Inductive nat : Type := | O : nat | S : forall (_: nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+Axiom f_equal_S : forall (a : nat), forall (b : nat), forall (_: eq nat a b),
+  eq nat (S a) (S b).
+
+Check (nat_ind (fun (k : nat) => eq nat (add k O) k) (eq_refl nat O)
+        (fun (n : nat) => fun (ih : eq nat (add n O) n) => f_equal_S (add n O) n ih)).

examples/computational_eliminator.me

@@ -0,0 +1,54 @@
+(* computational_eliminator.me
+
+   Regression coverage for two kernel fixes made for the Rocq-stdlib benchmark
+   (benchmarks/stdlib/).  Both must hold for this file to run to completion:
+
+   1. `cbv` reduces an *applied* fixpoint/definition.  Before the fix
+      `_normalize_cbv` only tried beta on an application spine, so `cbv` left
+      `negb (negb true)` and `add (S O) O` stuck.  Here each case below is closed
+      by `cbv` followed by the (syntactic) prelude `reflexivity`, which only
+      matches once `cbv` has reduced both sides to the same normal form.
+
+   2. Type-checking a *ground* computational eliminator no longer crashes.
+      `apply (bool_ind motive)` on a goal whose motive applies `negb` used to
+      build a correct proof term but then double-free / SIGSEGV at GC shutdown
+      (shared MatchBranch arrays).  If that regressed, this file would exit 139. *)
+
+Inductive bool : Type := | true : bool | false : bool.
+
+Definition negb : forall (_ : bool), bool :=
+  fun (b : bool) => match b with | true => false | false => true end.
+
+(* Ground computational case analysis via the generated eliminator. *)
+Theorem negb_involutive : forall (b : bool), eq bool (negb (negb b)) b.
+intro b.
+apply (bool_ind (fun (b : bool) => eq bool (negb (negb b)) b)).
+cbv. reflexivity.
+cbv. reflexivity.
+
+Inductive nat : Type := | O : nat | S : forall (n : nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+(* cbv must reduce the applied fixpoint for these to print their normal forms. *)
+Eval cbv in (add (S O) O).
+Eval cbv in (add (S (S O)) (S (S O))).
+
+(* Induction over a goal stated with a Fixpoint applied to a *symbolic* recursive
+   argument.  Proving this by `nat_ind` used to SIGSEGV (exit 139): type-checking the
+   step case converts `add (S p) O` with `p` a variable, and fix reduction was
+   unconditional, so a fixpoint unfolded forever on its non-constructor recursive
+   argument.  Reduction now fires only once the decreasing argument is
+   constructor-headed (see src/kernel/fix_reduction.c), so `add p O` stays stuck and
+   the conversion terminates.  If that regresses, this proof crashes or fails. *)
+Axiom f_equal_S : forall (a : nat), forall (b : nat), forall (_ : eq nat a b),
+  eq nat (S a) (S b).
+
+Theorem add_O_r : forall (n : nat), eq nat (add n O) n.
+intro n.
+apply (nat_ind (fun (k : nat) => eq nat (add k O) k)).
+cbv. reflexivity.
+intro p.
+intro ih.
+cbv. apply f_equal_S. exact ih.

examples/computational_induction_rewrite.me

@@ -0,0 +1,58 @@
+(* computational_induction_rewrite.me
+
+   Regression coverage for computational induction proved with `rewrite` on a
+   *quantified* induction hypothesis — the idiom the Rocq standard library uses
+   for arithmetic.  Exercises four fixes that must all hold together:
+
+   1. fix_reduction.c / normalize.c: a fixpoint constant stays folded (and so
+      `rewrite`-matchable) when its decreasing argument is symbolic, and fires
+      via fix_reduce_app once it is constructor-headed.  So `simpl` turns
+      `add (S n) m` into `S (add n m)` while leaving the stuck `add n m` headed
+      by the `add` constant rather than a bare fix node.
+   2. unify.c / rewrite_internal.c: `rewrite` reads the equation off an IH whose
+      stored type is the eliminator's beta-redex `(motive) n` by weak-head
+      normalizing it first, and instantiates the IH's `forall`.
+   3. expression.c: such a redex-typed IH can be *applied* (the syntactic-Pi
+      precheck in init_app_expression_wc was removed; _construct_app_type whnfs).
+   4. type_compat.c: the eliminator's index hole (left by a quantified motive) is
+      recorded during fill, instead of lingering as a stray open goal. *)
+
+Inductive nat : Type := | O : nat | S : forall (n : nat), nat.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat :=
+  match n with | O => m | S p => S (add p m) end.
+
+(* simpl/reflexivity/symmetry as the stdlib compat prelude defines them: simpl is
+   full cbv, and reflexivity closes by conversion (so `add O (S m)` and `S m` need
+   not be syntactically equal, only convertible). *)
+Tactic simpl := cbv.
+Tactic reflexivity := match Goal with
+| [ |- (((eq ?A) ?x) ?y) ] => exact ((eq_refl A) x)
+end.
+Tactic symmetry := apply eq_sym.
+
+(* add_succ_r: the IH `IHn : forall m, add n (S m) = S (add n m)` is quantified,
+   and its type is the eliminator's redex `(motive) n`.  `rewrite IHn with eq`
+   must whnf that type, instantiate `m`, and rewrite the stuck `add n (S m)`. *)
+Theorem add_succ_r : forall (n : nat), forall (m : nat),
+  eq nat (add n (S m)) (S (add n m)).
+intro n.
+apply (nat_ind (fun (n : nat) => forall (m : nat),
+  eq nat (add n (S m)) (S (add n m)))).
+simpl. intro m. reflexivity.
+intro n. intro IHn. simpl. intro m. simpl. rewrite IHn with eq. reflexivity.
+
+Theorem add_0_r : forall (n : nat), eq nat (add n O) n.
+intro n.
+apply (nat_ind (fun (n : nat) => eq nat (add n O) n)).
+simpl. reflexivity.
+intro n. intro IHn. simpl. rewrite IHn with eq. reflexivity.
+
+(* add_comm builds on add_succ_r and add_0_r, mixing rewrite/symmetry the way a
+   real stdlib proof does. *)
+Theorem add_comm : forall (n : nat), forall (m : nat), eq nat (add n m) (add m n).
+intro n.
+apply (nat_ind (fun (n : nat) => forall (m : nat), eq nat (add n m) (add m n))).
+simpl. intro m. simpl. symmetry. rewrite add_0_r with eq. reflexivity.
+intro n. intro IHn. simpl. intro m. simpl. rewrite IHn with eq. symmetry.
+rewrite add_succ_r with eq. reflexivity.