Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
114 changes: 88 additions & 26 deletions .github/workflows/actions.lock
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ workflows:
- 'google/clusterfuzzlite@v1'
'.github/workflows/codeql.yml':
- 'actions/checkout@v7.0.1'
- 'github/codeql-action@v4.37.9'
- 'github/codeql-action@b96794f015dfd88f77b49b1c93e0fa7110f94c63'
'.github/workflows/coq-build.yml':
- 'actions/checkout@v7.0.1'
'.github/workflows/doc-consonance.yml':
Expand All @@ -32,13 +32,16 @@ workflows:
'.github/workflows/ghcr-publish.yml':
- 'actions/attest-build-provenance@v4.2.2'
- 'actions/checkout@v7.0.1'
'.github/workflows/governance.yml': []
'.github/workflows/hypatia-scan.yml': []
'.github/workflows/governance.yml':
- 'hyperpolymath/standards@8f31a5a4ba591d544b65f91f6d78b136e07756f0'
'.github/workflows/hypatia-scan.yml':
- 'hyperpolymath/standards@cc58c0cb23f73fc2019ce85a56a468e5248a93b3'
'.github/workflows/instant-sync.yml':
- 'peter-evans/repository-dispatch@v4.0.1'
'.github/workflows/label-triage.yml': []
'.github/workflows/labels.yml': []
'.github/workflows/mirror.yml': []
'.github/workflows/mirror.yml':
- 'hyperpolymath/standards@fcb8669169b4e9f5d9848608df880ae5fae812b4'
'.github/workflows/pages.yml':
- 'actions/checkout@v7.0.1'
- 'actions/deploy-pages@v5.0.1'
Expand All @@ -50,12 +53,21 @@ workflows:
- 'actions/upload-artifact@v7.0.1'
- 'dtolnay/rust-toolchain@stable'
- 'rustsec/audit-check@v2.0.0'
- 'taiki-e/install-action@v2.87.13'
'.github/workflows/scorecard.yml': []
'.github/workflows/secret-scanner.yml': []
'.github/workflows/security-scan.yml': []
'.github/workflows/spark-theatre-gate.yml': []
- 'taiki-e/install-action@v2.87.15'
'.github/workflows/scorecard.yml':
- 'hyperpolymath/standards@8750b94ac1bbe8c51ad13fe106669b13478f0b62'
'.github/workflows/secret-scanner.yml':
- 'hyperpolymath/standards@84355587cb2a1f86e6882de83514a32db2646e7a'
'.github/workflows/security-scan.yml':
- 'hyperpolymath/panic-attack@27b3d93b11fbfc03cee695e791904d741ce2b24b'
'.github/workflows/spark-theatre-gate.yml':
- 'hyperpolymath/standards@fcb8669169b4e9f5d9848608df880ae5fae812b4'
dependencies:
'Swatinem/rust-cache@v2.8.2':
ref: 'v2.8.2'
commit: 'sha1-779680da715d629ac1d338a641029a2f4372abb5'
owner_id: 580492
repo_id: 298565987
'actions/attest-build-provenance@v4.2.2':
ref: 'v4.2.2'
commit: 'sha1-4d101475d8b20a2381f78447822ac1eab6504dd8'
Expand All @@ -73,6 +85,16 @@ dependencies:
commit: 'sha1-55cc8345863c7cc4c66a329aec7e433d2d1c52a9'
owner_id: 44036562
repo_id: 215566462
'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1':
ref: '3d3c42e5aac5ba805825da76410c181273ba90b1'
commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1'
owner_id: 44036562
repo_id: 197814629
'actions/checkout@v4.3.1':
ref: 'v4.3.1'
commit: 'sha1-34e114876b0b11c390a56381ad16ebd13914f8d5'
owner_id: 44036562
repo_id: 197814629
'actions/checkout@v7.0.1':
ref: 'v7.0.1'
commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1'
Expand Down Expand Up @@ -100,26 +122,76 @@ dependencies:
repo_id: 496012378
uses:
- 'actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f'
'dtolnay/rust-toolchain@2c7215f132e9ebf062739d9130488b56d53c060c':
ref: '2c7215f132e9ebf062739d9130488b56d53c060c'
commit: 'sha1-2c7215f132e9ebf062739d9130488b56d53c060c'
owner_id: 1940490
repo_id: 260749683
'dtolnay/rust-toolchain@stable':
ref: 'stable'
commit: 'sha1-6bed0761d98439e5a578e2877258200ad565ba87'
owner_id: 1940490
repo_id: 260749683
'dtolnay/rust-toolchain@v1':
ref: 'v1'
commit: 'sha1-02cb101ec7c40f2c49e1d9714d64511d8e1b74de'
owner_id: 1940490
repo_id: 260749683
'erlef/setup-beam@v1.24.1':
ref: 'v1.24.1'
commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124'
owner_id: 47606891
repo_id: 331103973
'github/codeql-action@v4.37.9':
ref: 'v4.37.9'
commit: 'sha1-cdf488f595d80d6e07e03d4674febd5ab45fa938'
'github/codeql-action@b96794f015dfd88f77b49b1c93e0fa7110f94c63':
ref: 'v4.38.0'
commit: 'sha1-b96794f015dfd88f77b49b1c93e0fa7110f94c63'
owner_id: 9919
repo_id: 259445878
'google/clusterfuzzlite@v1':
ref: 'v1'
commit: 'sha1-884713a6c30a92e5e8544c39945cd7cb630abcd1'
owner_id: 1342004
repo_id: 400046858
'hyperpolymath/panic-attack@27b3d93b11fbfc03cee695e791904d741ce2b24b':
ref: '27b3d93b11fbfc03cee695e791904d741ce2b24b'
commit: 'sha1-27b3d93b11fbfc03cee695e791904d741ce2b24b'
owner_id: 6759885
repo_id: 1152434997
uses:
- 'actions/checkout@v4.3.1'
- 'dtolnay/rust-toolchain@v1'
- 'Swatinem/rust-cache@v2.8.2'
'hyperpolymath/standards@84355587cb2a1f86e6882de83514a32db2646e7a':
ref: '84355587cb2a1f86e6882de83514a32db2646e7a'
commit: 'sha1-84355587cb2a1f86e6882de83514a32db2646e7a'
owner_id: 6759885
repo_id: 1116521501
uses:
- 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
'hyperpolymath/standards@8750b94ac1bbe8c51ad13fe106669b13478f0b62':
ref: '8750b94ac1bbe8c51ad13fe106669b13478f0b62'
commit: 'sha1-8750b94ac1bbe8c51ad13fe106669b13478f0b62'
owner_id: 6759885
repo_id: 1116521501
'hyperpolymath/standards@8f31a5a4ba591d544b65f91f6d78b136e07756f0':
ref: '8f31a5a4ba591d544b65f91f6d78b136e07756f0'
commit: 'sha1-8f31a5a4ba591d544b65f91f6d78b136e07756f0'
owner_id: 6759885
repo_id: 1116521501
'hyperpolymath/standards@cc58c0cb23f73fc2019ce85a56a468e5248a93b3':
ref: 'cc58c0cb23f73fc2019ce85a56a468e5248a93b3'
commit: 'sha1-cc58c0cb23f73fc2019ce85a56a468e5248a93b3'
owner_id: 6759885
repo_id: 1116521501
'hyperpolymath/standards@fcb8669169b4e9f5d9848608df880ae5fae812b4':
ref: 'fcb8669169b4e9f5d9848608df880ae5fae812b4'
commit: 'sha1-fcb8669169b4e9f5d9848608df880ae5fae812b4'
owner_id: 6759885
repo_id: 1116521501
uses:
- 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
- 'dtolnay/rust-toolchain@2c7215f132e9ebf062739d9130488b56d53c060c'
- 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555'
'peter-evans/repository-dispatch@v4.0.1':
ref: 'v4.0.1'
commit: 'sha1-28959ce8df70de7be546dd1250a005dd32156697'
Expand All @@ -130,23 +202,13 @@ dependencies:
commit: 'sha1-69366f33c96575abad1ee0dba8212993eecbe998'
owner_id: 25397242
repo_id: 523199201
'taiki-e/install-action@v2.87.13':
ref: 'v2.87.13'
commit: 'sha1-26e9283f268b880168bdbd2c545dfcd60ec2c6ab'
'taiki-e/install-action@v2.87.15':
ref: 'v2.87.15'
commit: 'sha1-4076c08d76dba979c11a7285295b0716c1d67908'
owner_id: 43724913
repo_id: 442947557
'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1':
ref: 'v7.0.1'
commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1'
owner_id: 44036562
repo_id: 197814629
'dtolnay/rust-toolchain@2c7215f132e9ebf062739d9130488b56d53c060c':
ref: 'stable'
commit: 'sha1-2c7215f132e9ebf062739d9130488b56d53c060c'
owner_id: 1940490
repo_id: 260749683
'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555':
ref: 'v0.10.0'
ref: 'e83874834305fe9a4a2997156cb26c5de65a8555'
commit: 'sha1-e83874834305fe9a4a2997156cb26c5de65a8555'
owner_id: 135788
repo_id: 208510314
63 changes: 63 additions & 0 deletions .github/workflows/lock-sync-gate.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
# SPDX-License-Identifier: MPL-2.0
name: Lock Sync Gate

