Formally verified expRayToWad

.github/actions/build-ln-proof/action.yml

@@ -0,0 +1,39 @@
+name: Build LnProof
+description: >-
+  Generate the LnWrapper EVMYulLean artifacts and certificate literals, then
+  build the LnProof Lean package. Requires Foundry, solc 0.8.34, the pinned
+  Lean toolchain, and a built formal/yul importer.
+
+runs:
+  using: composite
+  steps:
+    - name: Generate EVMYulLean artifacts from compiled LnWrapper Yul IR
+      shell: bash
+      run: |
+        ./formal/yul/generate_from_forge.sh \
+          ln \
+          src/wrappers/LnWrapper.sol:LnWrapper \
+          formal/ln/LnProof/LnProof/LnYul.lean \
+          0.8.34
+
+    - name: Fetch Ln proof dependency cache
+      uses: ./.github/actions/fetch-lean-cache
+      with:
+        working-directory: formal/ln/LnProof
+
+    - name: Generate Ln certificate artifacts
+      shell: bash
+      working-directory: formal/ln/LnProof
+      run: |
+        lake build LnProof.Floor.CertDefs Common.Foundation.KroneckerShift LnProof.Floor.Consts Common.GenCover
+        lake env lean GenFloorCertLit.lean
+        lake build LnProof.Cert.FloorCertLit
+        lake env lean GenCover.lean
+        lake env lean GenErr1.lean
+        lake build LnProof.Error.Core
+        lake env lean GenErrLit.lean
+
+    - name: Build Ln proof package
+      shell: bash
+      working-directory: formal/ln/LnProof
+      run: lake build

.github/actions/fetch-lean-cache/action.yml

@@ -0,0 +1,25 @@
+name: Fetch Lean build cache
+description: >-
+  Run `lake exe cache get` for a Lean package, first materializing the
+  ProofWidgets release layout it requires.
+
+inputs:
+  working-directory:
+    description: Directory containing the Lean package's lakefile.
+    required: true
+
+runs:
+  using: composite
+  steps:
+    - name: Fetch Lean build cache
+      shell: bash
+      working-directory: ${{ inputs.working-directory }}
+      run: |
+        # Mathlib's `cache get` fetches the ProofWidgets cloud release, then
+        # deletes its `lib`/`ir` outputs and fails if they are missing. Fetch
+        # the release and ensure those directories exist before it runs.
+        lake build proofwidgets:release
+        mkdir -p \
+          .lake/packages/proofwidgets/.lake/build/lib \
+          .lake/packages/proofwidgets/.lake/build/ir
+        lake exe cache get

.github/actions/setup-formal/action.yml

