From 069dae9e59bca563b6a3a6e0fa8b3c7f5122ef26 Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sat, 27 Jun 2026 21:07:58 +0000 Subject: [PATCH 1/8] Generate induction principles with induction hypotheses The auto-generated _ind was a dependent case-analysis principle: each constructor case was `forall args, P (c args)`, with no hypothesis for recursive arguments. That makes induction impossible (apply _ind gives no IH to work with). Add an induction hypothesis for every first-order recursive constructor argument, so e.g. nat_ind's step case becomes `forall (n:nat), P n -> P (S n)` and tree_ind's becomes `forall l r, P l -> P r -> P (node l r)`. Non-recursive arguments and non-recursive types (bool) are unaffected. Scope: non-parametric inductives only. Parametric `_ind` generation is still skipped for a separate, pre-existing reason (constructor types use fresh per-constructor parameter copies that don't match the builder's parameter variables) and is left for a follow-up. Adds a semantic regression test: a full abstract induction proof that only type-checks when the IH is present. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- src/commandlanguage/command_exec.c | 66 ++++++++++++++++++++++++++---- tests/engine/test_integration.c | 18 ++++++++ 2 files changed, 76 insertions(+), 8 deletions(-) diff --git a/src/commandlanguage/command_exec.c b/src/commandlanguage/command_exec.c index edbb9ed8..34094d11 100644 --- a/src/commandlanguage/command_exec.c +++ b/src/commandlanguage/command_exec.c @@ -261,9 +261,9 @@ static int _handle_print_command(MEngineRuntime *rt, PrintCmd *print_cmd) { } static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type, - Expression *motive_var, Expression **param_vars, - size_t param_count, size_t index_count, - Context *elim_ctx); + Expression *motive_var, Expression *ind_var, + Expression **param_vars, size_t param_count, + size_t index_count, Context *elim_ctx); static Expression *_build_motive_type(Expression *ind_var, Expression **param_vars, size_t param_count, Context *ctx, @@ -365,8 +365,8 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres Expression *ctor_type = kernel_expr_type(ctor_expr); Expression *case_type = - _build_constructor_case_type(ctor_expr, ctor_type, motive_var, param_vars, param_count, - index_count, case_contexts[i]); + _build_constructor_case_type(ctor_expr, ctor_type, motive_var, ind_var, param_vars, + param_count, index_count, case_contexts[i]); if (!case_type) { fprintf(stderr, ERROR "Failed to build case type for %s\n" CRESET, ctor->name); @@ -500,10 +500,47 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres return result; } +// Build the induction hypothesis for a single constructor argument, or NULL when +// the argument is not a recursive occurrence of the inductive being defined. +// +// An argument `arg : I p0..p_{m-1} x0..x_{k-1}` (the inductive applied to its +// parameters and indices) yields the hypothesis `P x0..x_{k-1} arg` — the motive +// applied to the argument's own indices and then the argument itself. This is +// what turns the generated principle from plain case analysis into induction. +// +// Only first-order recursion is recognised; a higher-order argument such as +// `(nat -> I)` is treated as non-recursive and gets no hypothesis. +static Expression *_build_recursive_arg_hypothesis(Expression *arg_var, Expression *arg_type, + Expression *ind_var, Expression *motive_var, + size_t param_count, size_t index_count, + Context *ctx) { + if (!kernel_expr_congruent(kernel_expr_head(arg_type), ind_var)) { + return NULL; + } + + Expression *hypothesis = motive_var; + if (index_count > 0) { + // arg_type is the spine `I p0..p_{m-1} x0..x_{k-1}`; the indices are the + // arguments past the parameters. + DoublyLinkedList *spine = dll_create(); + Expression *head = arg_type; + while (kernel_app_func(head) != NULL) { + dll_insert_at_head(spine, dll_new_node(kernel_app_arg(head))); + head = kernel_app_func(head); + } + for (size_t i = 0; i < index_count; i++) { + Expression *index = (Expression *)dll_at(spine, param_count + i)->data; + hypothesis = kernel_app_create(hypothesis, index, ctx); + } + dll_destroy(spine); + } + return kernel_app_create(hypothesis, arg_var, ctx); +} + static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type, - Expression *motive_var, Expression **param_vars, - size_t param_count, size_t index_count, - Context *elim_ctx) { + Expression *motive_var, Expression *ind_var, + Expression **param_vars, size_t param_count, + size_t index_count, Context *elim_ctx) { Expression *core_type = ctor_type; for (size_t i = 0; i < param_count; i++) { if (kernel_forall_var(core_type) != NULL) { @@ -615,6 +652,19 @@ static Expression *_build_constructor_case_type(Expression *ctor_expr, Expressio free(ctor_indices); } Expression *case_type = case_result; + + // Wrap the conclusion with an induction hypothesis per recursive argument, + // giving `IH_0 -> .. -> IH_k -> P (c args)`. These sit inside the argument + // binders below because each hypothesis mentions its argument. + for (size_t i = arg_count; i > 0; i--) { + Expression *arg_type = (Expression *)dll_at(arg_types, i - 1)->data; + Expression *hypothesis = _build_recursive_arg_hypothesis( + arg_vars[i - 1], arg_type, ind_var, motive_var, param_count, index_count, case_ctx); + if (hypothesis) { + case_type = kernel_arrow_create(hypothesis, case_type, case_ctx); + } + } + for (size_t i = arg_count; i > 0; i--) { case_type = kernel_forall_create(arg_vars[i - 1], case_type); } diff --git a/tests/engine/test_integration.c b/tests/engine/test_integration.c index f2e77ee3..3c1229ce 100644 --- a/tests/engine/test_integration.c +++ b/tests/engine/test_integration.c @@ -51,6 +51,23 @@ static void test_inductive_nat(void) { "Check nat_ind.\n"); } +/* The generated induction principle must carry an induction hypothesis for each + * recursive argument (not just case analysis). This proof only type-checks if + * `case_S` is `forall n, P n -> P (S n)`: `step` would not match a hypothesis- + * free `forall n, P (S n)`. */ +static void test_induction_principle_has_ih(void) { + run_ok("induction principle carries the induction hypothesis", + "Inductive nat : Type := | O : nat | S : forall (_: nat), nat.\n" + "Axiom P : forall (_: nat), Prop.\n" + "Axiom base : P O.\n" + "Axiom step : forall (n : nat), forall (_: P n), P (S n).\n" + "Theorem allP : forall (n : nat), P n.\n" + "intro n.\n" + "apply (nat_ind P).\n" + "exact base.\n" + "exact step.\n"); +} + static void test_inductive_match_pred(void) { run_ok("match expression: predecessor", "Inductive nat : Type := | O : nat | S : forall (_: nat), nat.\n" @@ -390,6 +407,7 @@ void run_integration_tests(void) { test_axiom_and_check(); test_definition(); test_inductive_nat(); + test_induction_principle_has_ih(); test_inductive_match_pred(); test_inductive_bool(); test_fixpoint_add(); From 2b696863f9f9ee53b61a84147718985c40c95f05 Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sat, 27 Jun 2026 21:33:55 +0000 Subject: [PATCH 2/8] Generate induction principles for parametric inductives Previously the generator skipped the induction principle entirely for parametric inductives (param_count > 0), because the principle was built with the inductive's own param_vars while each constructor's stored type used fresh per-constructor parameter copies in a divergent context branch. Build the principle with its own parameter set, bound once after ind_var, and derive each constructor case by *applying* the constructor to those parameters (letting the kernel substitute them) rather than textually stripping parameter binders. Argument variables are created fresh and the remaining telescope is recomputed from the partial application after each one, so argument and return types are rebased onto our variables and stay valid even when a type mentions an earlier argument or a parameter (e.g. cons's tail of type `list A`). This unifies the parametric and non-parametric paths. list_ind now matches Coq: forall A P, P (nil A) -> (forall a l, P l -> P (cons A a l)) -> forall l, P l Adds a regression test that proves an abstract list induction (only type-checks if list_ind has the IH-bearing shape). Also adds bugs/ with two minimal reproducers (plus a clean-failure contrast) for pre-existing crashes when inducting over goals stated with a Fixpoint: `apply` with a fixpoint-mentioning motive, and type-checking an explicit eliminator term whose step case must reduce `add (S n) O`. These are documented, not fixed (Tier 2: symbolic iota/fix reduction). Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- bugs/README.md | 42 +++++ bugs/note_clean_conversion_failure.me | 17 +++ bugs/segfault_apply_fixpoint_motive.me | 16 ++ bugs/segfault_exact_eliminator_fixpoint.me | 19 +++ src/commandlanguage/command_exec.c | 169 +++++++++------------ tests/engine/test_integration.c | 21 +++ 6 files changed, 191 insertions(+), 93 deletions(-) create mode 100644 bugs/README.md create mode 100644 bugs/note_clean_conversion_failure.me create mode 100644 bugs/segfault_apply_fixpoint_motive.me create mode 100644 bugs/segfault_exact_eliminator_fixpoint.me diff --git a/bugs/README.md b/bugs/README.md new file mode 100644 index 00000000..1ce388a2 --- /dev/null +++ b/bugs/README.md @@ -0,0 +1,42 @@ +# Known segfaults: induction over computational goals + +These two minimal examples crash the engine (SIGSEGV). They are **pre-existing** +kernel issues, not caused by the induction-principle generator change on this +branch — that change only fixed the *type* of the generated `_ind`. They surface +now because a correct, IH-bearing induction principle can finally be applied to a +goal stated with a `Fixpoint`. + +Both involve the same shape: an induction principle whose motive applies a +fixpoint (`add`) to a constructor-headed *symbolic* argument, so type-checking the +step case must reduce/convert `add (S n) O` with `n` a variable. (MEngine's +reduction is ground-only — `add (S n) O` does not reduce when `n` is symbolic; see +`bugs/note_clean_conversion_failure.me`, which fails *cleanly* with exit 1 rather +than crashing.) The crash is specific to the eliminator-*application* paths below. + +Run them with: + +```bash +./build/mengine -q bugs/segfault_apply_fixpoint_motive.me # exit 139 +./build/mengine -q bugs/segfault_exact_eliminator_fixpoint.me # exit 139 +``` + +## 1. `segfault_apply_fixpoint_motive.me` — the `apply` / unifier path + +`apply (nat_ind )`, where the motive mentions the `add` fixpoint, crashes +while the tactic unifies the principle against the goal and builds the subgoals. +This is the direct route a real induction proof would take, so it currently blocks +proving e.g. `forall n, add n O = n` by induction. + +## 2. `segfault_exact_eliminator_fixpoint.me` — the kernel type-check path + +`Check` (equivalently `exact`) of a fully explicit eliminator proof term crashes +while type-checking the step case, where `add (S n) O` must be converted to +`S (add n O)` under the `n` binder. This isolates the crash to the kernel's +handling of the eliminator application itself: the bare conversion alone does not +crash (it fails cleanly), but wrapping it in the eliminator application does. + +## Not fixed here + +Per the branch's scope, these crashes are documented, not fixed. Fixing them is +the "Tier 2" work: make iota/fix reduction fire on symbolic constructor-headed +arguments, and harden the eliminator application / conversion path against it. diff --git a/bugs/note_clean_conversion_failure.me b/bugs/note_clean_conversion_failure.me new file mode 100644 index 00000000..b30256dc --- /dev/null +++ b/bugs/note_clean_conversion_failure.me @@ -0,0 +1,17 @@ +(* NOT a crash: this fails cleanly (exit 1) with a type error. + + It shows the underlying limitation behind the two segfaults: MEngine's + reduction is ground-only, so `add (S n) O` does not reduce to `S (add n O)` + when `n` is a variable, and the conversion is rejected. On its own this is a + clean rejection; only the eliminator-application paths (the two segfault_*.me + files) turn it into a crash. + + 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)). diff --git a/bugs/segfault_apply_fixpoint_motive.me b/bugs/segfault_apply_fixpoint_motive.me new file mode 100644 index 00000000..f91cfbc4 --- /dev/null +++ b/bugs/segfault_apply_fixpoint_motive.me @@ -0,0 +1,16 @@ +(* SEGFAULT (exit 139). Pre-existing kernel crash, not fixed on this branch. + + Applying an induction principle whose motive mentions a Fixpoint crashes the + `apply` tactic while it unifies the principle with the goal and builds the + subgoals. This is the natural route an induction proof of `add n O = n` takes. + + 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)). diff --git a/bugs/segfault_exact_eliminator_fixpoint.me b/bugs/segfault_exact_eliminator_fixpoint.me new file mode 100644 index 00000000..9af25c23 --- /dev/null +++ b/bugs/segfault_exact_eliminator_fixpoint.me @@ -0,0 +1,19 @@ +(* SEGFAULT (exit 139). Pre-existing kernel crash, not fixed on this branch. + + Type-checking a fully explicit eliminator proof term crashes in the step case, + where `add (S n) O` must convert to `S (add n O)` under the `n` binder. The + bare conversion on its own fails *cleanly* (see note_clean_conversion_failure.me); + only wrapping it in the eliminator application crashes. + + 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)). diff --git a/src/commandlanguage/command_exec.c b/src/commandlanguage/command_exec.c index 34094d11..592a0970 100644 --- a/src/commandlanguage/command_exec.c +++ b/src/commandlanguage/command_exec.c @@ -260,10 +260,10 @@ static int _handle_print_command(MEngineRuntime *rt, PrintCmd *print_cmd) { return 0; } -static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type, - Expression *motive_var, Expression *ind_var, - Expression **param_vars, size_t param_count, - size_t index_count, Context *elim_ctx); +static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *motive_var, + Expression *ind_var, Expression **param_vars, + size_t param_count, size_t index_count, + Context *elim_ctx); static Expression *_build_motive_type(Expression *ind_var, Expression **param_vars, size_t param_count, Context *ctx, @@ -341,10 +341,23 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres Context **contexts) { Context *elim_ctx = contexts[param_count]; + // The inductive's own parameter variables (param_vars) were built in a context + // branch created *before* ind_var, so they are not in scope where the principle + // lives. Re-bind one shared set of parameters here, after ind_var; the motive, + // every constructor case, and the conclusion all refer to these. Parameter + // types are taken verbatim, which assumes a parameter's type does not mention + // earlier parameters (the usual case, e.g. `(A : Type)`). + Expression **params = malloc(param_count * sizeof(Expression *)); + for (size_t i = 0; i < param_count; i++) { + params[i] = kernel_var_create(kernel_var_name(param_vars[i]), + kernel_expr_type(param_vars[i]), elim_ctx); + elim_ctx = params[i]; + } + Expression **index_vars = NULL; size_t index_count = 0; Expression *motive_type = - _build_motive_type(ind_var, param_vars, param_count, elim_ctx, &index_vars, &index_count); + _build_motive_type(ind_var, params, param_count, elim_ctx, &index_vars, &index_count); Expression *motive_var = kernel_var_create("P", motive_type, elim_ctx); elim_ctx = motive_var; @@ -358,18 +371,19 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres Expression *ctor_expr = kernel_context_lookup(elim_ctx, ctor->name); if (!ctor_expr) { fprintf(stderr, ERROR "Constructor %s not found in context\n" CRESET, ctor->name); + free(params); free(case_vars); free(case_contexts); return NULL; } - Expression *ctor_type = kernel_expr_type(ctor_expr); Expression *case_type = - _build_constructor_case_type(ctor_expr, ctor_type, motive_var, ind_var, param_vars, - param_count, index_count, case_contexts[i]); + _build_constructor_case_type(ctor_expr, motive_var, ind_var, params, param_count, + index_count, case_contexts[i]); if (!case_type) { fprintf(stderr, ERROR "Failed to build case type for %s\n" CRESET, ctor->name); + free(params); free(case_vars); free(case_contexts); return NULL; @@ -380,6 +394,7 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres case_vars[i] = kernel_var_create(case_name, case_type, case_contexts[i]); if (!case_vars[i]) { fprintf(stderr, ERROR "Failed to create case variable for %s\n" CRESET, ctor->name); + free(params); free(case_vars); free(case_contexts); return NULL; @@ -407,13 +422,14 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres // Build (ind params concl_index_0 ... concl_index_n) Expression *ind_applied = ind_var; for (size_t i = 0; i < param_count; i++) { - ind_applied = kernel_app_create(ind_applied, param_vars[i], final_ctx); + ind_applied = kernel_app_create(ind_applied, params[i], final_ctx); if (!ind_applied) { fprintf(stderr, ERROR "Failed to apply parameter %zu to inductive in " "conclusion\n" CRESET, i); + free(params); free(case_vars); free(case_contexts); if (index_vars) { @@ -441,6 +457,7 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres target_applied = kernel_app_create(target_applied, target_var, target_ctx); if (!target_applied) { fprintf(stderr, ERROR "Failed to apply motive to target\n" CRESET); + free(params); free(case_vars); free(case_contexts); if (index_vars) { @@ -468,6 +485,7 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres result = kernel_forall_create(case_vars[i - 1], result); if (!result) { fprintf(stderr, ERROR "Failed to wrap with constructor case %zu\n" CRESET, i - 1); + free(params); free(case_vars); free(case_contexts); return NULL; @@ -477,21 +495,24 @@ static Expression *_build_induction_principle_type(InductiveCmd *ind_cmd, Expres result = kernel_forall_create(motive_var, result); if (!result) { fprintf(stderr, ERROR "Failed to wrap with motive P\n" CRESET); + free(params); free(case_vars); free(case_contexts); return NULL; } for (size_t i = param_count; i > 0; i--) { - result = kernel_forall_create(param_vars[i - 1], result); + result = kernel_forall_create(params[i - 1], result); if (!result) { fprintf(stderr, ERROR "Failed to wrap with parameter %zu\n" CRESET, i - 1); + free(params); free(case_vars); free(case_contexts); return NULL; } } + free(params); free(case_vars); free(case_contexts); if (index_vars) { @@ -537,140 +558,110 @@ static Expression *_build_recursive_arg_hypothesis(Expression *arg_var, Expressi return kernel_app_create(hypothesis, arg_var, ctx); } -static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *ctor_type, - Expression *motive_var, Expression *ind_var, - Expression **param_vars, size_t param_count, - size_t index_count, Context *elim_ctx) { - Expression *core_type = ctor_type; - for (size_t i = 0; i < param_count; i++) { - if (kernel_forall_var(core_type) != NULL) { - core_type = kernel_forall_body(core_type); - } - } - - DoublyLinkedList *arg_types = dll_create(); - Expression *current = core_type; - while (kernel_forall_var(current) != NULL) { - Expression *arg_type = kernel_expr_type(kernel_forall_var(current)); - dll_insert_at_tail(arg_types, dll_new_node(arg_type)); - current = kernel_forall_body(current); - } - +static Expression *_build_constructor_case_type(Expression *ctor_expr, Expression *motive_var, + Expression *ind_var, Expression **param_vars, + size_t param_count, size_t index_count, + Context *elim_ctx) { + // Instantiate the constructor at the principle's parameters by applying it, + // rather than stripping parameter binders from its type textually. The kernel + // substitutes the parameters into the resulting argument and return types, so + // everything below is expressed in terms of param_vars and valid in elim_ctx. Expression *ctor_app = ctor_expr; for (size_t i = 0; i < param_count; i++) { ctor_app = kernel_app_create(ctor_app, param_vars[i], elim_ctx); if (!ctor_app) { fprintf(stderr, ERROR "Failed to apply parameter %zu to constructor\n" CRESET, i); - dll_destroy(arg_types); return NULL; } } - size_t arg_count = dll_len(arg_types); - Expression **arg_vars = malloc(arg_count * sizeof(Expression *)); + // Walk the parameter-instantiated constructor telescope, creating a fresh + // variable for each argument. After applying each fresh argument we recompute + // the remaining type from the partial application, so the kernel rebases the + // following argument and return types onto our fresh variables — keeping them + // valid here even when a type mentions an earlier argument or a parameter + // (e.g. cons's tail of type `list A`). + DoublyLinkedList *args = dll_create(); + Expression *current = kernel_expr_type(ctor_app); Context *case_ctx = elim_ctx; - - for (size_t i = 0; i < arg_count; i++) { - Expression *arg_type = (Expression *)dll_at(arg_types, i)->data; + size_t arg_i = 0; + while (kernel_forall_var(current) != NULL) { + Expression *arg_type = kernel_expr_type(kernel_forall_var(current)); char arg_name[32]; - sprintf(arg_name, "arg%zu", i); - - arg_vars[i] = kernel_var_create(arg_name, arg_type, case_ctx); - case_ctx = arg_vars[i]; - ctor_app = kernel_app_create(ctor_app, arg_vars[i], case_ctx); + sprintf(arg_name, "arg%zu", arg_i++); + Expression *arg_var = kernel_var_create(arg_name, arg_type, case_ctx); + dll_insert_at_tail(args, dll_new_node(arg_var)); + case_ctx = arg_var; + ctor_app = kernel_app_create(ctor_app, arg_var, case_ctx); if (!ctor_app) { - fprintf(stderr, ERROR "Failed to apply constructor arg %zu\n" CRESET, i); - dll_destroy(arg_types); - free(arg_vars); + fprintf(stderr, ERROR "Failed to apply constructor argument\n" CRESET); + dll_destroy(args); return NULL; } + current = kernel_expr_type(ctor_app); } + size_t arg_count = dll_len(args); - // Extract indices from constructor return type - // current holds the return type after stripping foralls + // `current` now holds the return type `I params indices`; pull the indices out + // of its application spine (the arguments after the parameters). Expression **ctor_indices = NULL; if (index_count > 0) { ctor_indices = malloc(index_count * sizeof(Expression *)); - - // Parse the return type as a spine of applications - // For eq_refl: (((eq A) x) x) - we want to extract the indices (the - // trailing applications) DoublyLinkedList *spine = dll_create(); Expression *head = current; while (kernel_app_func(head) != NULL) { dll_insert_at_head(spine, dll_new_node(kernel_app_arg(head))); head = kernel_app_func(head); } - - // The spine now has all the arguments. Skip param_count, take - // index_count - size_t total_args = dll_len(spine); - if (total_args < param_count + index_count) { + if (dll_len(spine) < param_count + index_count) { fprintf(stderr, ERROR "Constructor return type has too few arguments\n" CRESET); dll_destroy(spine); - dll_destroy(arg_types); - free(arg_vars); + dll_destroy(args); free(ctor_indices); return NULL; } - - // Extract the indices (skip parameters) for (size_t i = 0; i < index_count; i++) { ctor_indices[i] = (Expression *)dll_at(spine, param_count + i)->data; } - dll_destroy(spine); } - // Apply motive to indices first, then to constructor application + // Conclusion: `P indices (c params args)`, valid in case_ctx (the innermost + // argument, or elim_ctx for a constructor with no arguments). Expression *case_result = motive_var; for (size_t i = 0; i < index_count; i++) { case_result = kernel_app_create(case_result, ctor_indices[i], case_ctx); - if (!case_result) { - fprintf(stderr, ERROR "Failed to apply motive to index %zu\n" CRESET, i); - dll_destroy(arg_types); - free(arg_vars); - if (ctor_indices) { - free(ctor_indices); - } - return NULL; - } } - case_result = kernel_app_create(case_result, ctor_app, case_ctx); + if (ctor_indices) { + free(ctor_indices); + } if (!case_result) { fprintf(stderr, ERROR "Failed to apply motive to constructor application\n" CRESET); - dll_destroy(arg_types); - free(arg_vars); - if (ctor_indices) { - free(ctor_indices); - } + dll_destroy(args); return NULL; } - if (ctor_indices) { - free(ctor_indices); - } Expression *case_type = case_result; // Wrap the conclusion with an induction hypothesis per recursive argument, // giving `IH_0 -> .. -> IH_k -> P (c args)`. These sit inside the argument // binders below because each hypothesis mentions its argument. for (size_t i = arg_count; i > 0; i--) { - Expression *arg_type = (Expression *)dll_at(arg_types, i - 1)->data; + Expression *arg_var = (Expression *)dll_at(args, i - 1)->data; Expression *hypothesis = _build_recursive_arg_hypothesis( - arg_vars[i - 1], arg_type, ind_var, motive_var, param_count, index_count, case_ctx); + arg_var, kernel_expr_type(arg_var), ind_var, motive_var, param_count, index_count, + case_ctx); if (hypothesis) { case_type = kernel_arrow_create(hypothesis, case_type, case_ctx); } } for (size_t i = arg_count; i > 0; i--) { - case_type = kernel_forall_create(arg_vars[i - 1], case_type); + case_type = kernel_forall_create((Expression *)dll_at(args, i - 1)->data, case_type); } - dll_destroy(arg_types); - free(arg_vars); + dll_destroy(args); return case_type; } @@ -842,16 +833,8 @@ static int _handle_inductive_command(MEngineRuntime *rt, InductiveCmd *ind_cmd) char *ind_principle_name = malloc(strlen(name) + 5); sprintf(ind_principle_name, "%s_ind", name); - /* The induction principle builder uses the original param_vars, but - * constructor types now use fresh parameter copies. The resulting case - * types would fail the application type check (fresh_param != original_param). - * Skip the induction principle for parametric inductives; it is not needed - * by the tactics that use parametric types (e.g., sep_list in cancel). */ - Expression *ind_principle_type = NULL; - if (param_count == 0) { - ind_principle_type = - _build_induction_principle_type(ind_cmd, ind_var, param_vars, param_count, contexts); - } + Expression *ind_principle_type = + _build_induction_principle_type(ind_cmd, ind_var, param_vars, param_count, contexts); Expression *ind_principle_var = NULL; if (ind_principle_type) { diff --git a/tests/engine/test_integration.c b/tests/engine/test_integration.c index 3c1229ce..ce513283 100644 --- a/tests/engine/test_integration.c +++ b/tests/engine/test_integration.c @@ -401,6 +401,26 @@ static void test_parametric_list(void) { "Check cons.\n"); } +/* Parametric inductives also get an induction principle (parameters bound once, + * out front), with an induction hypothesis on the recursive argument. This proof + * only type-checks if list_ind has the shape + * forall A P, P (nil A) -> (forall a l, P l -> P (cons A a l)) -> forall l, P l. */ +static void test_parametric_induction_principle(void) { + run_ok("parametric induction principle is usable", + "Inductive list (A : Type) : Type :=\n" + " | nil : list A\n" + " | cons : forall (_: A), forall (_: list A), list A.\n" + "Axiom A : Type.\n" + "Axiom P : forall (_: list A), Prop.\n" + "Axiom base : P (nil A).\n" + "Axiom step : forall (a : A), forall (l : list A), forall (_: P l), P (cons A a l).\n" + "Theorem allL : forall (l : list A), P l.\n" + "intro l.\n" + "apply (list_ind A P).\n" + "exact base.\n" + "exact step.\n"); +} + void run_integration_tests(void) { test_suite_start("Integration Tests"); @@ -408,6 +428,7 @@ void run_integration_tests(void) { test_definition(); test_inductive_nat(); test_induction_principle_has_ih(); + test_parametric_induction_principle(); test_inductive_match_pred(); test_inductive_bool(); test_fixpoint_add(); From 8ffea379f9e5d30d1e081ded62cdc0017d71fe38 Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sun, 28 Jun 2026 04:16:32 +0000 Subject: [PATCH 3/8] Reduce applied fixpoints in cbv; free shared match branches once at GC Two kernel fixes (split out from the original stdlib-benchmark commit, engine side only): - src/kernel/normalize.c: _normalize_cbv now unfolds (fix ...) arg in the APP case, so cbv/Eval actually compute applied fixpoints (add (S O) O -> S O). - src/kernel/expression.c: MatchBranch arrays are shared by pointer across arena nodes (normalize/conversion rebuild a match reusing its branches); GC shutdown now frees each shared allocation exactly once instead of double-freeing. examples/computational_eliminator.me is the regression; bugs/README documents it. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- bugs/README.md | 32 +++++++-- examples/computational_eliminator.me | 36 ++++++++++ src/kernel/expression.c | 98 +++++++++++++++++++++++++--- src/kernel/normalize.c | 16 +++++ 4 files changed, 169 insertions(+), 13 deletions(-) create mode 100644 examples/computational_eliminator.me diff --git a/bugs/README.md b/bugs/README.md index 1ce388a2..12ec8a2f 100644 --- a/bugs/README.md +++ b/bugs/README.md @@ -35,8 +35,32 @@ while type-checking the step case, where `add (S n) O` must be converted to handling of the eliminator application itself: the bare conversion alone does not crash (it fails cleanly), but wrapping it in the eliminator application does. -## Not fixed here +## Still not fixed here (the two reproducers above) -Per the branch's scope, these crashes are documented, not fixed. Fixing them is -the "Tier 2" work: make iota/fix reduction fire on symbolic constructor-headed -arguments, and harden the eliminator application / conversion path against it. +Both reproducers above still crash. Fixing them is the remaining "Tier 2" work: +make iota/fix reduction fire on symbolic constructor-headed arguments, and harden +the eliminator application / conversion path against it. The shared root cause is +non-termination in `conversion_whnf`/`conversion_derivable` when a fixpoint is +unfolded on a symbolic (variable) recursive argument (`is_fix_reducible` is +unconditional), so the standard guard — reduce a fix only when its decreasing +argument is in constructor head normal form — is the proper repair. + +## Fixed on the stdlib-benchmark branch (related, but distinct) + +Two adjacent crashes/limitations *were* fixed to unblock the Rocq-stdlib +benchmark (`benchmarks/stdlib/`); they are independent of the symbolic-fixpoint +crash above and all 431 kernel tests still pass: + +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. diff --git a/examples/computational_eliminator.me b/examples/computational_eliminator.me new file mode 100644 index 00000000..4d64f6c3 --- /dev/null +++ b/examples/computational_eliminator.me @@ -0,0 +1,36 @@ +(* 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))). diff --git a/src/kernel/expression.c b/src/kernel/expression.c index 972e8ffe..9a01c2bf 100644 --- a/src/kernel/expression.c +++ b/src/kernel/expression.c @@ -1,6 +1,7 @@ #include "src/kernel/expression.h" #include +#include #include #include #include @@ -193,8 +194,78 @@ void free_expression_graph(Expression *root) { (void)root; } void free_filled_hole(Expression *hole) { (void)hole; } -// Flat free of a single expression's non-expression heap allocations. -static void gc_free_node(Expression *expr) { +/* Pointer set used at shutdown to free each shared sub-allocation exactly once. + MATCH branch arrays (and their MatchBranch structs / pattern-variable arrays) + and FIX argument arrays are shared by pointer across distinct arena nodes — + e.g. normalize/conversion rebuild a match with a new scrutinee but reuse the + original branches array. A naive per-node free would double-free them. */ +typedef struct { + uintptr_t *slots; + size_t capacity; + size_t count; +} PtrSet; + +static void ptrset_init(PtrSet *set) { + set->capacity = 1024; + set->count = 0; + set->slots = calloc(set->capacity, sizeof(uintptr_t)); +} + +static void ptrset_free(PtrSet *set) { + free(set->slots); + set->slots = NULL; + set->capacity = 0; + set->count = 0; +} + +static size_t ptrset_slot(uintptr_t key, size_t mask) { + return (size_t)((key >> 4) ^ (key >> 12)) & mask; +} + +static void ptrset_grow(PtrSet *set) { + uintptr_t *old_slots = set->slots; + size_t old_capacity = set->capacity; + set->capacity *= 2; + set->slots = calloc(set->capacity, sizeof(uintptr_t)); + size_t mask = set->capacity - 1; + for (size_t i = 0; i < old_capacity; i++) { + if (!old_slots[i]) { + continue; + } + size_t idx = ptrset_slot(old_slots[i], mask); + while (set->slots[idx]) { + idx = (idx + 1) & mask; + } + set->slots[idx] = old_slots[i]; + } + free(old_slots); +} + +// Returns true if ptr was newly inserted, false if it was already present. +static bool ptrset_insert(PtrSet *set, const void *ptr) { + if (!ptr) { + return false; + } + if ((set->count + 1) * 10 >= set->capacity * 7) { + ptrset_grow(set); + } + uintptr_t key = (uintptr_t)ptr; + size_t mask = set->capacity - 1; + size_t idx = ptrset_slot(key, mask); + while (set->slots[idx]) { + if (set->slots[idx] == key) { + return false; + } + idx = (idx + 1) & mask; + } + set->slots[idx] = key; + set->count++; + return true; +} + +// Flat free of a single expression's non-expression heap allocations. Shared +// sub-allocations are guarded by `freed` so each is released exactly once. +static void gc_free_node(Expression *expr, PtrSet *freed) { /* Uplink nodes are arena-managed; no per-node free needed. */ expr->uplinks = NULL; @@ -205,15 +276,21 @@ static void gc_free_node(Expression *expr) { free(expr->as.var.name); break; case MATCH_EXPRESSION: - for (int i = 0; i < expr->as.match.branch_count; i++) { - MatchBranch *branch = expr->as.match.branches[i]; - free(branch->pattern_variables); - free(branch); + if (ptrset_insert(freed, expr->as.match.branches)) { + for (int i = 0; i < expr->as.match.branch_count; i++) { + MatchBranch *branch = expr->as.match.branches[i]; + if (ptrset_insert(freed, branch)) { + free(branch->pattern_variables); + free(branch); + } + } + free(expr->as.match.branches); } - free(expr->as.match.branches); break; case FIX_EXPRESSION: - free(expr->as.fix.args); + if (ptrset_insert(freed, expr->as.fix.args)) { + free(expr->as.fix.args); + } break; case HOLE_EXPRESSION: free(expr->as.hole.name); @@ -228,15 +305,18 @@ void expression_gc_shutdown(void) { inductive_registry_shutdown(); conversion_cache_clear(); + PtrSet freed; + ptrset_init(&freed); ExprArenaPage *page = g_arena_pages; while (page) { ExprArenaPage *next = page->next; for (int i = 0; i < page->used; i++) { - gc_free_node(&page->nodes[i]); + gc_free_node(&page->nodes[i], &freed); } free(page); page = next; } + ptrset_free(&freed); g_arena_pages = NULL; g_arena_current = NULL; diff --git a/src/kernel/normalize.c b/src/kernel/normalize.c index 8f80a7f3..18ec6291 100644 --- a/src/kernel/normalize.c +++ b/src/kernel/normalize.c @@ -39,6 +39,22 @@ static Expression *_normalize_cbv(Expression *expr, ReductionFlags flags) { } } + // Try fix reduction on an applied fixpoint (mirrors normalize_whnf). + // Unfolds `(fix ...) arg` one step so the surrounding match can then + // iota-reduce; without this, cbv leaves applied fixpoints stuck. + if ((flags & REDUCE_FIX) && norm_func->tag == FIX_EXPRESSION && + is_fix_reducible(norm_func)) { + Expression *unfolded = fix_reduce(norm_func); + if (unfolded) { + next = init_app_expression_wc(unfolded, norm_arg, ctx); + if (next) { + current = next; + changed = true; + continue; + } + } + } + // Rebuild application if subexpressions changed if (norm_func != func || norm_arg != arg) { next = init_app_expression_wc(norm_func, norm_arg, ctx); From 32e0d5d8ee2271fd79b9b21897a7cea0e33ef735 Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sun, 28 Jun 2026 01:48:37 +0000 Subject: [PATCH 4/8] Guard fixpoint reduction on constructor-headed decreasing argument MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Induction over a goal stated with a Fixpoint applied to a symbolic recursive argument (e.g. proving `forall n, add n O = n` by `nat_ind`) crashed the engine with SIGSEGV. The shared root cause was non-termination when a fixpoint unfolds on a variable recursive argument: `add n O` reduced to `match n with ... S p => S (add p O)`, and conversion recursed into the branch, unfolding forever. Fixes: - fix_reduction.c: add `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 use it instead of reducing fixpoints unconditionally; a bare fix is now a value. - expression.c: register the fix node itself as the recursive variable's body (not the eta-expanded lambda), so unfolding the constant yields a fix node the guard can govern. fix_reduce therefore no longer substitutes the fix inline (which captured the shared argument binders) — it just strips to the lambda abstraction; recursive calls resolve through the recursive variable via delta. - command_exec.c: the Definition command accepts a declared type convertible (not merely structurally congruent) to the inferred type, so computational types such as `add O O = O` are accepted. The three bugs/ reproducers now run to completion; bugs/README.md and the reproducer headers are updated. examples/computational_eliminator.me gains an end-to-end induction proof over a fixpoint as regression coverage. All 431 kernel tests and every examples/*.me still pass. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- bugs/README.md | 92 +++++++++++++--------- bugs/note_clean_conversion_failure.me | 12 +-- bugs/segfault_apply_fixpoint_motive.me | 10 ++- bugs/segfault_exact_eliminator_fixpoint.me | 11 +-- examples/computational_eliminator.me | 18 +++++ src/commandlanguage/command_exec.c | 16 +++- src/kernel/conversion.c | 29 +++---- src/kernel/expression.c | 17 ++-- src/kernel/fix_reduction.c | 74 ++++++++++++++++- src/kernel/fix_reduction.h | 14 +++- src/kernel/normalize.c | 75 ++++++++---------- 11 files changed, 240 insertions(+), 128 deletions(-) diff --git a/bugs/README.md b/bugs/README.md index 12ec8a2f..4ef5074c 100644 --- a/bugs/README.md +++ b/bugs/README.md @@ -1,55 +1,75 @@ -# Known segfaults: induction over computational goals +# Fixed: induction over computational goals (symbolic-fixpoint reduction) -These two minimal examples crash the engine (SIGSEGV). They are **pre-existing** -kernel issues, not caused by the induction-principle generator change on this -branch — that change only fixed the *type* of the generated `_ind`. They surface -now because a correct, IH-bearing induction principle can finally be applied to a -goal stated with a `Fixpoint`. +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. -Both involve the same shape: an induction principle whose motive applies a -fixpoint (`add`) to a constructor-headed *symbolic* argument, so type-checking the -step case must reduce/convert `add (S n) O` with `n` a variable. (MEngine's -reduction is ground-only — `add (S n) O` does not reduce when `n` is symbolic; see -`bugs/note_clean_conversion_failure.me`, which fails *cleanly* with exit 1 rather -than crashing.) The crash is specific to the eliminator-*application* paths below. +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 139 -./build/mengine -q bugs/segfault_exact_eliminator_fixpoint.me # exit 139 +./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 ``` -## 1. `segfault_apply_fixpoint_motive.me` — the `apply` / unifier path +A complete worked proof of `forall n, add n O = n` by induction now lives in +`examples/computational_eliminator.me` as permanent regression coverage. -`apply (nat_ind )`, where the motive mentions the `add` fixpoint, crashes -while the tactic unifies the principle against the goal and builds the subgoals. -This is the direct route a real induction proof would take, so it currently blocks -proving e.g. `forall n, add n O = n` by induction. +## Root cause -## 2. `segfault_exact_eliminator_fixpoint.me` — the kernel type-check path +The shared root cause was non-termination when a fixpoint is unfolded on a +*symbolic* (variable) recursive argument. Three issues conspired: -`Check` (equivalently `exact`) of a fully explicit eliminator proof term crashes -while type-checking the step case, where `add (S n) O` must be converted to -`S (add n O)` under the `n` binder. This isolates the crash to the kernel's -handling of the eliminator application itself: the bare conversion alone does not -crash (it fails cleanly), but wrapping it in the eliminator application does. +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. -## Still not fixed here (the two reproducers above) +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. -Both reproducers above still crash. Fixing them is the remaining "Tier 2" work: -make iota/fix reduction fire on symbolic constructor-headed arguments, and harden -the eliminator application / conversion path against it. The shared root cause is -non-termination in `conversion_whnf`/`conversion_derivable` when a fixpoint is -unfolded on a symbolic (variable) recursive argument (`is_fix_reducible` is -unconditional), so the standard guard — reduce a fix only when its decreasing -argument is in constructor head normal form — is the proper repair. +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. -## Fixed on the stdlib-benchmark branch (related, but distinct) +## The fix -Two adjacent crashes/limitations *were* fixed to unblock the Rocq-stdlib +- `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 and all 431 kernel tests still pass: +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 diff --git a/bugs/note_clean_conversion_failure.me b/bugs/note_clean_conversion_failure.me index b30256dc..07ac309e 100644 --- a/bugs/note_clean_conversion_failure.me +++ b/bugs/note_clean_conversion_failure.me @@ -1,10 +1,10 @@ -(* NOT a crash: this fails cleanly (exit 1) with a type error. +(* FIXED (now exit 0). This used to fail cleanly (exit 1) with a type error. - It shows the underlying limitation behind the two segfaults: MEngine's - reduction is ground-only, so `add (S n) O` does not reduce to `S (add n O)` - when `n` is a variable, and the conversion is rejected. On its own this is a - clean rejection; only the eliminator-application paths (the two segfault_*.me - files) turn it into a crash. + 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 *) diff --git a/bugs/segfault_apply_fixpoint_motive.me b/bugs/segfault_apply_fixpoint_motive.me index f91cfbc4..2a6f853d 100644 --- a/bugs/segfault_apply_fixpoint_motive.me +++ b/bugs/segfault_apply_fixpoint_motive.me @@ -1,8 +1,10 @@ -(* SEGFAULT (exit 139). Pre-existing kernel crash, not fixed on this branch. +(* FIXED (now exit 0). This used to SIGSEGV (exit 139). - Applying an induction principle whose motive mentions a Fixpoint crashes the - `apply` tactic while it unifies the principle with the goal and builds the - subgoals. This is the natural route an induction proof of `add n O = n` takes. + 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 *) diff --git a/bugs/segfault_exact_eliminator_fixpoint.me b/bugs/segfault_exact_eliminator_fixpoint.me index 9af25c23..533035f1 100644 --- a/bugs/segfault_exact_eliminator_fixpoint.me +++ b/bugs/segfault_exact_eliminator_fixpoint.me @@ -1,9 +1,10 @@ -(* SEGFAULT (exit 139). Pre-existing kernel crash, not fixed on this branch. +(* FIXED (now exit 0). This used to SIGSEGV (exit 139). - Type-checking a fully explicit eliminator proof term crashes in the step case, - where `add (S n) O` must convert to `S (add n O)` under the `n` binder. The - bare conversion on its own fails *cleanly* (see note_clean_conversion_failure.me); - only wrapping it in the eliminator application crashes. + 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 *) diff --git a/examples/computational_eliminator.me b/examples/computational_eliminator.me index 4d64f6c3..8c491a96 100644 --- a/examples/computational_eliminator.me +++ b/examples/computational_eliminator.me @@ -34,3 +34,21 @@ Fixpoint add (n : nat) (m : nat) {struct n} : nat := (* 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. diff --git a/src/commandlanguage/command_exec.c b/src/commandlanguage/command_exec.c index 592a0970..b8f05cf4 100644 --- a/src/commandlanguage/command_exec.c +++ b/src/commandlanguage/command_exec.c @@ -98,7 +98,21 @@ static int _handle_definition_command(MEngineRuntime *rt, DefinitionCmd *defn_cm fprintf(stderr, ERROR "Error:" CRESET " definition '%s' has a invalid type.\n", name); } - if (!kernel_expr_congruent(inferred_type_def_body, expected_type_def_body)) { + // Accept the definition when the inferred and declared types are convertible, + // not merely structurally congruent. The fast structural check avoids the cost of + // full conversion in the common case; the fallback lets computational types match + // (e.g. a declared `add O O` against an inferred `O`). + bool types_match = kernel_expr_congruent(inferred_type_def_body, expected_type_def_body); + if (!types_match) { + Conversion *conv = kernel_expr_conversion_in_context( + rendered_type_ctx, inferred_type_def_body, expected_type_def_body); + if (conv) { + types_match = true; + kernel_conversion_free(conv); + } + } + + if (!types_match) { fprintf(stderr, ERROR "Type error:" CRESET " definition '%s' has a mismatched type.\n", name); char *_s1 = kernel_expr_to_string(expected_type_def_body); diff --git a/src/kernel/conversion.c b/src/kernel/conversion.c index 5eaca3a3..7452f6eb 100644 --- a/src/kernel/conversion.c +++ b/src/kernel/conversion.c @@ -281,16 +281,14 @@ static Expression *conversion_whnf(Expression *expr) { } } - if (norm_func->tag == FIX_EXPRESSION && is_fix_reducible(norm_func)) { - Expression *unfolded = fix_reduce(norm_func); - if (unfolded) { - Expression *next = init_app_expression_wc(unfolded, arg, ctx); - if (next) { - conversion_record_step(ctx, current, next, CONVERSION_FIX); - current = next; - continue; - } - } + // Reduce a fix at the head of the spine only when its decreasing + // argument is constructor-headed (guards against non-termination on + // symbolic recursive arguments). + Expression *fix_unfolded = fix_reduce_app(current, conversion_whnf); + if (fix_unfolded) { + conversion_record_step(ctx, current, fix_unfolded, CONVERSION_FIX); + current = fix_unfolded; + continue; } conversion_record_whnf(current, current); @@ -299,15 +297,8 @@ static Expression *conversion_whnf(Expression *expr) { } case FIX_EXPRESSION: { - if (is_fix_reducible(current)) { - Expression *next = fix_reduce(current); - if (next) { - conversion_record_step(get_expression_context(current), current, next, - CONVERSION_FIX); - current = next; - continue; - } - } + // A bare fix is a value; it reduces only once applied to a + // constructor-headed decreasing argument (handled in APP_EXPRESSION). conversion_record_whnf(current, current); conversion_record_whnf(start, current); return current; diff --git a/src/kernel/expression.c b/src/kernel/expression.c index 9a01c2bf..06254a63 100644 --- a/src/kernel/expression.c +++ b/src/kernel/expression.c @@ -891,15 +891,6 @@ Expression *init_fix_expression_wc(Expression *recursive_var, Expression **args, } } - Expression *body_bound = body; - for (int i = arg_count - 1; i >= 0; i--) { - body_bound = init_lambda_expression_wc(args[i], body_bound); - if (!body_bound) { - fprintf(stderr, ERROR "Failed to create body bound.\n" CRESET); - return NULL; - } - } - Expression *expr = _init_expression_base(/* tag */ FIX_EXPRESSION, /* context */ gamma, /* ctx_size */ gamma->ctx_size, /* type */ get_expression_type(recursive_var)); @@ -921,7 +912,13 @@ Expression *init_fix_expression_wc(Expression *recursive_var, Expression **args, } propagate_evar_refs(expr, body); - if (!register_fix_body_to_expression(recursive_var, body_bound)) { + // Register the fix node itself as the recursive variable's definition. Unfolding + // the constant therefore yields a fix node (a value), so reduction is governed by + // the guarded fix rule (see fix_reduce_app): it fires only once the decreasing + // argument is constructor-headed. Registering the eta-expanded lambda form instead + // would make the constant delta-unfold unconditionally and loop on symbolic + // recursive arguments. + if (!register_fix_body_to_expression(recursive_var, expr)) { fprintf(stderr, ERROR "Failed to register body to recursive variable.\n" CRESET); free_expression(expr); return NULL; diff --git a/src/kernel/fix_reduction.c b/src/kernel/fix_reduction.c index 2257848d..fbf7067f 100644 --- a/src/kernel/fix_reduction.c +++ b/src/kernel/fix_reduction.c @@ -2,7 +2,7 @@ #include -#include "src/kernel/subst.h" +#include "src/kernel/inductive.h" bool is_fix_reducible(Expression *expression) { return expression->tag == FIX_EXPRESSION; } @@ -11,13 +11,18 @@ Expression *fix_reduce(Expression *expression) { return NULL; } - Expression *recursive_var = get_fix_recursive_var(expression); Expression **args = get_fix_args(expression); int arg_count = get_fix_arg_count(expression); Expression *body = get_fix_body(expression); - Context *context = get_expression_context(body); - Expression *result = new_subst(context, body, recursive_var, expression); + // Recursive occurrences in the body refer to the fix's recursive variable, whose + // definitional body is this very fix node (registered in init_fix_expression_wc). + // So unfolding is just stripping the fix down to its lambda abstraction over the + // arguments; the recursive calls keep resolving through the recursive variable + // (via delta). Substituting the fix node inline instead would be wrong here: the + // fix shares its argument binders with the body, so re-binding them with the + // wrapping lambdas would capture the copies living inside the substituted fix. + Expression *result = body; for (int i = arg_count - 1; i >= 0; i--) { result = init_lambda_expression_wc(args[i], result); @@ -28,3 +33,64 @@ Expression *fix_reduce(Expression *expression) { return result; } + +Expression *fix_reduce_app(Expression *app, Expression *(*whnf)(Expression *)) { + // The fix at the head of the application spine fires only when its decreasing + // argument is in constructor head normal form. This is the standard guard that + // keeps reduction terminating on symbolic (variable) recursive arguments: + // `add n O` with `n` a variable stays stuck instead of unfolding forever. + Expression *head = get_head(app); + if (head->tag != FIX_EXPRESSION) { + return NULL; + } + + int decreasing_index = get_fix_decreasing_arg_index(head); + if (decreasing_index < 0) { + return NULL; + } + + // Count the spine arguments (app = (((fix) a0) a1) ... a_{count-1}). + int count = 0; + for (Expression *cursor = app; cursor->tag == APP_EXPRESSION; cursor = get_app_func(cursor)) { + count++; + } + if (decreasing_index >= count) { + // The decreasing argument has not been supplied yet; cannot reduce. + return NULL; + } + + Expression **args = malloc(count * sizeof(Expression *)); + if (!args) { + return NULL; + } + Expression *cursor = app; + for (int i = count - 1; i >= 0; i--) { + args[i] = get_app_arg(cursor); + cursor = get_app_func(cursor); + } + + Expression *decreasing_arg = whnf ? whnf(args[decreasing_index]) : args[decreasing_index]; + if (!is_constructor(get_head(decreasing_arg))) { + free(args); + return NULL; + } + + Expression *unfolded = fix_reduce(head); + if (!unfolded) { + free(args); + return NULL; + } + + Context *context = get_expression_context(app); + Expression *result = unfolded; + for (int i = 0; i < count; i++) { + result = init_app_expression_wc(result, args[i], context); + if (!result) { + free(args); + return NULL; + } + } + + free(args); + return result; +} diff --git a/src/kernel/fix_reduction.h b/src/kernel/fix_reduction.h index 843248d3..2f8fd438 100644 --- a/src/kernel/fix_reduction.h +++ b/src/kernel/fix_reduction.h @@ -24,4 +24,16 @@ bool is_fix_reducible(Expression *expression); // where gamma is the context which the fix expression is well-typed in. Expression *fix_reduce(Expression *expression); -#endif // FIX_REDUCTION_H \ No newline at end of file +// fix_reduce_app reduces an application `(((fix ...) a0) a1) ... an` whose head is a +// fix, but only when the guard condition holds: the decreasing argument (after being +// reduced to weak head normal form via `whnf`) is in constructor head normal form. +// This mirrors Coq's iota/fix rule and prevents non-termination when a fixpoint is +// applied to a symbolic (variable) recursive argument. +// +// Returns the unfolded-and-reapplied term on success, or NULL when `app` is not a +// fix application, the decreasing argument has not been supplied, or it is not +// constructor-headed (i.e. the redex is stuck). `whnf` may be NULL to skip reducing +// the decreasing argument (useful when the caller has already normalized it). +Expression *fix_reduce_app(Expression *app, Expression *(*whnf)(Expression *)); + +#endif // FIX_REDUCTION_H diff --git a/src/kernel/normalize.c b/src/kernel/normalize.c index 18ec6291..ae5d3714 100644 --- a/src/kernel/normalize.c +++ b/src/kernel/normalize.c @@ -39,31 +39,35 @@ static Expression *_normalize_cbv(Expression *expr, ReductionFlags flags) { } } - // Try fix reduction on an applied fixpoint (mirrors normalize_whnf). - // Unfolds `(fix ...) arg` one step so the surrounding match can then - // iota-reduce; without this, cbv leaves applied fixpoints stuck. - if ((flags & REDUCE_FIX) && norm_func->tag == FIX_EXPRESSION && - is_fix_reducible(norm_func)) { - Expression *unfolded = fix_reduce(norm_func); - if (unfolded) { - next = init_app_expression_wc(unfolded, norm_arg, ctx); - if (next) { - current = next; - changed = true; - continue; - } + // Rebuild the application with normalized subexpressions (the args + // are now values, since cbv normalizes them first). + Expression *rebuilt = current; + if (norm_func != func || norm_arg != arg) { + rebuilt = init_app_expression_wc(norm_func, norm_arg, ctx); + if (!rebuilt) { + break; } } - // Rebuild application if subexpressions changed - if (norm_func != func || norm_arg != arg) { - next = init_app_expression_wc(norm_func, norm_arg, ctx); - if (next) { - current = next; + // Guarded fix reduction on an applied fixpoint (mirrors + // normalize_whnf): unfold `(fix ...) args` one step only when the + // decreasing argument is constructor-headed, so the surrounding match + // can then iota-reduce. The guard prevents runaway unfolding on a + // symbolic recursive argument. + if (flags & REDUCE_FIX) { + Expression *unfolded = fix_reduce_app(rebuilt, normalize_whnf); + if (unfolded) { + current = unfolded; changed = true; continue; } } + + if (rebuilt != current) { + current = rebuilt; + changed = true; + continue; + } break; } @@ -83,17 +87,8 @@ static Expression *_normalize_cbv(Expression *expr, ReductionFlags flags) { } case FIX_EXPRESSION: { - // Try fix reduction if enabled - if ((flags & REDUCE_FIX) && is_fix_reducible(current)) { - next = fix_reduce(current); - if (next) { - // Continue normalizing the result of fix reduction - current = next; - changed = true; - continue; - } - } - // FIX expressions that can't be reduced are in normal form + // A bare fix is a value; it reduces only once applied to a + // constructor-headed decreasing argument (see the APP case). return current; } @@ -199,25 +194,21 @@ Expression *normalize_whnf(Expression *expr) { continue; } - if (norm_func->tag == FIX_EXPRESSION && is_fix_reducible(norm_func)) { - Expression *unfolded = fix_reduce(norm_func); - if (unfolded) { - current = init_app_expression_wc(unfolded, arg, ctx); - continue; - } + // Guarded fix reduction: only fire when the decreasing argument is + // constructor-headed (see fix_reduce_app), preventing runaway + // unfolding on symbolic recursive arguments. + Expression *fix_unfolded = fix_reduce_app(current, normalize_whnf); + if (fix_unfolded) { + current = fix_unfolded; + continue; } return current; } case FIX_EXPRESSION: { - if (is_fix_reducible(current)) { - Expression *next = fix_reduce(current); - if (next) { - current = next; - continue; - } - } + // A bare fix is a value; reduction happens in APP_EXPRESSION once a + // constructor-headed decreasing argument is applied. return current; } From 111fd39fef01f606e0e4d4fe7f252b1a01099872 Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sun, 28 Jun 2026 04:16:49 +0000 Subject: [PATCH 5/8] Support rewrite on a quantified IH and applying a redex-typed eliminator Engine fixes (split out from the original stdlib-benchmark commit) that let computational induction be driven by rewrite on the induction hypothesis: - src/kernel/fix_reduction.c, normalize.c: a symbolic-fixpoint reduction leaves a stuck recursive call headed by the constant (add n O, not a bare fix node), so rewrite/congruence can match it after simpl. - src/engine/unify.c, rewrite_internal.c, src/tacticlanguage/tactic_interp.c, src/runtime/core.c: rewrite reads the equation off an IH whose stored type is the eliminator's beta-redex (motive) n by whnf-normalizing it first; _get_lhs_eq fails cleanly (NULL) on a non-eq type. - src/kernel/expression.c: a redex-typed IH can be applied (the syntactic-Pi precheck in init_app_expression_wc is removed; _construct_app_type whnfs). - src/kernel/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. examples/computational_induction_rewrite.me is the regression. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- bugs/README.md | 10 ++++ examples/computational_induction_rewrite.me | 58 +++++++++++++++++++++ src/engine/rewrite_internal.c | 9 +++- src/engine/unify.c | 8 ++- src/kernel/expression.c | 10 ++-- src/kernel/fix_reduction.c | 21 ++++++-- src/kernel/normalize.c | 14 +++++ src/kernel/type_compat.c | 12 +++++ src/runtime/core.c | 13 ++++- src/tacticlanguage/tactic_interp.c | 9 +++- 10 files changed, 148 insertions(+), 16 deletions(-) create mode 100644 examples/computational_induction_rewrite.me diff --git a/bugs/README.md b/bugs/README.md index 4ef5074c..59517b97 100644 --- a/bugs/README.md +++ b/bugs/README.md @@ -22,6 +22,16 @@ Run them with: 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 diff --git a/examples/computational_induction_rewrite.me b/examples/computational_induction_rewrite.me new file mode 100644 index 00000000..b14c6e46 --- /dev/null +++ b/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. diff --git a/src/engine/rewrite_internal.c b/src/engine/rewrite_internal.c index fa7a9b26..af39ca9c 100644 --- a/src/engine/rewrite_internal.c +++ b/src/engine/rewrite_internal.c @@ -358,8 +358,13 @@ RewriteResult *rewrite_head(Expression *mid, Expression *lemma, Context *context } Expression *proof = unif_result->lemma_instantiation; - Expression *proof_type = kernel_expr_type(proof); - if (!kernel_expr_congruent(_get_lhs_eq(proof_type), mid)) { + // Normalize the proof's type before reading off its equality: an induction + // hypothesis arrives as a beta-redex `(motive) x` (the eliminator's `P x`), so + // whnf exposes the underlying eq. Without this _get_lhs_eq returns NULL and the + // congruence check below dereferences it. + Expression *proof_type = kernel_normalize_whnf(kernel_expr_type(proof)); + Expression *lhs = _get_lhs_eq(proof_type); + if (!lhs || !kernel_expr_congruent(lhs, mid)) { free_unification_result(unif_result); return init_rewrite_result(mid, mid, NULL, NULL); } diff --git a/src/engine/unify.c b/src/engine/unify.c index 037b40c0..1112112d 100644 --- a/src/engine/unify.c +++ b/src/engine/unify.c @@ -205,7 +205,11 @@ UnificationResult *eunify2(Expression *lemma, Expression *goal) { UnificationResult *bad_unify_for_eq(Context *goal_context, Expression *lemma, Expression *expr) { Expression *current_lemma_app = lemma; - Expression *current_lemma_app_ty = kernel_expr_type(current_lemma_app); + // Normalize the lemma type before inspecting it: an induction hypothesis arrives + // as a beta-redex `(motive) x` (the eliminator's `P x`) whose whnf is the actual + // `forall ... eq ...`. Without this the foralls stay hidden behind the redex and + // never get instantiated, so the rewrite finds nothing to do. + Expression *current_lemma_app_ty = kernel_normalize_whnf(kernel_expr_type(current_lemma_app)); DoublyLinkedList *remaining_open = dll_create(); while (kernel_expr_is_forall(current_lemma_app_ty)) { Expression *current_lemma_ty_lhs = @@ -229,7 +233,7 @@ UnificationResult *bad_unify_for_eq(Context *goal_context, Expression *lemma, Ex dll_destroy(remaining_open); return NULL; } - current_lemma_app_ty = kernel_expr_type(current_lemma_app); + current_lemma_app_ty = kernel_normalize_whnf(kernel_expr_type(current_lemma_app)); } return init_unification_result(current_lemma_app, remaining_open); } diff --git a/src/kernel/expression.c b/src/kernel/expression.c index 06254a63..c0982d4b 100644 --- a/src/kernel/expression.c +++ b/src/kernel/expression.c @@ -533,11 +533,11 @@ Expression *init_app_expression_wc(Expression *func, Expression *arg, Context *c return NULL; } - Expression *func_type = get_expression_type(func); - if (func_type->tag != FORALL_EXPRESSION) { - fprintf(stderr, ERROR "Function is not a Forall expression.\n" CRESET); - return NULL; - } + // Whether `func`'s type is a Pi is validated by _construct_app_type below, which + // weak-head-normalizes first. That matters for functions whose type is a Pi only + // up to reduction (e.g. an induction hypothesis typed by the eliminator's + // beta-redex `(motive) x`); a premature syntactic FORALL check here would reject + // them. _construct_app_type returns NULL (and reports) for genuine non-functions. if (!valid_in_context(arg, context)) { fprintf(stderr, ERROR "Argument is not valid in context.\n" CRESET); diff --git a/src/kernel/fix_reduction.c b/src/kernel/fix_reduction.c index fbf7067f..6486c02b 100644 --- a/src/kernel/fix_reduction.c +++ b/src/kernel/fix_reduction.c @@ -2,6 +2,7 @@ #include +#include "src/kernel/delta_reduction.h" #include "src/kernel/inductive.h" bool is_fix_reducible(Expression *expression) { return expression->tag == FIX_EXPRESSION; } @@ -39,12 +40,26 @@ Expression *fix_reduce_app(Expression *app, Expression *(*whnf)(Expression *)) { // argument is in constructor head normal form. This is the standard guard that // keeps reduction terminating on symbolic (variable) recursive arguments: // `add n O` with `n` a variable stays stuck instead of unfolding forever. + // + // The head may already be a fix node, or a constant (recursive variable) whose + // definition is this fix. cbv/whnf keep such constants folded so that a *stuck* + // residual stays constant-headed (`add n O`, not `(fix ...) n O`) and therefore + // matchable by rewrite/congruence; we unfold here only to govern firing. Expression *head = get_head(app); - if (head->tag != FIX_EXPRESSION) { + Expression *fix = NULL; + if (head->tag == FIX_EXPRESSION) { + fix = head; + } else if (head->tag == VAR_EXPRESSION && is_delta_reducible(head)) { + Expression *body = delta_reduce(head); + if (body && body->tag == FIX_EXPRESSION) { + fix = body; + } + } + if (!fix) { return NULL; } - int decreasing_index = get_fix_decreasing_arg_index(head); + int decreasing_index = get_fix_decreasing_arg_index(fix); if (decreasing_index < 0) { return NULL; } @@ -75,7 +90,7 @@ Expression *fix_reduce_app(Expression *app, Expression *(*whnf)(Expression *)) { return NULL; } - Expression *unfolded = fix_reduce(head); + Expression *unfolded = fix_reduce(fix); if (!unfolded) { free(args); return NULL; diff --git a/src/kernel/normalize.c b/src/kernel/normalize.c index ae5d3714..64ed76dc 100644 --- a/src/kernel/normalize.c +++ b/src/kernel/normalize.c @@ -75,6 +75,14 @@ static Expression *_normalize_cbv(Expression *expr, ReductionFlags flags) { // Try delta reduction if enabled if ((flags & REDUCE_DELTA) && is_delta_reducible(current)) { next = delta_reduce(current); + if (next && next->tag == FIX_EXPRESSION) { + // A constant whose definition is a fixpoint is a value here; it + // fires only when applied to a constructor-headed decreasing + // argument (handled in the APP case via fix_reduce_app). Holding + // it folded keeps a stuck residual constant-headed (`add n O`, + // not `(fix ...) n O`) so rewrite/congruence can match it. + return current; + } if (next) { // Continue normalizing the unfolded definition current = next; @@ -168,6 +176,12 @@ Expression *normalize_whnf(Expression *expr) { case VAR_EXPRESSION: { if (is_delta_reducible(current)) { Expression *next = delta_reduce(current); + if (next && next->tag == FIX_EXPRESSION) { + // Fixpoint constant: a value here, fires in the APP case via + // fix_reduce_app. Holding it folded keeps stuck residuals + // constant-headed and matchable (see _normalize_cbv). + return current; + } if (next) { current = next; continue; diff --git a/src/kernel/type_compat.c b/src/kernel/type_compat.c index ad4971b2..54bbae79 100644 --- a/src/kernel/type_compat.c +++ b/src/kernel/type_compat.c @@ -40,6 +40,18 @@ static bool _open_compat(Expression *expected, Expression *actual, Map *bv_map, } if (actual->tag == HOLE_EXPRESSION) { + // Symmetric to the expected-side case: a hole on the actual (term-type) side is + // an unsolved evar that must be instantiated to `expected` for the term's type + // to match. This occurs when applying a function whose result type is a + // beta-redex that whnf-reduces to a binder (e.g. an eliminator's `motive y0` + // with a quantified motive): the index `y0` cannot be solved by spine + // unification and ends up embedded in the term type as a hole. Recording the + // assignment lets fill_hole cascade-fill it instead of leaving a stray goal. + Expression *already_mapped = linear_map_get(holes, actual); + if (already_mapped != NULL) { + return _open_compat(expected, already_mapped, bv_map, holes); + } + linear_map_set(holes, actual, expected); return _open_compat(get_expression_type(expected), get_expression_type(actual), bv_map, holes); } diff --git a/src/runtime/core.c b/src/runtime/core.c index 1cdc9074..45297a9b 100644 --- a/src/runtime/core.c +++ b/src/runtime/core.c @@ -468,8 +468,17 @@ static Context *init_bad_app_congruence(Context *c) { } Expression *_get_lhs_eq(Expression *eq_expression) { - // eq_expression is of the form eq A x y - return kernel_app_arg(kernel_app_func(eq_expression)); + // eq_expression is of the form `eq A x y`; return NULL when it is not a fully + // applied equality (e.g. a partially-applied or non-eq type), so callers fail + // cleanly instead of dereferencing a missing application argument. + if (!eq_expression || !kernel_expr_is_app(eq_expression)) { + return NULL; + } + Expression *eq_app = kernel_app_func(eq_expression); + if (!eq_app || !kernel_expr_is_app(eq_app)) { + return NULL; + } + return kernel_app_arg(eq_app); } Expression *_get_rhs_eq(Expression *eq_expression) { diff --git a/src/tacticlanguage/tactic_interp.c b/src/tacticlanguage/tactic_interp.c index fc6d951f..0496e454 100644 --- a/src/tacticlanguage/tactic_interp.c +++ b/src/tacticlanguage/tactic_interp.c @@ -849,8 +849,13 @@ TacticResult *tactic_interpret(MEngineRuntime *rt, Expression *goal, TacticExpr return engine_tactic_result_new(false, NULL, "rewrite_unify: unresolved bindings"); } Expression *inst = engine_unify_get_lemma(unif); - Expression *proof_type = kernel_expr_type(inst); - if (!kernel_expr_congruent(_get_lhs_eq(proof_type), target)) { + // Normalize the lemma type: an induction hypothesis arrives as a beta-redex + // `(motive) x` (the eliminator's `P x`), so reduce to expose the underlying + // eq before extracting its LHS. Without this _get_lhs_eq returns NULL and the + // congruence check dereferences it. + Expression *proof_type = kernel_normalize_whnf(kernel_expr_type(inst)); + Expression *lhs = _get_lhs_eq(proof_type); + if (!lhs || !kernel_expr_congruent(lhs, target)) { engine_unify_free(unif); return engine_tactic_result_new(false, NULL, "rewrite_unify: LHS does not match target"); From 722775d8086d1fd2b5c4cf6fccc06e5360f670a5 Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sun, 28 Jun 2026 04:16:49 +0000 Subject: [PATCH 6/8] Reduce fixpoints over parametric constructors (match alias + map capacity) Engine fixes (split out from the Lists benchmark commit) that unblock all reduction over parametric inductives such as list A: - src/kernel/mixed_subst.c: preserve a match parameter-slot pattern variable's delta-reducible body alias (_ := A) when rebuilding a branch under a substitution. Both rebuilders dropped it, so reducing a fixpoint over a parametric constructor (app A (cons A x xs) k) lost the alias, failed to type-check the branch body, and crashed on the resulting NULL. - src/common/map.c: map_new_with_capacity rounds up to a power of two. The open-addressing map masks indices with hash & (capacity - 1); iota_reduce sized its pattern map to the constructor arg count (3 for cons), so absent-key lookups in the full table probed forever. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- src/common/map.c | 15 ++++++++++++++- src/kernel/mixed_subst.c | 31 ++++++++++++++++++++++++++++--- 2 files changed, 42 insertions(+), 4 deletions(-) diff --git a/src/common/map.c b/src/common/map.c index 3d02dd72..8c9d2712 100644 --- a/src/common/map.c +++ b/src/common/map.c @@ -37,6 +37,19 @@ struct Map { static MapEntry *map_entries_new(size_t capacity) { return calloc(capacity, sizeof(MapEntry)); } +// All slot indexing masks with `capacity - 1`, so the capacity must be a power +// of two (otherwise the probe sequence skips slots and a lookup of an absent key +// in a full table loops forever). map_new uses a power-of-two literal and resize +// doubles, but map_new_with_capacity takes a caller-supplied size (e.g. a match's +// pattern-variable count), so round it up to the next power of two, floor 1. +static size_t map_round_capacity(size_t requested) { + size_t cap = 1; + while (cap < requested) { + cap <<= 1; + } + return cap; +} + // Size+tombstones together determine slot pressure. static bool map_should_grow(Map *m) { return (m->size + m->tombstones + 1) * MAP_LOAD_FACTOR_DEN > m->capacity * MAP_LOAD_FACTOR_NUM; @@ -100,7 +113,7 @@ Map *map_new_with_capacity(size_t initial_capacity) { if (!m) { return NULL; } - m->capacity = initial_capacity; + m->capacity = map_round_capacity(initial_capacity); m->size = 0; m->tombstones = 0; m->entries = map_entries_new(m->capacity); diff --git a/src/kernel/mixed_subst.c b/src/kernel/mixed_subst.c index 5c6669db..db1d2171 100644 --- a/src/kernel/mixed_subst.c +++ b/src/kernel/mixed_subst.c @@ -369,10 +369,24 @@ static Expression *_simple_topdown_psubst(Context *ctx, Expression *t, Map *subs Expression *old_var_type = get_expression_type(old_var); Expression *new_var_type = _simple_topdown_psubst(branch_ctx, old_var_type, subst_map, NULL); + // A parameter-slot pattern variable of a parametric inductive + // carries a delta-reducible body (the type argument read off the + // scrutinee, e.g. `_ := A`). Preserve it: dropping the alias here + // makes later pattern variables' types (`x : _`, `xs : list _`) + // opaque, so rebuilding the branch body's applications fails to + // type-check. + Expression *old_var_body = get_var_body(old_var); + Expression *new_var_body = + old_var_body + ? _simple_topdown_psubst(branch_ctx, old_var_body, subst_map, NULL) + : NULL; Expression *new_var; - if (new_var_type == old_var_type && + if (new_var_type == old_var_type && new_var_body == old_var_body && branch_ctx == get_expression_context(old_var)) { new_var = old_var; + } else if (old_var_body) { + new_var = init_var_expression_wc_with_body(get_var_name(old_var), + new_var_body, branch_ctx); } else { new_var = init_var_expression_wc(get_var_name(old_var), new_var_type, branch_ctx); @@ -630,8 +644,19 @@ static Expression *spine_rebuild(Context *apps_ctx, Expression *node, Map *subst Expression *old_var = br->pattern_variables[j]; Expression *new_var_type = maybe_rebuild(apps_ctx, get_expression_type(old_var), subst_map, memo, subtree_gen); - Expression *new_var = - init_var_expression_wc(get_var_name(old_var), new_var_type, apps_ctx); + // Preserve a parameter-slot pattern variable's delta-reducible + // body (see the matching note in _simple_topdown_psubst). + Expression *old_var_body = get_var_body(old_var); + Expression *new_var; + if (old_var_body) { + Expression *new_var_body = + maybe_rebuild(apps_ctx, old_var_body, subst_map, memo, subtree_gen); + new_var = init_var_expression_wc_with_body(get_var_name(old_var), + new_var_body, apps_ctx); + } else { + new_var = + init_var_expression_wc(get_var_name(old_var), new_var_type, apps_ctx); + } br2->pattern_variables[j] = new_var; if (new_var != old_var) { map_set(subst_map, old_var, new_var); From 17c69852d1ffd26b34f5bd32f76f396697cb20c4 Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sun, 28 Jun 2026 04:06:42 +0000 Subject: [PATCH 7/8] Document pre-existing dangling-options use-after-return in bugs/ `mengine_runtime_new` borrows MEngineOptions by pointer (rt->options = options) and reads through it for the runtime's whole life, while the integration test's make_rt hands it a stack-local that dies on return. Benign without ASan (the freed stack slot still holds the old bytes), but a genuine stack-use-after-return that aborts `make check` under AddressSanitizer. Captured here as a known, separate issue with root cause, ASan stack, repro command, and fix options. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- bugs/note_dangling_options_pointer.md | 85 +++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 bugs/note_dangling_options_pointer.md diff --git a/bugs/note_dangling_options_pointer.md b/bugs/note_dangling_options_pointer.md new file mode 100644 index 00000000..5f0a2d68 --- /dev/null +++ b/bugs/note_dangling_options_pointer.md @@ -0,0 +1,85 @@ +# Not fixed: dangling `MEngineOptions *` (use-after-return under ASan) + +**Status:** pre-existing, **not fixed**. Discovered while validating the +parametric-list kernel fixes (`stdlib-benchmark` branch) under AddressSanitizer; +unrelated to those fixes. Documented here so the next person who runs `make +check` under ASan knows it is a known, separate issue rather than a regression. + +## 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. + +## Fix options (when someone takes this on) + +1. **Own the options (preferred):** make `mengine_runtime_new` copy the struct + (`rt->options = malloc(sizeof *options); *rt->options = *options;`) and free it + in `mengine_runtime_free`. Removes the lifetime footgun for every caller. + Watch for code that *mutates* `rt->options` and expects the caller to observe + it (e.g. `runtime.c:76-79` toggles `quiet`; that stays internal, so a copy is + fine) and for callers that share one options struct across runtimes. +2. **Fix the caller only:** give `make_rt`'s options a lifetime ≥ the runtime + (a `static`/heap allocation). Narrower; leaves the by-reference API as a trap + for the next caller. + +No `.me` reproducer: this is a C-level lifetime bug in the runtime/test harness, +not a kernel or proof-checking bug, and it cannot affect proof soundness. From dfe09478c83316babd144f4a51a7320fce735952 Mon Sep 17 00:00:00 2001 From: Dustin Jamner Date: Sun, 28 Jun 2026 04:19:14 +0000 Subject: [PATCH 8/8] Fix dangling MEngineOptions pointer: runtime owns a copy mengine_runtime_new borrowed its options by pointer (rt->options = options) and read through it for the runtime's whole life, while a caller passing a stack-local options struct (e.g. the integration test's make_rt) left it dangling on return. Benign without ASan, but a genuine stack-use-after-return that aborted `make check` under AddressSanitizer. The runtime now mallocs and copies the options, and frees the copy in mengine_runtime_free. Mutations through rt->options (the quiet toggle, the execution_type) were already runtime-internal; main.c passes options by value and never reads them back, so owning a copy changes no observable behaviour. make check under ASan now runs to completion (431/431, no use-after-return). Updates bugs/note_dangling_options_pointer.md to record the fix. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT --- bugs/note_dangling_options_pointer.md | 39 +++++++++++++++------------ src/runtime/runtime.c | 15 ++++++++++- 2 files changed, 36 insertions(+), 18 deletions(-) diff --git a/bugs/note_dangling_options_pointer.md b/bugs/note_dangling_options_pointer.md index 5f0a2d68..4e7309da 100644 --- a/bugs/note_dangling_options_pointer.md +++ b/bugs/note_dangling_options_pointer.md @@ -1,9 +1,10 @@ -# Not fixed: dangling `MEngineOptions *` (use-after-return under ASan) +# Fixed: dangling `MEngineOptions *` (use-after-return under ASan) -**Status:** pre-existing, **not fixed**. Discovered while validating the -parametric-list kernel fixes (`stdlib-benchmark` branch) under AddressSanitizer; -unrelated to those fixes. Documented here so the next person who runs `make -check` under ASan knows it is a known, separate issue rather than a regression. +**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 @@ -69,17 +70,21 @@ 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. -## Fix options (when someone takes this on) +## The fix -1. **Own the options (preferred):** make `mengine_runtime_new` copy the struct - (`rt->options = malloc(sizeof *options); *rt->options = *options;`) and free it - in `mengine_runtime_free`. Removes the lifetime footgun for every caller. - Watch for code that *mutates* `rt->options` and expects the caller to observe - it (e.g. `runtime.c:76-79` toggles `quiet`; that stays internal, so a copy is - fine) and for callers that share one options struct across runtimes. -2. **Fix the caller only:** give `make_rt`'s options a lifetime ≥ the runtime - (a `static`/heap allocation). Narrower; leaves the by-reference API as a trap - for the next caller. +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. -No `.me` reproducer: this is a C-level lifetime bug in the runtime/test harness, -not a kernel or proof-checking bug, and it cannot affect proof soundness. +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. diff --git a/src/runtime/runtime.c b/src/runtime/runtime.c index b14936a6..c8df46c1 100644 --- a/src/runtime/runtime.c +++ b/src/runtime/runtime.c @@ -53,10 +53,22 @@ MEngineRuntime *mengine_runtime_new(MEngineOptions *options) { rt->proof_state = NULL; rt->pending_theorem = NULL; - rt->options = options; + + // Own a private copy of the options rather than borrowing the caller's + // pointer. The runtime reads through rt->options for its whole life (and + // even mutates it transiently, e.g. the quiet toggle below), so a borrowed + // pointer to a caller stack local would dangle the moment that caller + // returns. See bugs/note_dangling_options_pointer.md. + rt->options = malloc(sizeof(MEngineOptions)); + if (!rt->options) { + free(rt); + return NULL; + } + *rt->options = *options; rt->ctx = kernel_context_empty(); if (!rt->ctx) { + free(rt->options); free(rt); return NULL; } @@ -110,6 +122,7 @@ void mengine_runtime_free(MEngineRuntime *rt) { engine_rewrite_print_cumulative_stats(); kernel_context_free(rt->ctx); + free(rt->options); free(rt); kernel_expression_gc_shutdown();