Skip to content

Commit 356e866

Browse files
myfreessmyfreess
committed
add minimal initial impl
1 parent d0c0700 commit 356e866

359 files changed

Lines changed: 161222 additions & 438 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.gitattributes‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
**/pkg.generated.mbti whitespace=-blank-at-eof

‎.github/workflows/check.yml‎

Lines changed: 68 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -16,56 +16,86 @@ concurrency:
1616
cancel-in-progress: true
1717

1818
jobs:
19-
stable-build:
20-
name: stable
19+
environment:
20+
name: resolve reference environment
2121
runs-on: ubuntu-24.04
22-
container:
23-
image: ghcr.io/${{ github.repository }}-why3:1.7.2
24-
credentials:
25-
username: ${{ github.actor }}
26-
password: ${{ secrets.GITHUB_TOKEN }}
22+
outputs:
23+
image: ${{ steps.lock.outputs.image }}
2724
steps:
28-
- uses: actions/checkout@v6
25+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
2926

30-
- name: Trust checkout workspace
31-
run: git config --global --add safe.directory "$GITHUB_WORKSPACE"
27+
- name: Read the unique environment lock
28+
id: lock
29+
run: |
30+
image="$(node -e '
31+
const { readEnvironmentLock } = require("./tools/why3_reference/reference_environment.cjs");
32+
const lock = readEnvironmentLock();
33+
process.stdout.write(`${lock.image.repository}@${lock.image.digest}`);
34+
')"
35+
echo "image=$image" >> "$GITHUB_OUTPUT"
3236
33-
- name: Setup Moon
34-
uses: moonbit-community/setup-moonbit@main
35-
with:
36-
version: stable
37+
project:
38+
name: project
39+
runs-on: ubuntu-24.04
40+
steps:
41+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
3742

38-
- name: moon update
39-
run: moon update
43+
- name: Set up MoonBit stable
44+
uses: moonbit-community/setup-moonbit@04293a8a813bfd4b6c2fce22701b52ae1050d100
45+
with:
46+
version: stable
4047

41-
- name: Show tool versions
48+
- name: Install the non-contractual project prover
4249
run: |
43-
moon version --all
44-
moonrun --version
50+
sudo apt-get update
51+
sudo apt-get install --yes z3
4552
46-
- name: Show Why3 version
47-
run: why3 --version
53+
- name: Bootstrap and check the project
54+
run: |
55+
node tools/run.mjs bootstrap
56+
node tools/run.mjs project
4857
49-
- name: Check all targets
50-
run: moon check --target all --warn-list +73
58+
reference:
59+
name: fixed reference
60+
needs:
61+
- environment
62+
- project
63+
runs-on: ubuntu-24.04
64+
container:
65+
image: ${{ needs.environment.outputs.image }}
66+
credentials:
67+
username: ${{ github.actor }}
68+
password: ${{ secrets.GITHUB_TOKEN }}
69+
env:
70+
WHY3_REFERENCE_CACHE_DIR: ${{ github.workspace }}/.cache/why3-reference
71+
WHY3_REFERENCE_CONTEXT_DIR: ${{ github.workspace }}/_build/reference-context
72+
steps:
73+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
5174

52-
- name: Test all targets
53-
run: |
54-
moon test --target all --serial --release
55-
moon test --target all --serial
75+
- name: Trust checkout workspace
76+
run: git config --global --add safe.directory "$GITHUB_WORKSPACE"
5677