@@ -0,0 +1,83 @@
+name: Set up the formal toolchain
+description: >-
+  The shared prefix of every *-formal workflow: install Foundry and the pinned
+  Lean toolchain, restore the Lean build cache, install solc 0.8.34, fetch the
+  Yul importer's Mathlib cache, and build the Yul importer. Requires the
+  repository (with submodules) to be checked out first.
+
+inputs:
+  lean-toolchain-files:
+    description: >-
+      Newline-separated lean-toolchain file paths. The first names the
+      toolchain to install; every subsequent file must pin the same toolchain.
+    required: true
+  cache-name:
+    description: Per-proof segment of the Lean build cache key (e.g. exp-formal).
+    required: true
+  cache-paths:
+    description: >-
+      Newline-separated proof-package build directories to cache, in addition
+      to the Yul importer's and EVMYulLean's.
+    required: true
+  cache-hash-globs:
+    description: >-
+      Newline-separated hashFiles patterns covering the proof packages' lake
+      configuration and Lean sources, hashed into the cache key alongside the
+      Yul importer's and EVMYulLean's.
+    required: true
+
+runs:
+  using: composite
+  steps:
+    - name: Install Foundry
+      uses: foundry-rs/foundry-toolchain@v1
+      with:
+        version: v1.5.1
+
+    - name: Install pinned Lean toolchain
+      shell: bash
+      env:
+        LEAN_TOOLCHAIN_FILES: ${{ inputs.lean-toolchain-files }}
+      run: |
+        curl https://raw.githubusercontent.com/leanprover/elan/917c18d0ad52f649c2603dc8b973f5b9fa5f8f43/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+        LEAN_TOOLCHAIN=''
+        while IFS= read -r file; do
+          [ -n "$file" ] || continue
+          if [ -z "$LEAN_TOOLCHAIN" ]; then
+            LEAN_TOOLCHAIN="$(cat "$file")"
+          else
+            test "$LEAN_TOOLCHAIN" = "$(cat "$file")"
+          fi
+        done <<< "$LEAN_TOOLCHAIN_FILES"
+        "$HOME/.elan/bin/elan" toolchain install "$LEAN_TOOLCHAIN"
+        "$HOME/.elan/bin/elan" default "$LEAN_TOOLCHAIN"
+
+    - name: Restore Lean build cache
+      uses: actions/cache@v4
+      with:
+        path: |
+          formal/yul/.lake/build
+          formal/yul/.lake/packages/*/.lake/build
+          lib/EVMYulLean/.lake/build
+          ${{ inputs.cache-paths }}
+        key: ${{ runner.os }}-${{ inputs.cache-name }}-lean-${{ hashFiles('formal/yul/lean-toolchain', 'formal/yul/lakefile.toml', 'formal/yul/lake-manifest.json', 'formal/yul/FormalYul/**/*.lean', 'lib/EVMYulLean/**/*.lean') }}-${{ hashFiles(inputs.cache-hash-globs) }}
+        restore-keys: |
+          ${{ runner.os }}-${{ inputs.cache-name }}-lean-
+          ${{ runner.os }}-formal-lean-
+
+    - name: Install solc 0.8.34
+      shell: bash
+      run: forge build -- src/chains/Mainnet/TakerSubmitted.sol
+      env:
+        FOUNDRY_SOLC_VERSION: 0.8.34
+
+    - name: Fetch Mathlib cache
+      uses: ./.github/actions/fetch-lean-cache
+      with:
+        working-directory: formal/yul
+
+    - name: Build Yul importer
+      shell: bash
+      working-directory: formal/yul
+      run: lake build FormalYul.Preservation yul_importer

.github/workflows/cbrt-formal.yml

@@ -12,6 +12,10 @@ on:
       - formal/yul/**
       - foundry.toml
       - remappings.txt
+      - .gitmodules
+      - lib/EVMYulLean
+      - .github/actions/setup-formal/**
+      - .github/actions/fetch-lean-cache/**
       - .github/workflows/cbrt-formal.yml
   pull_request:
     paths:
@@ -22,6 +26,10 @@ on:
       - formal/yul/**
       - foundry.toml
       - remappings.txt
+      - .gitmodules
+      - lib/EVMYulLean
+      - .github/actions/setup-formal/**
+      - .github/actions/fetch-lean-cache/**
       - .github/workflows/cbrt-formal.yml
 
 jobs:
@@ -32,50 +40,17 @@ jobs:
         with:
           submodules: recursive
 
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@v1
-
-      - name: Install pinned Lean toolchain
-        run: |
-          curl https://raw.githubusercontent.com/leanprover/elan/917c18d0ad52f649c2603dc8b973f5b9fa5f8f43/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-          LEAN_TOOLCHAIN="$(cat formal/cbrt/CbrtProof/lean-toolchain)"
-          "$HOME/.elan/bin/elan" toolchain install "$LEAN_TOOLCHAIN"
-          "$HOME/.elan/bin/elan" default "$LEAN_TOOLCHAIN"
-
-      - name: Restore Lean build cache
-        uses: actions/cache@v4
+      - name: Set up the formal toolchain
+        uses: ./.github/actions/setup-formal
         with:
-          path: |
-            formal/yul/.lake/build
-            formal/yul/.lake/packages/*/.lake/build
-            lib/EVMYulLean/.lake/build
+          lean-toolchain-files: formal/cbrt/CbrtProof/lean-toolchain
+          cache-name: cbrt-formal
+          cache-paths: |
             formal/cbrt/CbrtProof/.lake/build