# Fails any pull request whose .github/workflows/actions.lock has drifted from
# the workflow YAML. That drift is not cosmetic: GitHub refuses such a run at
# startup, creating ZERO jobs, and reports only "This run likely failed because
# of a workflow file issue." A single grouped Dependabot bump can take out most
# of a repository's CI that way, because Dependabot rewrites `uses:` refs in the
# YAML and cannot touch the lockfile. Measured across 200 repositories on
# 2026-09-22: 39 had silently dead CI from exactly this cause.
# See hyperpolymath/standards#968.
#
# This workflow deliberately carries NO `uses:` of its own. It checks out by
# calling git in a `run:` step instead of using actions/checkout, so it has no
# lockfile entry to go stale and is structurally immune to the very failure it
# detects. Do not add a `uses:` to this file.
#
# There is also no `paths:` filter, on purpose: a filtered workflow never
# reports on pull requests that miss the filter, which deadlocks any branch
# ruleset that requires this check.

on:
pull_request:
push:
branches: [main]

permissions:
contents: read

concurrency:
group: lock-sync-gate-${{ github.ref }}
cancel-in-progress: true

jobs:
lock-sync:
name: actions.lock is in sync with the workflow YAML
runs-on: ubuntu-latest
timeout-minutes: 5
steps:
- name: Check out without actions/checkout
env:
REPO: ${{ github.repository }}
SHA: ${{ github.event.pull_request.head.sha || github.sha }}
TOKEN: ${{ github.token }}
run: |
set -euo pipefail
# Authenticate the fetch. An anonymous clone works only for public
# repositories; this gate must also run on private ones. The header
# form is used rather than a token in the remote URL so the
# credential is never written into .git/config.
AUTH="AUTHORIZATION: basic $(printf 'x-access-token:%s' "${TOKEN}" | base64 -w0)"
git init -q .
git remote add origin "https://github.com/${REPO}.git"
git -c http.extraheader="${AUTH}" fetch -q --depth 1 origin "${SHA}"
git checkout -q FETCH_HEAD
echo "checked out ${SHA}"

