design and implementation of LS in LS

.github/workflows/ci.yml

@@ -73,6 +73,37 @@ jobs:
       - name: Build
         run: lake build
 
+  # Self-run (DESIGN_LS_IN_LS.md §8): compile and verify the modules listed
+  # in LemmaScript-files.txt with this checkout's toolchain.
+  self-verify:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+
+      - name: Setup Node.js
+        uses: actions/setup-node@v6
+        with:
+          node-version: '24'
+
+      - name: Install tools dependencies
+        working-directory: tools
+        run: npm ci
+
+      - uses: ./.github/actions/setup-dafny
+
+      - name: Self-run
+        run: ./tools/check.sh dafny
+
+      - name: Check self-run artifacts are up to date
+        run: |
+          git diff --exit-code -- 'tools/src/*.dfy.gen' 'tools/src/*.dfy'
+          untracked=$(git ls-files --others --exclude-standard -- 'tools/src/*.dfy.gen')
+          if [ -n "$untracked" ]; then
+            echo "ERROR: Untracked self-run .dfy.gen files:"
+            echo "$untracked"
+            exit 1
+          fi
+
   # Dafny verification of the examples, sharded across runners. The `tools` job
   # enforces drift + additions-only (regen --no-verify); this job runs the actual
   # `dafny verify` in parallel. Files are split by index (i % N == shard), so no

LemmaScript-files.txt

@@ -0,0 +1,5 @@
+tools/src/typedir.ts
+tools/src/ir.ts
+tools/src/peephole.ts 60 --boogie /proverOpt:O:smt.qi.eager_threshold=30
+tools/src/condition-facts.ts
+tools/src/narrow.ts 300 --boogie /proverOpt:O:smt.qi.eager_threshold=30

tools/src/builtins.ts

@@ -153,3 +153,10 @@ export function recognizeBuiltin(objTy: Ty, method: string): BuiltinId | null {
 export function builtinSpec(id: BuiltinId): BuiltinSpec {
   return BUILTINS[id];
 }
+
+/** The one classification bit narrow reads, as a scalar: fn-valued
+ *  `BuiltinSpec` fields don't cross the self-run import boundary (§8.6),
+ *  so the self-applied narrow imports this instead of `builtinSpec`. */
+export function builtinPure(id: BuiltinId): boolean {
+  return BUILTINS[id].pure;
+}