Implement WokeLang interpreter in Rust#2
Merged
Conversation
Complete implementation of WokeLang with: Lexer (src/lexer/): - Token definitions for all keywords, operators, literals - Uses logos for fast tokenization - Handles comments, strings with escapes, numbers Parser (src/parser/): - Recursive descent parser - Full expression parsing with correct precedence - All statement types: remember, when/otherwise, repeat, attempt safely - Pattern matching with decide based on - Emote tags, consent blocks, gratitude declarations AST (src/ast/): - Complete type definitions for all language constructs - Spanned nodes for error reporting Interpreter (src/interpreter/): - Tree-walking interpreter - Scoped environments for variables - Built-in functions: print, len, toString, toInt - Consent system with interactive prompts - Pattern matching evaluation - All operators (arithmetic, comparison, logical) CLI (src/main.rs): - woke <file.woke> - run program - woke --tokenize <file> - show tokens - woke --parse <file> - show AST Examples: - examples/hello.woke - feature showcase - examples/demo.woke - runnable demo
hyperpolymath
added a commit
that referenced
this pull request
Jun 14, 2026
…I gate (#79) ## Summary The Lean 4 formal-verification file `docs/proofs/verification/WokeLang.lean` claimed *"all 12 `sorry` eliminated / verified"* — but it had **silently bit-rotted** and did **not compile** under a current Lean toolchain (~100 errors). Root cause: **no CI ever ran the prover** (workflows only covered the OCaml core + e2e), so the headline correctness claim was never machine-enforced. This PR restores **sorry-free compilation under Lean 4.30.0**, adds the missing **CI gate**, and documents a coverage/correspondence audit. ## What changed **Only proof bodies + 2 `deriving` clauses + 1 `abbrev`** — every theorem signature and every inductive is **byte-identical** (verified by diff). No statement was weakened; no `sorry`/`admit`/`axiom` introduced. Root causes fixed: - **`DecidableEq` no longer derives** for `Value`/`WokeType` (`Float` has none — NaN; and nested `List Self` blocks the deriving handler) → reduced to `deriving Repr`; equality decisions use Lean's classical `by_cases` (no instance needed). - **`induction`/`cases` on concrete indices** (`emptyTypeEnv`, `emptyEnv`) + binder-arity drift across Lean versions. `preservation` made **type-polymorphic** via `induction hs generalizing t` (its congruence cases need the IH at the operand type, not the result type). `cases … with | inr ⟨..⟩` anonymous-constructor patterns → `obtain` (no longer supported in `cases`). Type-mismatched reduction siblings discharged with `nomatch`. - **`BEq Permission`**: made `Permission` a reducible `abbrev` so the `String` instance transfers. ## Verification ``` $ lean docs/proofs/verification/WokeLang.lean # exit 0, no output ``` Machine-checked: `progress`, `preservation`, `type_safety` (multi-step), `consent_monotonicity`, `consent_preservation` — for the expression core (incl. the Result/`unwrap`/`error` panic-propagation fragment). ## Added - **`docs/proofs/verification/lean-toolchain`** — pins Lean v4.30.0. - **`docs/proofs/verification/AUDIT.md`** — answers PROOF-NEEDS.md #1 & #2: the proofs cover a **clean expression core** (a strict, honestly-scoped subset), the Lean type system corresponds to the **Rust** typechecker (not the OCaml `core/eval.ml`, which models a different language), and the consent theorems correspond to the spec's Hoare logic. - **`.github/workflows/lean-proofs.yml`** — installs the pinned toolchain and runs the check on every push to the proof dir, so this can't bit-rot again. SHA-pinned action, pure-bash install (matches estate governance). ## Note on scope This repairs and re-verifies the **existing** proofs and makes them durable. It does **not** yet extend coverage (more binops/comparisons, statements, arrays, compiler/VM correctness) — those remain per PROOF-NEEDS.md and are tabulated in AUDIT.md. https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7 --- _Generated by [Claude Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_ Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jun 15, 2026
…ation state (#83) ## Why The Lean + Coq proof repair/extension landed in **#79–#82 (all merged)** but was **invisible to the estate's bot-coordination layer**. The machine-readable state still described a pre-proof-work world: - `STATE.a2ml [frontier]` named only an aspirational Isabelle narrative and **omitted the existing, now-verified Lean+Coq type-safety track** entirely; `last-shepherd` stopped at #77. - `debt.a2ml` carried **zero** real items — so the documented proof follow-ups would not reach the next session's Phase 0. - `coverage.a2ml` had no record that `docs/proofs/verification/` was visited. - `methodology.a2ml`'s divergent-mode invariants were generic template stubs — one example literally read *"Idris2 only … no Lean4, Coq"*, the **opposite** of reality, a real footgun for a divergent-mode bot. ## What (all additive; no curated content overwritten) Surfaced through the channels whose own contracts say *"updated by agents at session end"*: | File | Change | |---|---| | `bot_directives/debt.a2ml` | Carry-forward follow-ups as Phase-0 input: **should** — Coq binop parity, Lean array typing (Coq's is a ready template), `cap_subsumes_trans`; **could** — Coq `preservation` clean rewrite, Lean float binops, echo-types L3 integration blueprint. | | `bot_directives/coverage.a2ml` | `docs/proofs/verification/` recorded as a visited component (PRs #79–#82). | | `bot_directives/methodology.a2ml` | `divergent-invariants`: provers are **Lean 4 + Coq** (not Idris2/Isabelle); admit/sorry stay **zero**; the `Coq.Reals` axioms are **permitted, not escape hatches** (don't let an Axiom-scanner flag them). `known-constraints`: CI-gated + toolchain-pinned (Coq is version-sensitive); Lean/Coq cover **complementary** subsets; PROOF-NEEDS #2 is **ill-posed** pending a maintainer (a)/(b) decision. | | `6a2/STATE.a2ml` | Added `type-safety-proofs` to `[frontier]`; added `proof-gates` + `last-proof-shepherd` to `[ci]`. Existing lines preserved. | Source of truth for every claim: [`docs/proofs/verification/AUDIT.md`](../blob/main/docs/proofs/verification/AUDIT.md). ## Notes for review - **Draft on purpose** — `.machine_readable/` is maintainer-curated (`gitbot-fleet`/`hypatia` are both barred from it), so this goes through human review rather than direct-to-`main`. - The only deletions are replaced **generic template-example comments** in `methodology.a2ml` (incl. the misleading "Idris2 only" stub). No real data removed. - `coverage.a2ml`'s `total/visited` summary counters were left untouched — I won't fabricate a component denominator. - Stacked on the merged #82; the net diff is the four files above. https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7 --- _Generated by [Claude Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
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.
Complete implementation of WokeLang with:
Lexer (src/lexer/):
Parser (src/parser/):
AST (src/ast/):
Interpreter (src/interpreter/):
CLI (src/main.rs):
Examples: