From af3878d04f2b203cba8ffbceb68290999c1737e4 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 6 Jun 2026 11:10:55 +0200 Subject: [PATCH] chore(artifacts): remap retired status values for rivet vocabulary update MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A rivet tool update retired 'reviewed'/'accepted'/'in_progress' (rivet validate failed with 43 errors). Remap to the current vocabulary: reviewed -> approved (35) accepted -> approved (7) in_progress -> implemented (1, FEAT-006 — pipeline now works end-to-end) rivet validate: FAIL (43 errors) -> PASS (9 pre-existing coverage warnings). Co-Authored-By: Claude Opus 4.8 (1M context) --- artifacts/architecture.yaml | 14 ++++---- artifacts/features.yaml | 2 +- artifacts/safety.yaml | 70 ++++++++++++++++++------------------- 3 files changed, 43 insertions(+), 43 deletions(-) diff --git a/artifacts/architecture.yaml b/artifacts/architecture.yaml index 95075fc..eadefd1 100644 --- a/artifacts/architecture.yaml +++ b/artifacts/architecture.yaml @@ -6,7 +6,7 @@ artifacts: - id: DD-001 type: design-decision title: Per-platform toolchain download with SHA-256 registry - status: accepted + status: approved description: > Download pre-built Lean 4 binaries from GitHub releases for each supported platform. Maintain a KNOWN_VERSIONS registry in @@ -33,7 +33,7 @@ artifacts: - id: DD-002 type: design-decision title: Single version string for Lean and Mathlib - status: accepted + status: approved description: > The module extension uses the same version string from lean.toolchain(version=...) as the lean_version parameter passed to @@ -54,7 +54,7 @@ artifacts: - id: DD-003 type: design-decision title: Per-file ctx.actions.run with lean as executable - status: accepted + status: approved description: > Compile each .lean source file in a separate ctx.actions.run() call with the lean binary as the executable. Each action declares its @@ -79,7 +79,7 @@ artifacts: - id: DD-004 type: design-decision title: Source file copy via cp -L before lean invocation - status: accepted + status: approved description: > Each source .lean file is copied into bazel-out/ via cp -L (dereference symlinks) before being passed to the lean compiler. @@ -103,7 +103,7 @@ artifacts: - id: DD-005 type: design-decision title: Platform constraint mapping with artifact name translation - status: accepted + status: approved description: > Maintain two maps: _PLATFORM_CONSTRAINTS (Bazel constraint labels) and _PLATFORM_ARTIFACT (Lean release archive names). The hub repo @@ -127,7 +127,7 @@ artifacts: - id: DD-006 type: design-decision title: Mathlib fetch via lake with olean consolidation - status: accepted + status: approved description: > Download Lean toolchain within the mathlib_repo rule, create a lakefile pinned to the specified revision, run lake exe cache get @@ -155,7 +155,7 @@ artifacts: - id: DD-007 type: design-decision title: Charon toolchain via prebuilt downloads + Rust sysroot (pure Bazel) - status: accepted + status: approved description: > Download Charon's prebuilt release binaries from GitHub plus the matching Rust nightly sysroot (rustc, rust-std, rustc-dev, rust-src) diff --git a/artifacts/features.yaml b/artifacts/features.yaml index f5bbb68..d8ed1f7 100644 --- a/artifacts/features.yaml +++ b/artifacts/features.yaml @@ -93,7 +93,7 @@ artifacts: - id: FEAT-006 type: feature title: Aeneas LLBC-to-Lean translation - status: in_progress + status: implemented description: > Downloads pre-built Aeneas binaries from GitHub releases. Provides aeneas_translate rule for converting Charon LLBC files to Lean 4 diff --git a/artifacts/safety.yaml b/artifacts/safety.yaml index 8572a19..de61115 100644 --- a/artifacts/safety.yaml +++ b/artifacts/safety.yaml @@ -6,7 +6,7 @@ artifacts: - id: L-001 type: loss title: Undetected proof unsoundness - status: reviewed + status: approved description: > A Lean proof that type-checks in the build system is actually unsound due to toolchain misconfiguration, version mismatch, or incomplete @@ -17,7 +17,7 @@ artifacts: - id: L-002 type: loss title: Silent build corruption - status: reviewed + status: approved description: > Build artifacts (.olean files) are corrupted, stale, or produced by the wrong toolchain version, leading to downstream proof failures or @@ -28,7 +28,7 @@ artifacts: - id: L-003 type: loss title: Supply-chain compromise of toolchain - status: reviewed + status: approved description: > A tampered Lean binary or Mathlib olean set is downloaded and used, potentially introducing a malicious prover that accepts invalid proofs. @@ -38,7 +38,7 @@ artifacts: - id: L-004 type: loss title: Loss of reproducibility - status: reviewed + status: approved description: > Builds produce different results on different platforms or at different times due to non-hermetic inputs, making verification results unreliable @@ -53,7 +53,7 @@ artifacts: - id: H-001 type: hazard title: Lean compiler version mismatch with Mathlib oleans - status: reviewed + status: approved description: > The Lean compiler version used for compilation differs from the version used to build Mathlib oleans, causing olean format incompatibility. @@ -69,7 +69,7 @@ artifacts: - id: H-002 type: hazard title: SHA-256 hash verification bypassed or missing - status: reviewed + status: approved description: > Toolchain archive is downloaded without SHA-256 verification, allowing a tampered binary to be used. Empty sha256 strings disable verification @@ -83,7 +83,7 @@ artifacts: - id: H-003 type: hazard title: LEAN_PATH includes stale or incorrect directories - status: reviewed + status: approved description: > The LEAN_PATH environment variable points to directories containing oleans from a previous build, a different Lean version, or a wrong @@ -99,7 +99,7 @@ artifacts: - id: H-004 type: hazard title: Source file symlink resolution exposes wrong file content - status: reviewed + status: approved description: > Bazel's execroot uses symlinks for source files. If symlink targets change between analysis and execution (TOCTOU), the compiler may @@ -113,7 +113,7 @@ artifacts: - id: H-005 type: hazard title: Platform-specific binary used on wrong platform - status: reviewed + status: approved description: > Bazel's toolchain resolution selects a Lean binary for the wrong platform (e.g., darwin_aarch64 binary on linux_x86_64), leading to @@ -127,7 +127,7 @@ artifacts: - id: H-006 type: hazard title: Non-hermetic Mathlib fetch produces inconsistent oleans - status: reviewed + status: approved description: > The mathlib_repo rule uses network access (lake exe cache get) during fetch. If the cache server returns different oleans across builds @@ -141,7 +141,7 @@ artifacts: - id: H-007 type: hazard title: Sandbox disabled allows untracked host dependencies - status: reviewed + status: approved description: > The no-sandbox execution requirement means Lean actions can access host filesystem resources not declared as inputs. Changes to host @@ -249,7 +249,7 @@ artifacts: - id: CTRL-001 type: controller title: Bazel build system - status: reviewed + status: approved description: > The Bazel build system orchestrates toolchain resolution, action scheduling, input/output tracking, and caching. It controls which @@ -264,7 +264,7 @@ artifacts: - id: CTRL-002 type: controller title: Module extension (lean/extensions.bzl) - status: reviewed + status: approved description: > The Lean module extension configures toolchain downloads, Mathlib fetching, and toolchain registration. It mediates between the user's @@ -279,7 +279,7 @@ artifacts: - id: CTRL-003 type: controller title: lean_library rule implementation - status: reviewed + status: approved description: > The lean_library rule creates compilation actions for each .lean source file. It computes LEAN_PATH, manages source file copying, @@ -294,7 +294,7 @@ artifacts: - id: CTRL-004 type: controller title: Developer - status: reviewed + status: approved description: > The developer writes MODULE.bazel configuration (version, SHA-256 hashes), BUILD.bazel rules, and .lean source files. They decide @@ -305,7 +305,7 @@ artifacts: - id: CP-001 type: controlled-process title: Lean compilation process - status: reviewed + status: approved description: > The process of invoking the Lean compiler binary on source files to produce .olean outputs or typecheck proofs. Includes module @@ -314,7 +314,7 @@ artifacts: - id: CP-002 type: controlled-process title: Toolchain download and setup - status: reviewed + status: approved description: > The process of downloading Lean binaries from GitHub releases, extracting archives, setting permissions, and registering toolchains. @@ -322,7 +322,7 @@ artifacts: - id: CP-003 type: controlled-process title: Mathlib fetch and olean consolidation - status: reviewed + status: approved description: > The process of downloading Mathlib sources via lake, fetching pre-built oleans from the Mathlib cloud cache, and consolidating @@ -335,7 +335,7 @@ artifacts: - id: CA-001 type: control-action title: Select toolchain for platform - status: reviewed + status: approved description: > Bazel selects the appropriate Lean toolchain based on the execution platform's OS and CPU constraints. @@ -350,7 +350,7 @@ artifacts: - id: CA-002 type: control-action title: Download and extract Lean archive - status: reviewed + status: approved description: > The lean_release repository rule downloads the Lean 4 binary archive from GitHub releases and extracts it. @@ -365,7 +365,7 @@ artifacts: - id: CA-003 type: control-action title: Set LEAN_PATH for compilation - status: reviewed + status: approved description: > The lean_library rule constructs the LEAN_PATH environment variable from stdlib, dependency oleans, and the output directory. @@ -380,7 +380,7 @@ artifacts: - id: CA-004 type: control-action title: Invoke lean compiler on source file - status: reviewed + status: approved description: > The lean_library rule invokes the lean binary on a copied source file with -o flag to produce an olean output. @@ -395,7 +395,7 @@ artifacts: - id: CA-005 type: control-action title: Fetch Mathlib oleans via lake - status: reviewed + status: approved description: > The mathlib_repo rule invokes lake to download Mathlib source and pre-built oleans, then consolidates them into lib/. @@ -414,7 +414,7 @@ artifacts: - id: UCA-001 type: uca title: Extension provides mismatched Lean version to Mathlib fetch - status: reviewed + status: approved description: > The module extension passes a different lean_version to mathlib_repo than the version used for lean_release, causing Mathlib to be fetched @@ -437,7 +437,7 @@ artifacts: - id: UCA-002 type: uca title: Extension provides empty SHA-256 for production builds - status: reviewed + status: approved description: > The extension allows empty SHA-256 strings (from KNOWN_VERSIONS or user overrides), causing Bazel to download without hash verification. @@ -460,7 +460,7 @@ artifacts: - id: UCA-003 type: uca title: lean_library includes stale LEAN_PATH from previous dep version - status: reviewed + status: approved description: > A dependency's olean path from a previous build is included in LEAN_PATH because Bazel's cache returns a stale LeanInfo provider. @@ -481,7 +481,7 @@ artifacts: - id: UCA-004 type: uca title: Source copy action omitted, lean receives symlink - status: reviewed + status: approved description: > The _copy_src helper fails or is bypassed, passing the original symlinked source file to lean instead of a dereferenced copy. @@ -502,7 +502,7 @@ artifacts: - id: UCA-005 type: uca title: Toolchain hub registers wrong platform constraints - status: reviewed + status: approved description: > The _PLATFORM_CONSTRAINTS map or _PLATFORM_ARTIFACT map contains incorrect mappings, causing Bazel to select a binary for the wrong @@ -524,7 +524,7 @@ artifacts: - id: UCA-006 type: uca title: Mathlib olean consolidation misses packages - status: reviewed + status: approved description: > The shell script that copies oleans from .lake/packages/*/build/lib/lean/ fails to find oleans due to Lake directory structure changes, leaving @@ -623,7 +623,7 @@ artifacts: - id: LS-001 type: loss-scenario title: Lean version upgrade without Mathlib version bump - status: reviewed + status: approved description: > Developer changes lean.toolchain(version="4.28.0") but forgets to update lean.mathlib(rev="v4.28.0"). The extension passes lean_version @@ -644,7 +644,7 @@ artifacts: - id: LS-002 type: loss-scenario title: New platform added with wrong artifact name mapping - status: reviewed + status: approved description: > A new Lean release adds a platform (e.g., linux_riscv64). A developer adds it to ALL_PLATFORMS but with the wrong _PLATFORM_ARTIFACT mapping. @@ -664,7 +664,7 @@ artifacts: - id: LS-003 type: loss-scenario title: Lake changes olean output directory structure - status: reviewed + status: approved description: > A Lake version update changes the build output path from .lake/packages//.lake/build/lib/lean/ to a new layout @@ -685,7 +685,7 @@ artifacts: - id: LS-004 type: loss-scenario title: GitHub CDN serves tampered Lean binary without hash check - status: reviewed + status: approved description: > An attacker compromises a GitHub CDN edge or performs a MITM attack. The downloaded lean archive has a different SHA-256 but the hash @@ -706,7 +706,7 @@ artifacts: - id: LS-005 type: loss-scenario title: Bazel cache serves stale LeanInfo after dependency version change - status: reviewed + status: approved description: > Developer updates a dependency's Lean version in MODULE.bazel but Bazel's analysis cache still holds the old LeanInfo provider with @@ -729,7 +729,7 @@ artifacts: - id: LS-006 type: loss-scenario title: Code change removes _copy_src call, lean receives symlinked source - status: reviewed + status: approved description: > A refactor of lean.bzl removes or bypasses the _copy_src helper, passing the original source file (a symlink in the execroot) directly