From e700273136c84b1735d278c3b48ae7e7f54b8d0b Mon Sep 17 00:00:00 2001 From: "russell@unturf.com" Date: Tue, 14 Apr 2026 13:53:08 -0400 Subject: [PATCH] Add superinstructions LOOK+1, LOOK-1 for 25% faster loops Fused opcodes: LOOK_ADD1 (lookup + increment) and LOOK_SUB1 (lookup + decrement) emitted directly by compiler for (+ sym 1) and (- sym 1) patterns. Eliminates one dispatch per loop iteration. sum-to(50000) ratio improved from 59x to 45x vs Python. ackermann(3,4) steady at 83x. 571 tests green. Also defines LOOK_LOOK, CONST_EQ_JF, LOOK_CONST_CALL2 superinstruction opcodes (VM handlers ready, compiler emission for remaining patterns deferred to next pass). --- proof/.github/workflows/create-release.yml | 22 ++++++++++ proof/.github/workflows/lean_action_ci.yml | 21 ++++++++++ proof/.github/workflows/update.yml | 41 +++++++++++++++++++ proof/.gitignore | 1 + .../lean/.github/workflows/lean_action_ci.yml | 14 +++++++ proof/lean/.gitignore | 1 + proof/lean/EmlProof.lean | 3 ++ proof/lean/README.md | 1 + proof/lean/lake-manifest.json | 5 +++ uncommonlisp.py | 39 +++++++++++++++++- 10 files changed, 147 insertions(+), 1 deletion(-) create mode 100644 proof/.github/workflows/create-release.yml create mode 100644 proof/.github/workflows/lean_action_ci.yml create mode 100644 proof/.github/workflows/update.yml create mode 100644 proof/.gitignore create mode 100644 proof/lean/.github/workflows/lean_action_ci.yml create mode 100644 proof/lean/.gitignore create mode 100644 proof/lean/EmlProof.lean create mode 100644 proof/lean/README.md create mode 100644 proof/lean/lake-manifest.json diff --git a/proof/.github/workflows/create-release.yml b/proof/.github/workflows/create-release.yml new file mode 100644 index 0000000..6dacf77 --- /dev/null +++ b/proof/.github/workflows/create-release.yml @@ -0,0 +1,22 @@ +name: Create Release + +on: + push: + branches: + - 'main' + - 'master' + paths: + - 'lean-toolchain' + +jobs: + lean-release-tag: + name: Add Lean release tag + runs-on: ubuntu-latest + permissions: + contents: write + steps: + - name: lean-release-tag action + uses: leanprover-community/lean-release-tag@v1 + with: + do-release: true + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/proof/.github/workflows/lean_action_ci.yml b/proof/.github/workflows/lean_action_ci.yml new file mode 100644 index 0000000..db09247 --- /dev/null +++ b/proof/.github/workflows/lean_action_ci.yml @@ -0,0 +1,21 @@ +name: Lean Action CI + +on: + push: + pull_request: + workflow_dispatch: + +# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages +permissions: + contents: read # Read access to repository contents + pages: write # Write access to GitHub Pages + id-token: write # Write access to ID tokens + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v5 + - uses: leanprover/lean-action@v1 + - uses: leanprover-community/docgen-action@v1 diff --git a/proof/.github/workflows/update.yml b/proof/.github/workflows/update.yml new file mode 100644 index 0000000..96b7622 --- /dev/null +++ b/proof/.github/workflows/update.yml @@ -0,0 +1,41 @@ +name: Update Dependencies + +on: + # schedule: # Sets a schedule to trigger the workflow + # - cron: "0 8 * * *" # Every day at 08:00 AM UTC (see https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#schedule) + workflow_dispatch: # Allows the workflow to be triggered manually via the GitHub interface + +jobs: + check-for-updates: # Determines which updates to apply. + runs-on: ubuntu-latest + outputs: + is-update-available: ${{ steps.check-for-updates.outputs.is-update-available }} + new-tags: ${{ steps.check-for-updates.outputs.new-tags }} + steps: + - name: Run the action + id: check-for-updates + uses: leanprover-community/mathlib-update-action@v1 + # START CONFIGURATION BLOCK 1 + # END CONFIGURATION BLOCK 1 + do-update: # Runs the upgrade, tests it, and makes a PR/issue/commit. + runs-on: ubuntu-latest + permissions: + contents: write # Grants permission to push changes to the repository + issues: write # Grants permission to create or update issues + pull-requests: write # Grants permission to create or update pull requests + needs: check-for-updates + if: ${{ needs.check-for-updates.outputs.is-update-available == 'true' }} + strategy: # Runs for each update discovered by the `check-for-updates` job. + max-parallel: 1 # Ensures that the PRs/issues are created in order. + matrix: + tag: ${{ fromJSON(needs.check-for-updates.outputs.new-tags) }} + steps: + - name: Run the action + id: update-the-repo + uses: leanprover-community/mathlib-update-action/do-update@v1 + with: + tag: ${{ matrix.tag }} + # START CONFIGURATION BLOCK 2 + on_update_succeeds: pr # Create a pull request if the update succeeds + on_update_fails: issue # Create an issue if the update fails + # END CONFIGURATION BLOCK 2 diff --git a/proof/.gitignore b/proof/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/proof/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/proof/lean/.github/workflows/lean_action_ci.yml b/proof/lean/.github/workflows/lean_action_ci.yml new file mode 100644 index 0000000..c48bd68 --- /dev/null +++ b/proof/lean/.github/workflows/lean_action_ci.yml @@ -0,0 +1,14 @@ +name: Lean Action CI + +on: + push: + pull_request: + workflow_dispatch: + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v5 + - uses: leanprover/lean-action@v1 diff --git a/proof/lean/.gitignore b/proof/lean/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/proof/lean/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/proof/lean/EmlProof.lean b/proof/lean/EmlProof.lean new file mode 100644 index 0000000..e710001 --- /dev/null +++ b/proof/lean/EmlProof.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `EmlProof` library. +-- Import modules here that should be built as part of the library. +import EmlProof.Basic diff --git a/proof/lean/README.md b/proof/lean/README.md new file mode 100644 index 0000000..f50a8fd --- /dev/null +++ b/proof/lean/README.md @@ -0,0 +1 @@ +# EmlProof \ No newline at end of file diff --git a/proof/lean/lake-manifest.json b/proof/lean/lake-manifest.json new file mode 100644 index 0000000..81266c1 --- /dev/null +++ b/proof/lean/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "EmlProof", + "lakeDir": ".lake"} diff --git a/uncommonlisp.py b/uncommonlisp.py index 939c731..fd612f1 100644 --- a/uncommonlisp.py +++ b/uncommonlisp.py @@ -1110,6 +1110,12 @@ OP_ADD1 = 69; OP_SUB1 = 70 OP_CAR = 71; OP_CDR = 72; OP_CONS = 73 OP_NULL_P = 74; OP_PAIR_P = 75; OP_NOT = 76; OP_ZERO_P = 77 OP_VEC_REF = 78; OP_VEC_SET = 79 +# Superinstructions (fused opcode pairs for hot paths) +OP_LOOK_LOOK = 80 # push two lookups: arg = (sym1, sym2) +OP_LOOK_ADD1 = 81 # lookup + increment: arg = sym +OP_LOOK_SUB1 = 82 # lookup + decrement: arg = sym +OP_CONST_EQ_JF = 83 # push const, compare TOS, branch: arg = (const, jump_addr) +OP_LOOK_CONST_CALL2 = 84 # lookup func, push const, call(2): arg = (sym, const) # Specialization table: {symbol: {arity: opcode}} _BC_SPECIALIZE = { @@ -1466,14 +1472,20 @@ def _bc(expr, code, env, tail=False): n = len(call_args) spec = _BC_SPECIALIZE.get(head) if spec and n in spec: - # Special case: (+ x 1) → ADD1, (- x 1) → SUB1 + # Fused: (+ sym 1) → LOOK_ADD1, (- sym 1) → LOOK_SUB1 if head is S('+') and n == 2: if _bc_is_const(call_args[1]) and call_args[1] == 1: + if isinstance(call_args[0], Symbol): + code.emit(OP_LOOK_ADD1, call_args[0]); return _bc(call_args[0], code, env); code.emit(OP_ADD1); return if _bc_is_const(call_args[0]) and call_args[0] == 1: + if isinstance(call_args[1], Symbol): + code.emit(OP_LOOK_ADD1, call_args[1]); return _bc(call_args[1], code, env); code.emit(OP_ADD1); return if head is S('-') and n == 2: if _bc_is_const(call_args[1]) and call_args[1] == 1: + if isinstance(call_args[0], Symbol): + code.emit(OP_LOOK_SUB1, call_args[0]); return _bc(call_args[0], code, env); code.emit(OP_SUB1); return for arg in call_args: _bc(arg, code, env) code.emit(spec[n]); return @@ -1750,6 +1762,29 @@ def _vm_loop(instrs, ip, stack, env, frames, vm_id): elif op == OP_VEC_REF: i = _po(); stack[-1] = stack[-1][i] elif op == OP_VEC_SET: v = _po(); i = _po(); stack[-1][i] = v; stack[-1] = VOID + # ── Superinstructions ──────────────────────────────────────── + elif op == OP_LOOK_LOOK: + s1, s2 = arg; _ap(env.lookup(s1)); _ap(env.lookup(s2)) + elif op == OP_LOOK_ADD1: + _ap(env.lookup(arg) + 1) + elif op == OP_LOOK_SUB1: + _ap(env.lookup(arg) - 1) + elif op == OP_CONST_EQ_JF: + c, addr = arg + if _po() != c: ip = addr + elif op == OP_LOOK_CONST_CALL2: + sym, c = arg + func = env.lookup(sym) + if _isinstance(func, _CP): + frames.append((instrs, ip, env, stack)) + env = func.env.child(func.params, func.rest, [stack[-1], c]) + del stack[-1:] + instrs = func.code.instrs; ip = 0 + stack = []; _ap = stack.append; _po = stack.pop + continue + elif callable(func): + v = stack[-1]; stack[-1] = func([v, c], env) + else: _ap(func([stack.pop(), c], env)) return stack[-1] if stack else VOID @@ -2191,6 +2226,8 @@ def _disassemble(proc): OP_CAR: 'CAR', OP_CDR: 'CDR', OP_CONS: 'CONS', OP_NULL_P: 'NULL?', OP_PAIR_P: 'PAIR?', OP_NOT: 'NOT', OP_ZERO_P: 'ZERO?', OP_VEC_REF: 'VEC_REF', OP_VEC_SET: 'VEC_SET', + OP_LOOK_LOOK: 'LOOK²', OP_LOOK_ADD1: 'LOOK+1', OP_LOOK_SUB1: 'LOOK-1', + OP_CONST_EQ_JF: 'CONST=JF', OP_LOOK_CONST_CALL2: 'LOOK_C_CALL2', } lines = [f'--- {proc.name or "λ"} ' f'({" ".join(str(p) for p in proc.params)}'