verity/.github/workflows/evmyullean-fork-conformance.yml at main · lfglabs-dev/verity · 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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
name: EVMYulLean fork conformance

# Weekly probe that the pinned lfglabs-dev/EVMYulLean fork still
# satisfies Verity's bridge assumptions: the fork audit and native lowering
# report artifacts are in sync, all universal bridge lemmas still build, the
# native transition harness still builds, emitted dispatcher native coverage still passes, the
# public EndToEnd EVMYulLean target still builds, and all 0 concrete
# `native_decide` bridge-equivalence tests still pass.
#
# On scheduled or manual failure the probe job exits red and the
# follow-up job opens or updates a tracking issue.

on:
  schedule:
    # Monday 07:23 UTC — off the :00/:30 minute mark to avoid
    # scheduler pile-up with other weekly jobs.
    - cron: '23 7 * * 1'
  workflow_dispatch:
  push:
    branches: [main]
    paths:
      - '.github/workflows/evmyullean-fork-conformance.yml'
      - 'Makefile'
      - 'Compiler/Proofs/EndToEnd.lean'
      - 'scripts/generate_evmyullean_native_lowering_report.py'
      - 'scripts/generate_evmyullean_fork_audit.py'
      - 'scripts/test_evmyullean_fork_conformance_workflow.py'
      - 'artifacts/evmyullean_fork_audit.json'
      - 'artifacts/evmyullean_native_lowering_report.json'
      - 'lake-manifest.json'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeLowering.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSignedArithSpec.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanStateBridge.lean'
  pull_request:
    paths:
      - '.github/workflows/evmyullean-fork-conformance.yml'
      - 'Makefile'
      - 'Compiler/Proofs/EndToEnd.lean'
      - 'scripts/generate_evmyullean_native_lowering_report.py'
      - 'scripts/generate_evmyullean_fork_audit.py'
      - 'scripts/test_evmyullean_fork_conformance_workflow.py'
      - 'artifacts/evmyullean_fork_audit.json'
      - 'artifacts/evmyullean_native_lowering_report.json'
      - 'lake-manifest.json'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeLowering.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeTest.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSignedArithSpec.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean'
      - 'Compiler/Proofs/YulGeneration/Backends/EvmYulLeanStateBridge.lean'

permissions:
  contents: read

concurrency:
  group: evmyullean-fork-conformance-${{ github.ref }}
  cancel-in-progress: ${{ github.event_name != 'schedule' }}

jobs:
  probe:
    runs-on: ubuntu-latest
    timeout-minutes: 60
    steps:
      - uses: actions/checkout@v6
        with:
          submodules: recursive

      - name: Setup Lean
        uses: ./.github/actions/setup-lean
        with:
          cache-key-prefix: lake

      - name: Run EVMYulLean fork conformance probe
        id: probe
        run: make test-evmyullean-fork

      - name: Report probe outcome
        if: always()
        run: |
          if [ "${{ steps.probe.outcome }}" = "success" ]; then
            echo "::notice::EVMYulLean fork conformance probe passed."
          else
            echo "::error::EVMYulLean fork conformance probe failed. Investigate locally with 'make test-evmyullean-fork'."
          fi

  open-drift-issue:
    needs: probe
    if: always() && needs.probe.result == 'failure' && (github.event_name == 'schedule' || github.event_name == 'workflow_dispatch')
    runs-on: ubuntu-latest
    permissions:
      contents: read
      issues: write
    steps:
      - name: Open or update drift issue
        uses: actions/github-script@v7
        with:
          script: |
            const marker = "<!-- evmyullean-fork-conformance-failure -->";
            const owner = context.repo.owner;
            const repo = context.repo.repo;
            const runUrl = `${context.serverUrl}/${owner}/${repo}/actions/runs/${context.runId}`;
            const title = "EVMYulLean fork conformance probe failed";
            const bodyLines = [
              marker,
              "The EVMYulLean fork conformance probe failed.",
              "",
              `Run: ${runUrl}`,
              `Workflow: ${context.workflow}`,
              `Ref: ${context.ref}`,
              `SHA: ${context.sha}`,
              "",
              "Local triage:",
              "```bash",
              "make test-evmyullean-fork",
              "```",
              "",
              "This guard checks the pinned EVMYulLean fork audit, checks the native lowering report, rebuilds the native transition harness, and the public EndToEnd target, and runs the concrete bridge-equivalence tests."
            ];
            const body = bodyLines.join("\n");

            const query = `repo:${owner}/${repo} is:issue is:open in:title "${title}"`;
            const search = await github.rest.search.issuesAndPullRequests({
              q: query,
              per_page: 10
            });
            const existing = search.data.items.find((item) =>
              item.title === title && !item.pull_request
            );

            if (existing) {
              await github.rest.issues.createComment({
                owner,
                repo,
                issue_number: existing.number,
                body
              });
              core.notice(`Updated existing conformance issue #${existing.number}.`);
            } else {
              const created = await github.rest.issues.create({
                owner,
                repo,
                title,
                body
              });
              core.notice(`Created conformance issue #${created.data.number}.`);
            }