Skip to content

Commit 74d9e18

Browse files
myfreessmyfreess
committed
add minimal initial impl
1 parent d0c0700 commit 74d9e18

358 files changed

Lines changed: 160909 additions & 441 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: 47 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -16,56 +16,64 @@ concurrency:
1616
cancel-in-progress: true
1717

1818
jobs:
19-
stable-build:
20-
name: stable
19+
environment:
20+
name: resolve reference environment
21+
runs-on: ubuntu-24.04
22+
outputs:
23+
image: ${{ steps.lock.outputs.image }}
24+
steps:
25+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
26+
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"
36+
37+
project:
38+
name: project
39+
needs:
40+
- environment
2141
runs-on: ubuntu-24.04
2242
container:
23-
image: ghcr.io/${{ github.repository }}-why3:1.7.2
43+
image: ${{ needs.environment.outputs.image }}
2444
credentials:
2545
username: ${{ github.actor }}
2646
password: ${{ secrets.GITHUB_TOKEN }}
47+
env:
48+
WHY3_REFERENCE_CACHE_DIR: ${{ github.workspace }}/.cache/why3-reference
49+
WHY3_REFERENCE_CONTEXT_DIR: ${{ github.workspace }}/_build/reference-context
2750
steps:
28-
- uses: actions/checkout@v6
51+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
2952

3053
- name: Trust checkout workspace
3154
run: git config --global --add safe.directory "$GITHUB_WORKSPACE"
3255

