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
name: F* / hax extraction proof
# Extracts the AES-256-GCM/SIV composition from the real Rust source to F* with
# hax (Cryspen), then verifies HrcComposition.fst with F* - a source-level
# functional-correctness proof of j0 / increment_counter. A drift guard re-runs
# the extraction and fails if the proved bodies no longer match the shipped code.
#
# Runs INSIDE the pinned proof image (.github/docker/fstar-proof.Dockerfile, built
# by proof-image.yml), so there is no from-source toolchain build or network fetch
# at run time - the gate is deterministic and fast (~2 min). To advance a pinned
# tool, bump the Dockerfile + IMAGE_TAG + the container ref below, on purpose.
# Runs on every push/PR (fast and deterministic in the image), as a release gate
# (see publish.yml), and on demand.
on:
workflow_dispatch:
workflow_call:
push:
branches:
pull_request:
permissions:
contents: read
packages: read
concurrency:
group: fstar-${{ github.ref }}
cancel-in-progress: true
jobs:
fstar:
name: F* proof over hax-extracted composition
runs-on: ubuntu-24.04
container:
image: ghcr.io/godaddy/hardware-rust-crypto/fstar-proof:hax-a914ac7-fstar-v2026.03.24
credentials:
username: ${{ github.actor }}
password: ${{ secrets.GITHUB_TOKEN }}
steps:
- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
# The image bakes the pinned hax + F* toolchain and the env (PATH, OPAMROOT,
# HAX). Re-extracts with hax, drift-checks the proved bodies against the
# fresh extraction, then runs F* on HrcComposition.fst (non-zero on any
# unproved obligation).
- name: Verify the F* proof (with drift guard)
run: ./proofs/fstar/check.sh