Repository navigation
[v0.4] Add reasoning-machine semantics: state, rules, search, verification, iteration, and termination #31
Description
Scope
Represent reasoning engines as ordinary LexLean computational/formal objects.
Work
- Define typed reasoning state, observation, rule/inference, candidate, verification, branch/search, iteration/fuel, and result/error semantics.
- Support deterministic rule engines and bounded search; permit richer search only with explicit termination/resource evidence.
- Make every inference rule and verifier a typed semantic object with explicit proof/evidence relationship.
- Separate reasoning trace/evidence from user-facing prose.
DoD
- No opaque reasoner primitive or model-based semantic escape hatch.
- Search/resource accounting is explicit for production/GNAF claims.
- Reasoning state transitions lower to Lean and production-eligible forms compile to Rust.
Acceptance criteria
- Nontrivial expert-system/reasoning fixture performs multi-step derivation and verifies its invariant/result.
- Invalid rule application, nonterminating/unbounded search, forged trace, and inconsistent verifier negatives fail closed.
- A planted rule-semantics mutation is detected.
- Full just vv passes.
Depends on generalized language, model semantics, and state/graph primitives.
Activity
afflom commentedon Oct 4, 2026
Integration audit found main source/artifact drift: main commit 6944f8b imported compiler/src/ReasoningOracle.lex.tex and reasoning fixtures/packages/expected outputs without the reasoning compiler, schemas, generator, specification, or registered RS cases. Current main 629f76b still has that split. A genuine compiler-project build after merging main into PR #51 fails LLT4001: unknown variant logic (expected the currently implemented declaration kinds). Independent AST review found one logic, eight inference_rule, two verifier and two reasoner declarations; the imported AST matches the older 364aaf7 reasoning source, not the current PR #50 head e7ac020. The existing calculus generator does not own ReasoningOracle or its Main import. Running that writer alone would remove orphaned reasoning artifacts rather than implement this feature. Complete feature-preserving integration needs the authored reasoning implementation and current proof/generator/test prerequisites from #50, followed by actual regeneration and all RS/existing kernel/native gates. This is distinct from the byte-literal lowering change; no permissive parser alias or handwritten Lean repair has been introduced.
Reasoning-machine semantics (#31) (#50)
Merge origin/main (#31 reasoning machines, #50) into issue-25; cut th…
Reasoning: register RS-01..RS-14, their scenarios, and failing tests