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

@@ -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 }}

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

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

proof/.gitignore

@@ -0,0 +1 @@
+/.lake

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

proof/lean/.gitignore

@@ -0,0 +1 @@
+/.lake

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

proof/lean/README.md

@@ -0,0 +1 @@
+# EmlProof

proof/lean/lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "EmlProof",
+ "lakeDir": ".lake"}

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)}'