- name: Verify lockfile synchronisation
run: |
set -euo pipefail
test -x scripts/check-lock-sync.sh \
|| { echo "::error::scripts/check-lock-sync.sh missing or not executable"; exit 1; }
./scripts/check-lock-sync.sh
77 changes: 43 additions & 34 deletions rust-core/verisim-api/src/a2ml.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,7 @@ pub const A2ML_CONTENT_TYPE: &str = "text/a2ml; charset=utf-8";
/// Wrap an A2ML body string in an Axum [`Response`] with the correct
/// `Content-Type`.
pub fn a2ml_response(status: StatusCode, body: String) -> Response {
(
status,
[(header::CONTENT_TYPE, A2ML_CONTENT_TYPE)],
body,
)
.into_response()
(status, [(header::CONTENT_TYPE, A2ML_CONTENT_TYPE)], body).into_response()
}

/// Convenience alias so callers can `use crate::a2ml::String` implicitly.
Expand Down Expand Up @@ -126,20 +121,36 @@ pub fn proof_attempts_to_a2ml(rows: &[serde_json::Value]) -> String {
let mut out = String::new();
out.push_str("@proof-attempts():\n");
for v in rows {
let Some(attempt_id) = v["attempt_id"].as_str() else { continue };
let Some(obligation_id) = v["obligation_id"].as_str() else { continue };
let Some(repo) = v["repo"].as_str() else { continue };
let Some(file) = v["file"].as_str() else { continue };
let Some(claim) = v["claim"].as_str() else { continue };
let Some(obligation_class) = v["obligation_class"].as_str() else { continue };
let Some(prover_used) = v["prover_used"].as_str() else { continue };
let Some(outcome) = v["outcome"].as_str() else { continue };
let duration_ms = v["duration_ms"].as_u64().unwrap_or(0);
let confidence = v["confidence"].as_f64().unwrap_or(0.0);
let parent_attempt_id = v["parent_attempt_id"].as_str();
let strategy_tag = v["strategy_tag"].as_str().unwrap_or("");
let started_at = v["started_at"].as_str().unwrap_or("");
let completed_at = v["completed_at"].as_str().unwrap_or("");
let Some(attempt_id) = v["attempt_id"].as_str() else {
continue;
};
let Some(obligation_id) = v["obligation_id"].as_str() else {
continue;
};
let Some(repo) = v["repo"].as_str() else {
continue;
};
let Some(file) = v["file"].as_str() else {
continue;
};
let Some(claim) = v["claim"].as_str() else {
continue;
};
let Some(obligation_class) = v["obligation_class"].as_str() else {
continue;
};
let Some(prover_used) = v["prover_used"].as_str() else {
continue;
};
let Some(outcome) = v["outcome"].as_str() else {
continue;
};
let duration_ms = v["duration_ms"].as_u64().unwrap_or(0);
let confidence = v["confidence"].as_f64().unwrap_or(0.0);
let parent_attempt_id = v["parent_attempt_id"].as_str();
let strategy_tag = v["strategy_tag"].as_str().unwrap_or("");
let started_at = v["started_at"].as_str().unwrap_or("");
let completed_at = v["completed_at"].as_str().unwrap_or("");

let row = ProofAttemptRowA2ml {
attempt_id,
Expand Down Expand Up @@ -210,10 +221,10 @@ pub fn parse_recommendations(text: &str) -> Vec<RecommendationA2ml> {
.filter_map(|line| {
let v: serde_json::Value = serde_json::from_str(line).ok()?;
Some(RecommendationA2ml {
prover: v["prover_used"].as_str()?.to_string(),
success_rate: v["success_rate"].as_f64().unwrap_or(0.0),
prover: v["prover_used"].as_str()?.to_string(),
success_rate: v["success_rate"].as_f64().unwrap_or(0.0),
avg_duration_ms: v["avg_duration_ms"].as_f64().unwrap_or(0.0),
total_attempts: v["total_attempts"].as_u64().unwrap_or(0),
total_attempts: v["total_attempts"].as_u64().unwrap_or(0),
})
})
.collect()
Expand Down Expand Up @@ -257,9 +268,9 @@ pub fn parse_certs(text: &str) -> Vec<CertRowA2ml> {
.filter_map(|line| {
let v: serde_json::Value = serde_json::from_str(line).ok()?;
Some(CertRowA2ml {
prover_used: v["prover_used"].as_str()?.to_string(),
status: v["status"].as_str().unwrap_or("pending").to_string(),
success_rate: v["success_rate"].as_f64().unwrap_or(0.0),
prover_used: v["prover_used"].as_str()?.to_string(),
status: v["status"].as_str().unwrap_or("pending").to_string(),
success_rate: v["success_rate"].as_f64().unwrap_or(0.0),
total_attempts: v["total_attempts"].as_u64().unwrap_or(0),
})
})
Expand Down Expand Up @@ -310,14 +321,12 @@ mod tests {

#[test]
fn strategy_to_a2ml_format() {
let recs = vec![
RecommendationA2ml {
prover: "echidna".to_string(),
success_rate: 0.95,
avg_duration_ms: 120.5,
total_attempts: 100,
},
];
let recs = vec![RecommendationA2ml {
prover: "echidna".to_string(),
success_rate: 0.95,
avg_duration_ms: 120.5,
total_attempts: 100,
}];
let s = strategy_to_a2ml(&recs);
assert!(s.starts_with("@strategy-recommendations():\n"));
assert!(s.contains("prover=\"echidna\""));
Expand Down
Loading