Engine fixes#4
Merged
Merged
Conversation
The auto-generated <T>_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 <T>_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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
…city) 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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
`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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GNvD2hCU3jo1wq6fCLv9GT
This was referenced Jun 28, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Warning: the code in this PR was AI-generated and not human-validated. It should be treated with suspicion until reviewed line-by-line or rewritten.
Includes LLM fixes to a number of bugs in the engine, especially around inductives and fixpoints, including adding inductive hypotheses to the principles generated by inductive datatypes.
Supersedes #2 and should be seen as a prerequisite for #3 , which is now based on this branch.