valence-shell/.github/workflows/lean-verification.yml at 85d8eb5f8aab7639c331e2054da7a7977a872e81 · 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
# 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: 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