-          key: ${{ runner.os }}-cbrt-formal-lean-${{ hashFiles('formal/yul/lean-toolchain', 'formal/yul/lakefile.toml', 'formal/yul/lake-manifest.json', 'formal/cbrt/CbrtProof/lakefile.toml', 'formal/cbrt/CbrtProof/lake-manifest.json', 'formal/yul/FormalYul/**/*.lean', 'formal/cbrt/CbrtProof/**/*.lean', 'lib/EVMYulLean/**/*.lean') }}
-          restore-keys: |
-            ${{ runner.os }}-cbrt-formal-lean-
-            ${{ runner.os }}-formal-lean-
-
-      - name: Install solc 0.8.34
-        run: forge build -- src/chains/Mainnet/TakerSubmitted.sol
-        env:
-          FOUNDRY_SOLC_VERSION: 0.8.34
-
-      - name: Fetch Mathlib cache
-        working-directory: formal/yul
-        run: |
-          # Mathlib's `cache get` fetches the ProofWidgets cloud release, then
-          # deletes its `lib`/`ir` outputs and fails if they are missing. Fetch
-          # the release and ensure those directories exist before it runs.
-          lake build proofwidgets:release
-          mkdir -p \
-            .lake/packages/proofwidgets/.lake/build/lib \
-            .lake/packages/proofwidgets/.lake/build/ir
-          lake exe cache get
-
-      - name: Build Yul importer
-        working-directory: formal/yul
-        run: lake build FormalYul.Preservation yul_importer
+          cache-hash-globs: |
+            formal/cbrt/CbrtProof/lakefile.toml
+            formal/cbrt/CbrtProof/lake-manifest.json
+            formal/cbrt/CbrtProof/**/*.lean
 
       - name: Generate EVMYulLean artifacts from compiled CbrtWrapper Yul IR
         run: |
@@ -91,16 +66,9 @@ jobs:
             --output formal/cbrt/CbrtProof/CbrtProof/FiniteCert.lean
 
       - name: Fetch proof dependency cache
-        working-directory: formal/cbrt/CbrtProof
-        run: |
-          # Mathlib's `cache get` fetches the ProofWidgets cloud release, then
-          # deletes its `lib`/`ir` outputs and fails if they are missing. Fetch
-          # the release and ensure those directories exist before it runs.
-          lake build proofwidgets:release
-          mkdir -p \
-            .lake/packages/proofwidgets/.lake/build/lib \
-            .lake/packages/proofwidgets/.lake/build/ir
-          lake exe cache get
+        uses: ./.github/actions/fetch-lean-cache
+        with:
+          working-directory: formal/cbrt/CbrtProof
 
       - name: Build Cbrt proof package
         working-directory: formal/cbrt/CbrtProof

.github/workflows/cbrt512-formal.yml

@@ -19,6 +19,10 @@ on:
       - formal/yul/**
       - foundry.toml
       - remappings.txt
+      - .gitmodules
+      - lib/EVMYulLean
+      - .github/actions/setup-formal/**
+      - .github/actions/fetch-lean-cache/**
       - .github/workflows/cbrt512-formal.yml
   pull_request:
     paths:
@@ -36,6 +40,10 @@ on:
       - formal/yul/**
       - foundry.toml
       - remappings.txt
+      - .gitmodules
+      - lib/EVMYulLean
+      - .github/actions/setup-formal/**
+      - .github/actions/fetch-lean-cache/**
       - .github/workflows/cbrt512-formal.yml
 
 jobs:
@@ -46,52 +54,23 @@ jobs:
         with:
           submodules: recursive
 
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@v1
-
-      - name: Install pinned Lean toolchain
-        run: |
-          curl https://raw.githubusercontent.com/leanprover/elan/917c18d0ad52f649c2603dc8b973f5b9fa5f8f43/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-          LEAN_TOOLCHAIN="$(cat formal/cbrt/Cbrt512Proof/lean-toolchain)"
-          test "$LEAN_TOOLCHAIN" = "$(cat formal/cbrt/CbrtProof/lean-toolchain)"
-          "$HOME/.elan/bin/elan" toolchain install "$LEAN_TOOLCHAIN"
-          "$HOME/.elan/bin/elan" default "$LEAN_TOOLCHAIN"
-
-      - name: Restore Lean build cache
-        uses: actions/cache@v4
+      - name: Set up the formal toolchain
+        uses: ./.github/actions/setup-formal
         with:
-          path: |
-            formal/yul/.lake/build
-            formal/yul/.lake/packages/*/.lake/build
-            lib/EVMYulLean/.lake/build
+          lean-toolchain-files: |
+            formal/cbrt/Cbrt512Proof/lean-toolchain
+            formal/cbrt/CbrtProof/lean-toolchain
+          cache-name: cbrt512-formal
+          cache-paths: |
             formal/cbrt/CbrtProof/.lake/build
             formal/cbrt/Cbrt512Proof/.lake/build