57-
- name: Test Node.js tools
58-
run: node --test tools/*.test.mjs
78+
- name: Restore patched Why3 runtime
79+
uses: actions/cache@5a3ec84eff668545956fd18022155c47e93e2684
80+
with:
81+
path: ${{ env.WHY3_REFERENCE_CACHE_DIR }}
82+
key: reference-runtime-${{ runner.os }}-${{ hashFiles('tools/contracts/reference-environment-lock-v1.json', 'tools/why3_reference/reference_runtime.mjs', 'tools/why3_reference/patches/driver-trace.patch') }}
5983

60-
- name: Check Why3 fixtures
61-
run: node tools/check_why3_fixtures.mjs
84+
- name: Set up MoonBit stable
85+
uses: moonbit-community/setup-moonbit@04293a8a813bfd4b6c2fce22701b52ae1050d100
86+
with:
87+
version: stable
6288

63-
- name: Check generated interfaces
89+
- name: Check the fixed reference
6490
run: |
65-
moon info
66-
git diff --exit-code
91+
node tools/run.mjs bootstrap
92+
node tools/run.mjs reference \
93+
--why3-archive "$WHY3_REFERENCE_ARCHIVE"
6794
68-
- name: Check formatting
69-
run: |
70-
moon fmt
71-
git diff --exit-code
95+
- name: Upload resolved environment provenance
96+
if: always()
97+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
98+
with:
99+
name: reference-context-${{ github.sha }}
100+
path: ${{ env.WHY3_REFERENCE_CONTEXT_DIR }}
101+
if-no-files-found: warn

‎.github/workflows/nightly-reference.yml‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
name: nightly-reference
2+
3+
on:
4+
schedule:
5+
- cron: "17 2 * * *"
6+
workflow_dispatch:
7+
8+
permissions:
9+
contents: read
10+
packages: read
11+
12+
concurrency:
13+
group: ${{ github.workflow }}-${{ github.ref }}
14+
cancel-in-progress: true
15+
16+
jobs:
17+
environment:
18+
name: resolve reference environment
19+
runs-on: ubuntu-24.04
20+
outputs:
21+
image: ${{ steps.lock.outputs.image }}
22+
steps:
23+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
24+
- id: lock
25+
name: Read the unique environment lock
26+
run: |
27+
image="$(node -e '
28+
const { readEnvironmentLock } = require("./tools/why3_reference/reference_environment.cjs");
29+
const lock = readEnvironmentLock();
30+
process.stdout.write(`${lock.image.repository}@${lock.image.digest}`);
31+
')"
32+
echo "image=$image" >> "$GITHUB_OUTPUT"
33+
34+
reference:
35+
name: full layered reference
36+
needs: environment
37+
runs-on: ubuntu-24.04
38+
container:
39+
image: ${{ needs.environment.outputs.image }}
40+
credentials:
41+
username: ${{ github.actor }}
42+
password: ${{ secrets.GITHUB_TOKEN }}
43+
env:
44+
WHY3_REFERENCE_CACHE_DIR: ${{ github.workspace }}/.cache/why3-reference
45+
WHY3_REFERENCE_CONTEXT_DIR: ${{ github.workspace }}/_build/reference-context
46+
steps:
47+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
48+
49+
- name: Trust checkout workspace
50+
run: git config --global --add safe.directory "$GITHUB_WORKSPACE"
51+
52+
- name: Restore patched Why3 runtime
53+
uses: actions/cache@5a3ec84eff668545956fd18022155c47e93e2684
54+
with:
55+
path: ${{ env.WHY3_REFERENCE_CACHE_DIR }}
56+
key: reference-runtime-${{ runner.os }}-${{ hashFiles('tools/contracts/reference-environment-lock-v1.json', 'tools/why3_reference/reference_runtime.mjs', 'tools/why3_reference/patches/driver-trace.patch') }}
57+
58+
- name: Set up MoonBit stable
59+
uses: moonbit-community/setup-moonbit@04293a8a813bfd4b6c2fce22701b52ae1050d100
60+
with:
61+
version: stable
62+
63+
- name: Run complete reference
64+
run: |
65+
node tools/run.mjs bootstrap
66+
node tools/run.mjs reference \
67+
--why3-archive "$WHY3_REFERENCE_ARCHIVE"
68+
69+
- name: Regenerate and compare PR baselines
70+
run: |
71+
node tools/run.mjs baselines candidate \
72+
--records "$RUNNER_TEMP/nightly-pr-records" \
73+
--result "$RUNNER_TEMP/nightly-prover-result.json" \
74+
--compare
75+
76+
- name: Upload full nightly records and provenance
77+
if: always()
78+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
79+
with:
80+
name: nightly-reference-${{ github.sha }}
81+
path: |
82+
${{ runner.temp }}/nightly-pr-records
83+
${{ runner.temp }}/nightly-prover-result.json
84+
${{ env.WHY3_REFERENCE_CONTEXT_DIR }}
85+
if-no-files-found: warn

‎.github/workflows/update-baselines.yml‎

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
name: update-baselines
2+
3+
on:
4+
workflow_dispatch:
5+
inputs:
6+
mode:
7+
description: Generate a candidate or explicitly verify and promote it in the checkout
8+
required: true
9+
default: candidate
10+
type: choice
11+
options:
12+
- candidate
13+
- promote
14+
15+
permissions:
16+
contents: read
17+
packages: read
18+
19+
concurrency:
20+
group: ${{ github.workflow }}-${{ github.ref }}
21+
cancel-in-progress: false
22+
23+
jobs:
24+
environment:
25+
name: resolve reference environment
26+
runs-on: ubuntu-24.04
27+
outputs:
28+
image: ${{ steps.lock.outputs.image }}
29+
steps:
30+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
31+
- id: lock
32+
name: Read the unique environment lock
33+
run: |
34+
image="$(node -e '
35+
const { readEnvironmentLock } = require("./tools/why3_reference/reference_environment.cjs");
36+
const lock = readEnvironmentLock();
37+
process.stdout.write(`${lock.image.repository}@${lock.image.digest}`);
38+
')"
39+
echo "image=$image" >> "$GITHUB_OUTPUT"
40+
41+
update:
42+
name: ${{ inputs.mode }} baselines
43+
needs: environment
44+
runs-on: ubuntu-24.04
45+
container:
46+
image: ${{ needs.environment.outputs.image }}
47+
credentials:
48+
username: ${{ github.actor }}
49+
password: ${{ secrets.GITHUB_TOKEN }}
50+
env:
51+
WHY3_REFERENCE_CACHE_DIR: ${{ github.workspace }}/.cache/why3-reference
52+
WHY3_REFERENCE_CONTEXT_DIR: ${{ github.workspace }}/_build/reference-context
53+
steps:
54+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
55+
56+
- name: Trust checkout workspace
57+
run: git config --global --add safe.directory "$GITHUB_WORKSPACE"
58+
59+
- name: Restore patched Why3 runtime
60+
uses: actions/cache@5a3ec84eff668545956fd18022155c47e93e2684
61+
with:
62+
path: ${{ env.WHY3_REFERENCE_CACHE_DIR }}
63+
key: reference-runtime-${{ runner.os }}-${{ hashFiles('tools/contracts/reference-environment-lock-v1.json', 'tools/why3_reference/reference_runtime.mjs', 'tools/why3_reference/patches/driver-trace.patch') }}
64+
65+
- name: Set up MoonBit stable
66+
uses: moonbit-community/setup-moonbit@04293a8a813bfd4b6c2fce22701b52ae1050d100
67+
with:
68+
version: stable
69+
70+
- name: Verify project contracts and layered behavior
71+
run: |
72+
node tools/run.mjs bootstrap
73+
node tools/run.mjs contracts \
74+
--why3-archive "$WHY3_REFERENCE_ARCHIVE"
75+
node tools/run.mjs layers \
76+
--why3-archive "$WHY3_REFERENCE_ARCHIVE"
77+
78+
- name: Generate candidates in separate paths
79+
run: |
80+
node tools/run.mjs baselines candidate \
81+
--records "$RUNNER_TEMP/baseline-candidate" \
82+
--result "$RUNNER_TEMP/prover-result.json"
83+
84+
- name: Explicitly promote after fresh regeneration
85+
if: inputs.mode == 'promote'
86+
run: |
87+
node tools/run.mjs baselines promote \
88+
--records "$RUNNER_TEMP/baseline-candidate" \
89+
--result "$RUNNER_TEMP/prover-result.json"
90+
91+
- name: Render review patch
92+
run: |
93+
git diff --binary -- \
94+
tools/why3_reference/baselines/pr-v1 \
95+
> "$RUNNER_TEMP/baseline.patch"
96+
git status --short > "$RUNNER_TEMP/baseline.status"
97+
98+
- name: Upload candidate, provenance, and review material
99+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
100+
with:
101+
name: baselines-${{ inputs.mode }}-${{ github.sha }}
102+
path: |
103+
${{ runner.temp }}/baseline-candidate
104+
${{ runner.temp }}/prover-result.json
105+
${{ runner.temp }}/baseline.patch
106+
${{ runner.temp }}/baseline.status
107+
${{ env.WHY3_REFERENCE_CONTEXT_DIR }}
108+
if-no-files-found: warn

0 commit comments

Comments
 (0)