valence-shell/.github/workflows/lean-verification.yml at a96306425726bd6dcae3d0ddf4e7c30b35c8e67b · hyperpolymath/valence-shell · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
# SPDX-License-Identifier: MPL-2.0
name: Lean Verification Build

on:
  push:
    branches: [main]
    paths:
      - 'proofs/lean4/**'
      - 'impl/rust-cli/src/proof_refs.rs'
      - '.github/workflows/lean-verification.yml'
  pull_request:
    paths:
      - 'proofs/lean4/**'
      - 'impl/ocaml/**'
      - 'impl/rust-cli/**'
  workflow_dispatch:

permissions:
  contents: read

jobs:
  build-lean-extraction:
    name: Build and Test Lean Extraction Pipeline
    runs-on: ubuntu-latest
    timeout-minutes: 30

    steps:
      - name: Checkout code
        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v4

      - name: Install Lean 4
        run: |
          # Download the elan installer pinned to an immutable release tag,
          # verify its SHA-256, then execute it — no `curl | sh`.
          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v3.1.1/elan-init.sh -o elan-init.sh
          echo "f5d473c923c093759ae3839073bec2a58e82cb8bc0e4083930e76090da75b310  elan-init.sh" | sha256sum -c -
          sh elan-init.sh -y
          rm -f elan-init.sh
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Verify Lean installation
        run: |
          source $HOME/.elan/env
          lean --version
          lean --print-prefix
          ls -la $(lean --print-prefix)/lib/lean/libleanshared.so

      - name: Install Rust toolchain
        uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b
        with:
          toolchain: stable

      - name: Cache Lean build
        uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4
        with:
          path: proofs/lean4/.lake
          key: ${{ runner.os }}-lean-${{ hashFiles('proofs/lean4/lakefile.lean', 'proofs/lean4/lean-toolchain') }}

      - name: Build Lean extraction
        run: |
          source $HOME/.elan/env
          cd proofs/lean4
          lake build Extraction

      - name: Verify Lean extraction output
        run: |
          ls -lh proofs/lean4/.lake/build/ir/Extraction.c
          wc -l proofs/lean4/.lake/build/ir/Extraction.c

      - name: Build C wrapper library
        run: |
          source $HOME/.elan/env
          cd impl/ocaml
          lean_prefix="$(lean --print-prefix)"
          lean_include="$lean_prefix/include"
          lean_lib="$lean_prefix/lib/lean"
          gcc -shared -fPIC -o liblean_vsh.so \
            lean_wrapper.c \
            ../../proofs/lean4/.lake/build/ir/Extraction.c \
            -I"$lean_include" \
            -L"$lean_lib" \
            -lleanshared \
            -Wl,-rpath,"$lean_lib"

      - name: Verify shared library
        run: |
          ls -lh impl/ocaml/liblean_vsh.so
          ldd impl/ocaml/liblean_vsh.so
          nm -D impl/ocaml/liblean_vsh.so | grep vsh_safe || echo "Warning: vsh_safe functions not exported"

      - name: Cache Rust build
        uses: Swatinem/rust-cache@7e35be21c2b94d972b1143087fabc27d7dc881ef  # v2
        with:
          workspaces: impl/rust-cli

      - name: Build Rust without Lean (baseline)
        run: |
          cd impl/rust-cli
          cargo build --release
          ls -lh target/release/vsh

      - name: Test Rust without Lean
        run: |
          cd impl/rust-cli
          cargo test
          cargo test --test correspondence_tests
          cargo test --test property_correspondence_tests

      - name: Build Lean model oracle (proof artifact as test oracle)
        run: |
          source $HOME/.elan/env
          cd proofs/lean4
          lake build model_oracle
          ls -lh .lake/build/bin/model_oracle

      - name: Differential correspondence (proven Lean model vs Rust impl)
        run: |
          cd impl/rust-cli
          cargo test --test model_oracle_correspondence -- --nocapture

      - name: Report Rust binary size
        run: |
          echo "Rust binary: $(stat -c%s impl/rust-cli/target/release/vsh) bytes"

      - name: Upload artifacts
        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
        with:
          name: lean-extraction-artifacts
          path: |
            proofs/lean4/.lake/build/ir/Extraction.c
            impl/ocaml/liblean_vsh.so
            impl/rust-cli/target/release/vsh