-          key: ${{ runner.os }}-cbrt512-formal-lean-${{ hashFiles('formal/yul/lean-toolchain', 'formal/yul/lakefile.toml', 'formal/yul/lake-manifest.json', 'formal/cbrt/CbrtProof/lakefile.toml', 'formal/cbrt/CbrtProof/lake-manifest.json', 'formal/cbrt/Cbrt512Proof/lakefile.toml', 'formal/cbrt/Cbrt512Proof/lake-manifest.json', 'formal/yul/FormalYul/**/*.lean', 'formal/cbrt/CbrtProof/**/*.lean', 'formal/cbrt/Cbrt512Proof/**/*.lean', 'lib/EVMYulLean/**/*.lean') }}
-          restore-keys: |
-            ${{ runner.os }}-cbrt512-formal-lean-
-            ${{ runner.os }}-formal-lean-
-
-      - name: Install solc 0.8.34
-        run: forge build -- src/chains/Mainnet/TakerSubmitted.sol
-        env:
-          FOUNDRY_SOLC_VERSION: 0.8.34
-
-      - name: Fetch Mathlib cache
-        working-directory: formal/yul
-        run: |
-          # Mathlib's `cache get` fetches the ProofWidgets cloud release, then
-          # deletes its `lib`/`ir` outputs and fails if they are missing. Fetch
-          # the release and ensure those directories exist before it runs.
-          lake build proofwidgets:release
-          mkdir -p \
-            .lake/packages/proofwidgets/.lake/build/lib \
-            .lake/packages/proofwidgets/.lake/build/ir
-          lake exe cache get
-
-      - name: Build Yul importer
-        working-directory: formal/yul
-        run: lake build FormalYul.Preservation yul_importer
+          cache-hash-globs: |
+            formal/cbrt/CbrtProof/lakefile.toml
+            formal/cbrt/CbrtProof/lake-manifest.json
+            formal/cbrt/Cbrt512Proof/lakefile.toml
+            formal/cbrt/Cbrt512Proof/lake-manifest.json
+            formal/cbrt/CbrtProof/**/*.lean
+            formal/cbrt/Cbrt512Proof/**/*.lean
 
       - name: Generate 512-bit EVMYulLean artifacts from compiled Cbrt512Wrapper Yul IR
         run: |
@@ -107,16 +86,9 @@ jobs:
             --output formal/cbrt/CbrtProof/CbrtProof/FiniteCert.lean
 
       - name: Fetch proof dependency cache
-        working-directory: formal/cbrt/Cbrt512Proof
-        run: |
-          # Mathlib's `cache get` fetches the ProofWidgets cloud release, then
-          # deletes its `lib`/`ir` outputs and fails if they are missing. Fetch
-          # the release and ensure those directories exist before it runs.
-          lake build proofwidgets:release
-          mkdir -p \
-            .lake/packages/proofwidgets/.lake/build/lib \
-            .lake/packages/proofwidgets/.lake/build/ir
-          lake exe cache get
+        uses: ./.github/actions/fetch-lean-cache
+        with:
+          working-directory: formal/cbrt/Cbrt512Proof
 
       - name: Build Cbrt512 proof package
         working-directory: formal/cbrt/Cbrt512Proof