33-
- name: Setup Moon
34-
uses: moonbit-community/setup-moonbit@main
35-
with:
36-
version: stable
37-
38-
- name: moon update
39-
run: moon update
40-
41-
- name: Show tool versions
42-
run: |
43-
moon version --all
44-
moonrun --version
45-
46-
- name: Show Why3 version
47-
run: why3 --version
48-
49-
- name: Check all targets
50-
run: moon check --target all --warn-list +73
51-
52-
- name: Test all targets
53-
run: |
54-
moon test --target all --serial --release
55-
moon test --target all --serial
56-
57-
- name: Test Node.js tools
58-
run: node --test tools/*.test.mjs
56+
- name: Restore patched Why3 runtime
57+
uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9
58+
with:
59+
path: ${{ env.WHY3_REFERENCE_CACHE_DIR }}
60+
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') }}
5961

60-
- name: Check Why3 fixtures
61-
run: node tools/check_why3_fixtures.mjs
62+
- name: Set up MoonBit stable
63+
uses: moonbit-community/setup-moonbit@04293a8a813bfd4b6c2fce22701b52ae1050d100
64+
with:
65+
version: stable
6266

63-
- name: Check generated interfaces
67+
- name: Bootstrap and run the complete check
6468
run: |
65-
moon info
66-
git diff --exit-code
69+
node tools/run.mjs bootstrap
70+
node tools/run.mjs check \
71+
--why3-archive "$WHY3_REFERENCE_ARCHIVE"
6772
68-
- name: Check formatting
69-
run: |
70-
moon fmt
71-
git diff --exit-code
73+
- name: Upload resolved environment provenance
74+
if: always()
75+
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
76+
with:
77+
name: reference-context-${{ github.sha }}
78+
path: ${{ env.WHY3_REFERENCE_CONTEXT_DIR }}
79+
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@55cc8345863c7cc4c66a329aec7e433d2d1c52a9
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@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
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

‎.github/workflows/why3-image.yml‎

Lines changed: 81 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,7 @@ on:
66
- main
77
- update-why3-image
88
paths:
9-
- Dockerfile
10-
- .dockerignore
11-
- .github/workflows/why3-image.yml
9+
- infra/reference-env/**
1210
workflow_dispatch:
1311

1412
permissions:
@@ -24,28 +22,98 @@ jobs:
2422
name: build and push
2523
runs-on: ubuntu-24.04
2624
steps:
27-
- uses: actions/checkout@v6
25+
- uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803
2826

2927
- name: Log in to GHCR
30-
uses: docker/login-action@v3
28+
uses: docker/login-action@af1e73f918a031802d376d3c8bbc3fe56130a9b0
3129
with:
3230
registry: ghcr.io
3331
username: ${{ github.actor }}
3432
password: ${{ secrets.GITHUB_TOKEN }}
3533

3634
- name: Set up Docker Buildx
37-
uses: docker/setup-buildx-action@v3
35+
uses: docker/setup-buildx-action@bb05f3f5519dd87d3ba754cc423b652a5edd6d2c
3836

39-
- name: Build and push Why3 image
40-
uses: docker/build-push-action@v6
37+
- name: Build and push reference environment
38+
id: build
39+
uses: docker/build-push-action@53b7df96c91f9c12dcc8a07bcb9ccacbed38856a
4140
with:
42-
context: .
41+
context: infra/reference-env
4342
platforms: linux/amd64
4443
push: true
4544
tags: |
46-
ghcr.io/${{ github.repository }}-why3:1.7.2
47-
ghcr.io/${{ github.repository }}-why3:1.7.2-${{ github.sha }}
45+
ghcr.io/${{ github.repository }}-why3:1.7.2-z3-4.8.12
46+
ghcr.io/${{ github.repository }}-why3:reference-env-${{ github.sha }}
4847
build-args: |
48+
OCAML_VERSION=4.14.4
4949
WHY3_VERSION=1.7.2
50-
cache-from: type=gha,scope=why3-1.7.2
51-
cache-to: type=gha,mode=max,scope=why3-1.7.2
50+
WHY3_COMMIT=1343338d3bb1941c0d4f134283bb0790816113c4
51+
WHY3_TREE=f5e82693620413d7d8e3ebcba69addcb6a65f877
52+
WHY3_SOURCE_ARCHIVE_SHA256=c7bf782933a5d8ef9e78638cbf18e480eef895dca95317ba50231f20d45e92c7
53+
Z3_VERSION=4.8.12
54+
Z3_ARCHIVE_SHA256=648e8a7afb57445440ad711b733bd675e3888da2767c14ae5122582c924d8d52
55+
REFERENCE_MANIFEST_SHA256=d842c4413353e620a6ee409f58cef8f5572db7e3d0a6dd50c007981f44fee2eb
56+
cache-from: type=gha,scope=why3-reference-env-v1
57+
cache-to: type=gha,mode=max,scope=why3-reference-env-v1
58+
59+
- name: Verify pinned components and required Why3 capabilities
60+
env:
61+
IMAGE_DIGEST: ${{ steps.build.outputs.digest }}
62+
run: |
63+
image_ref="ghcr.io/${GITHUB_REPOSITORY}-why3@${IMAGE_DIGEST}"
64+
docker pull "$image_ref"
65+
docker run --rm --platform linux/amd64 "$image_ref" bash -ceu '
66+
test "$(ocamlc -version)" = 4.14.4
67+
test "$(why3 --version)" = "Why3 platform, version 1.7.2"
68+
test "$(z3 --version)" = "Z3 version 4.8.12 - 64 bit"
69+
printf "theory Simple\n goal trivial : true\nend\n" \
70+
> /tmp/why3-sexp-smoke.mlw
71+
why3 pp --output=sexp /tmp/why3-sexp-smoke.mlw \
72+
> /tmp/why3-sexp-smoke.sexp
73+
test -s /tmp/why3-sexp-smoke.sexp
74+
printf "%s %s\n" \
75+
c7bf782933a5d8ef9e78638cbf18e480eef895dca95317ba50231f20d45e92c7 \
76+
/opt/reference-env/why3-source.tar.gz \
77+
| sha256sum --check --strict
78+
printf "let _ = Driver.prepare_task_trace\n" > /tmp/trace_probe.ml
79+
if ocamlfind ocamlc -package why3 -c /tmp/trace_probe.ml >/dev/null 2>&1; then
80+
echo "global Why3 unexpectedly contains the repository trace extension" >&2
81+
exit 1
82+
fi
83+
'
84+
85+
- name: Generate the environment lock candidate
86+
env:
87+
IMAGE_DIGEST: ${{ steps.build.outputs.digest }}
88+
run: |
89+
image_ref="ghcr.io/${GITHUB_REPOSITORY}-why3@${IMAGE_DIGEST}"
90+
container_id="$(docker create --platform linux/amd64 "$image_ref")"
91+
docker cp "$container_id:/opt/reference-env/manifest.json" \
92+
"$RUNNER_TEMP/reference-env-manifest.json"
93+
docker rm "$container_id"
94+
node tools/why3_reference/generate_environment_lock_candidate.mjs \
95+
--image-digest "$IMAGE_DIGEST" \
96+
--manifest "$RUNNER_TEMP/reference-env-manifest.json" \
97+
--output "$RUNNER_TEMP/reference-environment-lock-v1.json"
98+
99+
- name: Report immutable image digest
100+
env:
101+
IMAGE_DIGEST: ${{ steps.build.outputs.digest }}
102+
run: |
103+
{
104+
echo '### Reference environment candidate'
105+
echo
106+
echo "Image digest: \`${IMAGE_DIGEST}\`"
107+
echo
108+
echo 'Promotion replaces only `tools/contracts/reference-environment-lock-v1.json`.'
109+
} >> "$GITHUB_STEP_SUMMARY"
110+
111+
- name: Upload environment lock candidate
112+
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
113+
with:
114+
name: reference-environment-${{ github.sha }}
115+
path: |
116+
${{ runner.temp }}/reference-env-manifest.json
117+
${{ runner.temp }}/reference-environment-lock-v1.json
118+
if-no-files-found: error
119+
retention-days: 30

‎Dockerfile‎

Lines changed: 0 additions & 40 deletions
This file was deleted.

0 commit comments

Comments
 (0)