From 0bf59591a0e7b15840b07b0aa56514afe63282c4 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 23:40:40 +0000 Subject: [PATCH 01/10] fix(api)!: authenticate and authorize the GraphQL API; bind loopback by default The whole GraphQL schema was served without authentication on 0.0.0.0. Any caller that reached the port could rewrite a repository's webhook secret through updateRepoSettings, then forge webhooks that start prover runs and post to GitHub, or write training rows through recordTacticOutcome. - Two bearer credentials, read only from the environment: ECHIDNABOT_API_ROUTE_TOKEN may only call submitProofObligation, and only for repositories in [api] route_repos ("owner/name" or "owner/*"); ECHIDNABOT_API_ADMIN_TOKEN may call everything. Each must be at least 32 bytes and they must differ. Compared in constant time. - A middleware in front of POST /graphql rate-limits per IP ([api] rate_limit_rpm, default 120) and answers 401 without a valid credential. - Every resolver carries a field guard that fails closed: executing the schema without a principal is refused, so the gate cannot be bypassed by calling the schema directly. Refusals carry code FORBIDDEN or UNAUTHENTICATED. - [server] host now defaults to 127.0.0.1, and the daemon refuses to bind a non-loopback address unless at least one credential is set. BREAKING CHANGE: /graphql now requires a bearer credential. Deployments that bind a non-loopback address (the compose setup binds 0.0.0.0) must set the credentials or the daemon will not start. Hypatia needs the route credential before its obligations are accepted again. Plan: metadatastician/standards#1397 (Wave 0, merged row 1). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- .env.example | 11 + docs/content/configuration.adoc | 9 +- echidnabot.example.toml | 18 +- src/api/auth.rs | 489 ++++++++++++++++++++++++++++++++ src/api/graphql.rs | 18 ++ src/api/mod.rs | 1 + src/config.rs | 49 +++- src/main.rs | 49 +++- src/trust/solver_integrity.rs | 2 +- tests/protocol_contract.rs | 101 ++++++- tests/smoke.rs | 134 ++++++++- wiki/Getting-Started.md | 2 + 12 files changed, 856 insertions(+), 27 deletions(-) create mode 100644 src/api/auth.rs diff --git a/.env.example b/.env.example index 2a9cd02..ce0b19f 100644 --- a/.env.example +++ b/.env.example @@ -29,6 +29,17 @@ DATABASE_URL=postgres://echidnabot:changeme@postgres:5432/echidnabot # mapping in compose.yml if you need something else. ECHIDNABOT__SERVER__HOST=0.0.0.0 ECHIDNABOT__SERVER__PORT=8080 + +# GraphQL API credentials. REQUIRED here: the container binds 0.0.0.0, and +# the daemon refuses a non-loopback bind without at least one of them. +# Each at least 32 bytes, the two different: `openssl rand -hex 32`. +# ECHIDNABOT_API_ROUTE_TOKEN submitProofObligation only, for [api] route_repos +# (the credential Hypatia holds) +# ECHIDNABOT_API_ADMIN_TOKEN every GraphQL query and mutation +# ECHIDNABOT_API_ROUTE_TOKEN= +# ECHIDNABOT_API_ADMIN_TOKEN= +# The repositories the route credential may submit for are set in +# echidnabot.toml: [api] route_repos = ["hyperpolymath/*"]. RUST_LOG=info # ─── ECHIDNA prover orchestrator (REST endpoint) ──────────────────────── diff --git a/docs/content/configuration.adoc b/docs/content/configuration.adoc index 95dffc6..f02959a 100644 --- a/docs/content/configuration.adoc +++ b/docs/content/configuration.adoc @@ -13,8 +13,13 @@ The main configuration file, located in your repository root or at ---- # Server configuration [server] -host = "0.0.0.0" +host = "127.0.0.1" # a non-loopback host needs API credentials port = 8080 + +# GraphQL API access (credentials come from the environment only) +[api] +route_repos = ["hyperpolymath/*"] # "owner/name" or "owner/*" +rate_limit_rpm = 120 # 0 disables workers = 4 # Database configuration @@ -66,6 +71,8 @@ webhook_secret = "${GITLAB_WEBHOOK_SECRET}" |`+ECHIDNABOT_ECHIDNA_ENDPOINT+` |ECHIDNA Core GraphQL endpoint |Yes |`+ECHIDNABOT_ECHIDNA_REST_ENDPOINT+` |ECHIDNA Core REST endpoint |No |`+ECHIDNABOT_ECHIDNA_MODE+` |ECHIDNA API mode (auto/graphql/rest) |No +|`+ECHIDNABOT_API_ROUTE_TOKEN+` |Bearer credential for `submitProofObligation` only, limited to `[api] route_repos`; at least 32 bytes |To submit obligations +|`+ECHIDNABOT_API_ADMIN_TOKEN+` |Bearer credential for every GraphQL query and mutation; at least 32 bytes, distinct from the route credential |To use the API |`+GITHUB_WEBHOOK_SECRET+` |GitHub webhook secret |For GitHub |`+GITHUB_APP_ID+` |GitHub App ID |For GitHub |`+GITHUB_PRIVATE_KEY+` |GitHub App private key (PEM) |For GitHub diff --git a/echidnabot.example.toml b/echidnabot.example.toml index 77dbfcc..eb01858 100644 --- a/echidnabot.example.toml +++ b/echidnabot.example.toml @@ -2,11 +2,25 @@ # Copy to echidnabot.toml and customize [server] -# Host to bind to (0.0.0.0 for all interfaces) -host = "0.0.0.0" +# Host to bind to. Loopback by default. Binding every interface +# ("0.0.0.0") needs ECHIDNABOT_API_ROUTE_TOKEN and/or +# ECHIDNABOT_API_ADMIN_TOKEN in the environment, or the daemon refuses to start. +host = "127.0.0.1" # Port to listen on port = 8080 +[api] +# The GraphQL API at /graphql needs a bearer credential. The two credentials +# are read only from the environment, never from this file: +# ECHIDNABOT_API_ROUTE_TOKEN submitProofObligation only, for route_repos +# ECHIDNABOT_API_ADMIN_TOKEN every query and mutation +# Each must be at least 32 bytes and they must differ: `openssl rand -hex 32`. +# Repositories the route credential may submit for: "owner/name" or "owner/*". +# Empty allows none. +route_repos = ["hyperpolymath/*"] +# /graphql requests per IP per minute (0 disables). +rate_limit_rpm = 120 + [database] # SQLite for development, PostgreSQL for production # SQLite: sqlite://path/to/db.sqlite diff --git a/src/api/auth.rs b/src/api/auth.rs new file mode 100644 index 0000000..b97dfbf --- /dev/null +++ b/src/api/auth.rs @@ -0,0 +1,489 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell +//! Authentication and authorization for the GraphQL API. +//! +//! Before this module the whole schema was served without authentication. +//! Any caller that could reach the port could rewrite a repository's webhook +//! secret (`updateRepoSettings`) and then forge webhooks, or write training +//! rows (`recordTacticOutcome`). +//! +//! The API now has two credentials, each read from its own environment +//! variable and never from a config file: +//! +//! * the *route* credential ([`ROUTE_TOKEN_ENV`]) may only call +//! `submitProofObligation`, and only for repositories in +//! `[api] route_repos`. It is the credential Hypatia holds; +//! * the *admin* credential ([`ADMIN_TOKEN_ENV`]) may call everything. +//! +//! Enforcement is in two layers. [`api_gate_middleware`] runs before the +//! schema: it rate-limits by peer address and answers 401 to a request with +//! no valid credential. Field guards ([`admin_only`], [`route_or_admin`], +//! [`check_repo_scope`]) run inside the schema and fail closed: a resolver +//! executed without a [`Principal`] in the request data is refused, so a +//! caller that executes the schema directly cannot bypass the gate. + +use std::sync::Arc; + +use async_graphql::{Context, ErrorExtensions}; +use async_graphql_axum::{GraphQLRequest, GraphQLResponse}; +use axum::{ + body::Body, + extract::{ConnectInfo, State}, + http::{header, Request, StatusCode}, + middleware::{self, Next}, + response::{IntoResponse, Response}, + routing::{post, MethodRouter}, + Extension, +}; +use std::net::SocketAddr; + +use super::graphql::EchidnabotSchema; +use super::rate_limit::WebhookRateLimiter; +use crate::trust::solver_integrity::constant_time_eq; + +/// Environment variable holding the route credential. +pub const ROUTE_TOKEN_ENV: &str = "ECHIDNABOT_API_ROUTE_TOKEN"; + +/// Environment variable holding the administrative credential. +pub const ADMIN_TOKEN_ENV: &str = "ECHIDNABOT_API_ADMIN_TOKEN"; + +/// Shortest credential accepted, in bytes. Generate one with +/// `openssl rand -hex 32` (64 characters). +pub const MIN_TOKEN_LEN: usize = 32; + +/// Who a request is, once its credential has been checked. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Principal { + /// The route credential: submit obligations for the repositories in scope. + Route(RepoScope), + /// The administrative credential: every query and mutation. + Admin, +} + +/// The repositories the route credential may submit obligations for. +/// +/// Each pattern is either an exact `owner/name` slug or `owner/*`, which +/// matches every repository of that owner. There is no global wildcard: an +/// empty scope allows nothing. +#[derive(Clone, Debug, Default, PartialEq, Eq)] +pub struct RepoScope { + patterns: Vec, +} + +impl RepoScope { + /// Build a scope from `owner/name` and `owner/*` patterns. + pub fn new(patterns: I) -> Self + where + I: IntoIterator, + S: Into, + { + Self { + patterns: patterns.into_iter().map(Into::into).collect(), + } + } + + /// Whether the scope lists no pattern at all. + pub fn is_empty(&self) -> bool { + self.patterns.is_empty() + } + + /// Whether `repo` (an `owner/name` slug) is in scope. + pub fn allows(&self, repo: &str) -> bool { + let Some((owner, name)) = repo.split_once('/') else { + return false; + }; + if owner.is_empty() || name.is_empty() || name.contains('/') { + return false; + } + self.patterns + .iter() + .any(|pattern| match pattern.split_once('/') { + Some((p_owner, "*")) => !p_owner.is_empty() && p_owner == owner, + Some(_) => pattern == repo, + None => false, + }) + } +} + +/// A credential that cannot be used safely. +#[derive(Debug, PartialEq, Eq, thiserror::Error)] +pub enum CredentialError { + /// The named credential is shorter than [`MIN_TOKEN_LEN`] bytes. + #[error("{0} is shorter than {MIN_TOKEN_LEN} bytes")] + TooShort(&'static str), + /// Both credentials are the same string, so roles cannot be told apart. + #[error("{ROUTE_TOKEN_ENV} and {ADMIN_TOKEN_ENV} must differ")] + NotDistinct, +} + +/// The configured credentials and the route credential's scope. +#[derive(Clone, Default)] +pub struct ApiCredentials { + route_token: Option, + admin_token: Option, + route_scope: RepoScope, +} + +impl std::fmt::Debug for ApiCredentials { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("ApiCredentials") + .field("route_token", &crate::config::redacted(&self.route_token)) + .field("admin_token", &crate::config::redacted(&self.admin_token)) + .field("route_scope", &self.route_scope) + .finish() + } +} + +impl ApiCredentials { + /// Validate and hold the two credentials. An empty string counts as unset. + /// + /// # Errors + /// [`CredentialError`] when a credential is too short or both are equal. + pub fn new( + route_token: Option, + admin_token: Option, + route_scope: RepoScope, + ) -> Result { + let route_token = route_token.filter(|t| !t.is_empty()); + let admin_token = admin_token.filter(|t| !t.is_empty()); + if route_token + .as_ref() + .is_some_and(|t| t.len() < MIN_TOKEN_LEN) + { + return Err(CredentialError::TooShort(ROUTE_TOKEN_ENV)); + } + if admin_token + .as_ref() + .is_some_and(|t| t.len() < MIN_TOKEN_LEN) + { + return Err(CredentialError::TooShort(ADMIN_TOKEN_ENV)); + } + if let (Some(route), Some(admin)) = (&route_token, &admin_token) { + if constant_time_eq(route.as_bytes(), admin.as_bytes()) { + return Err(CredentialError::NotDistinct); + } + } + Ok(Self { + route_token, + admin_token, + route_scope, + }) + } + + /// Read both credentials from [`ROUTE_TOKEN_ENV`] and [`ADMIN_TOKEN_ENV`]. + /// + /// # Errors + /// As for [`ApiCredentials::new`]. + pub fn from_env(route_scope: RepoScope) -> Result { + Self::new( + std::env::var(ROUTE_TOKEN_ENV).ok(), + std::env::var(ADMIN_TOKEN_ENV).ok(), + route_scope, + ) + } + + /// Whether no credential is configured, so every API request is refused. + pub fn is_empty(&self) -> bool { + self.route_token.is_none() && self.admin_token.is_none() + } + + /// Whether a route credential is configured. + pub fn has_route_token(&self) -> bool { + self.route_token.is_some() + } + + /// The route credential's repository scope. + pub fn route_scope(&self) -> &RepoScope { + &self.route_scope + } + + /// Map an `Authorization` header value to a principal. + /// + /// Accepts `Bearer ` with the scheme in any letter case. Both + /// credentials are compared in constant time, so the response time does + /// not reveal which one, if either, a guess was close to. + pub fn authenticate(&self, authorization: Option<&str>) -> Option { + let value = authorization?.trim(); + let (scheme, token) = value.split_once(' ')?; + if !scheme.eq_ignore_ascii_case("bearer") { + return None; + } + let token = token.trim().as_bytes(); + if token.is_empty() { + return None; + } + let is_admin = self + .admin_token + .as_ref() + .is_some_and(|t| constant_time_eq(t.as_bytes(), token)); + let is_route = self + .route_token + .as_ref() + .is_some_and(|t| constant_time_eq(t.as_bytes(), token)); + if is_admin { + Some(Principal::Admin) + } else if is_route { + Some(Principal::Route(self.route_scope.clone())) + } else { + None + } + } +} + +/// What the gate needs: the credentials and an optional per-IP limiter. +pub struct ApiGate { + credentials: ApiCredentials, + limiter: Option, +} + +impl ApiGate { + /// A gate over `credentials`, limiting each peer to `rate_limit_rpm` + /// requests a minute when given. + pub fn new(credentials: ApiCredentials, rate_limit_rpm: Option) -> Self { + Self { + credentials, + limiter: rate_limit_rpm.map(WebhookRateLimiter::new), + } + } +} + +/// Middleware in front of `POST /graphql`: rate limit, then authenticate. +/// +/// A request over the limit gets 429. A request without a valid credential +/// gets 401 with `WWW-Authenticate: Bearer` and never reaches the schema. An +/// authenticated request carries its [`Principal`] onward in the request +/// extensions. +pub async fn api_gate_middleware( + State(gate): State>, + mut request: Request, + next: Next, +) -> Response { + if let Some(limiter) = &gate.limiter { + let peer_ip = request + .extensions() + .get::>() + .map(|ci| ci.0.ip()); + if let Some(ip) = peer_ip { + if !limiter.check_ip(ip) { + tracing::warn!(%ip, limit = limiter.limit(), "GraphQL rate limit exceeded"); + return ( + StatusCode::TOO_MANY_REQUESTS, + [(header::RETRY_AFTER, "60")], + "Rate limit exceeded", + ) + .into_response(); + } + } + } + + let authorization = request + .headers() + .get(header::AUTHORIZATION) + .and_then(|v| v.to_str().ok()); + match gate.credentials.authenticate(authorization) { + Some(principal) => { + request.extensions_mut().insert(principal); + next.run(request).await + } + None => ( + StatusCode::UNAUTHORIZED, + [(header::WWW_AUTHENTICATE, "Bearer")], + "A valid bearer credential is required", + ) + .into_response(), + } +} + +/// `POST /graphql`: execute the request with the caller's principal attached. +pub async fn graphql_post( + Extension(schema): Extension, + Extension(principal): Extension, + request: GraphQLRequest, +) -> GraphQLResponse { + schema + .execute(request.into_inner().data(principal)) + .await + .into() +} + +/// The guarded `POST /graphql` handler, ready to mount on any router. +/// +/// The router must also provide `Extension`. +pub fn graphql_post_route(gate: Arc) -> MethodRouter +where + S: Clone + Send + Sync + 'static, +{ + post(graphql_post).layer(middleware::from_fn_with_state(gate, api_gate_middleware)) +} + +fn unauthenticated() -> async_graphql::Error { + async_graphql::Error::new("authentication required") + .extend_with(|_, e| e.set("code", "UNAUTHENTICATED")) +} + +fn forbidden(reason: &str) -> async_graphql::Error { + async_graphql::Error::new(format!("forbidden: {reason}")) + .extend_with(|_, e| e.set("code", "FORBIDDEN")) +} + +/// Field guard: the administrative credential only. +pub fn admin_only(ctx: &Context<'_>) -> async_graphql::Result<()> { + match ctx.data_opt::() { + Some(Principal::Admin) => Ok(()), + Some(Principal::Route(_)) => { + Err(forbidden("this field needs the administrative credential")) + } + None => Err(unauthenticated()), + } +} + +/// Field guard: either credential. +pub fn route_or_admin(ctx: &Context<'_>) -> async_graphql::Result<()> { + match ctx.data_opt::() { + Some(_) => Ok(()), + None => Err(unauthenticated()), + } +} + +/// Refuse `repo` unless the caller is the administrator or `repo` is in the +/// route credential's scope. +pub fn check_repo_scope(ctx: &Context<'_>, repo: &str) -> async_graphql::Result<()> { + match ctx.data_opt::() { + Some(Principal::Admin) => Ok(()), + Some(Principal::Route(scope)) if scope.allows(repo) => Ok(()), + Some(Principal::Route(_)) => Err(forbidden( + "repository is outside the route credential's scope", + )), + None => Err(unauthenticated()), + } +} + +/// Whether `host` binds only the loopback interface. +pub fn is_loopback_host(host: &str) -> bool { + let trimmed = host.trim_start_matches('[').trim_end_matches(']'); + if trimmed.eq_ignore_ascii_case("localhost") { + return true; + } + trimmed + .parse::() + .is_ok_and(|ip| ip.is_loopback()) +} + +#[cfg(test)] +mod tests { + use super::*; + + const ROUTE: &str = "test-route-credential-0123456789abcdef"; + const ADMIN: &str = "test-admin-credential-0123456789abcdef"; + + fn creds(scope: &[&str]) -> ApiCredentials { + ApiCredentials::new( + Some(ROUTE.to_string()), + Some(ADMIN.to_string()), + RepoScope::new(scope.iter().copied()), + ) + .unwrap() + } + + #[test] + fn scope_matches_exact_and_owner_wildcard_only() { + let scope = RepoScope::new(["hyperpolymath/*", "other/one"]); + assert!(scope.allows("hyperpolymath/hypatia")); + assert!(scope.allows("other/one")); + assert!(!scope.allows("other/two")); + assert!(!scope.allows("hyperpolymathx/hypatia")); + assert!(!scope.allows("hyperpolymath/")); + assert!(!scope.allows("hyperpolymath/a/b")); + assert!(!scope.allows("hyperpolymath")); + assert!(!RepoScope::new(["*"]).allows("a/b")); + assert!(!RepoScope::new(["*/*"]).allows("a/b")); + assert!(!RepoScope::default().allows("a/b")); + } + + #[test] + fn authenticate_maps_each_credential_to_its_role() { + let c = creds(&["hyperpolymath/*"]); + assert_eq!( + c.authenticate(Some(&format!("Bearer {ADMIN}"))), + Some(Principal::Admin) + ); + assert_eq!( + c.authenticate(Some(&format!("bearer {ROUTE}"))), + Some(Principal::Route(RepoScope::new(["hyperpolymath/*"]))) + ); + } + + #[test] + fn authenticate_refuses_missing_wrong_and_malformed_headers() { + let c = creds(&[]); + assert_eq!(c.authenticate(None), None); + assert_eq!(c.authenticate(Some("")), None); + assert_eq!(c.authenticate(Some("Bearer")), None); + assert_eq!(c.authenticate(Some("Bearer ")), None); + assert_eq!(c.authenticate(Some(&format!("Basic {ADMIN}"))), None); + assert_eq!(c.authenticate(Some(ADMIN)), None); + assert_eq!( + c.authenticate(Some("Bearer not-a-configured-credential-xxxx")), + None + ); + } + + #[test] + fn no_credentials_authenticate_nobody() { + let c = ApiCredentials::default(); + assert!(c.is_empty()); + assert_eq!( + c.authenticate(Some("Bearer anything-at-all-anything-at-all")), + None + ); + } + + #[test] + fn short_or_identical_credentials_are_refused() { + assert_eq!( + ApiCredentials::new(Some("short".into()), None, RepoScope::default()).unwrap_err(), + CredentialError::TooShort(ROUTE_TOKEN_ENV) + ); + assert_eq!( + ApiCredentials::new(None, Some("short".into()), RepoScope::default()).unwrap_err(), + CredentialError::TooShort(ADMIN_TOKEN_ENV) + ); + assert_eq!( + ApiCredentials::new(Some(ADMIN.into()), Some(ADMIN.into()), RepoScope::default()) + .unwrap_err(), + CredentialError::NotDistinct + ); + assert!(ApiCredentials::new( + Some(String::new()), + Some(String::new()), + RepoScope::default() + ) + .unwrap() + .is_empty()); + } + + #[test] + fn debug_never_prints_a_credential() { + let rendered = format!("{:?}", creds(&[])); + assert!(!rendered.contains(ROUTE)); + assert!(!rendered.contains(ADMIN)); + assert!(rendered.contains("")); + } + + #[test] + fn loopback_hosts_are_recognised() { + for host in [ + "127.0.0.1", + "::1", + "[::1]", + "localhost", + "LOCALHOST", + "127.1.2.3", + ] { + assert!(is_loopback_host(host), "{host}"); + } + for host in ["0.0.0.0", "::", "192.168.1.10", "example.org", ""] { + assert!(!is_loopback_host(host), "{host}"); + } + } +} diff --git a/src/api/graphql.rs b/src/api/graphql.rs index 9b6b0a1..9a1391c 100644 --- a/src/api/graphql.rs +++ b/src/api/graphql.rs @@ -4,6 +4,8 @@ //! GraphQL schema and resolvers use async_graphql::{Context, EmptySubscription, Object, Schema, SimpleObject, ID}; + +use super::auth::{admin_only, check_repo_scope, route_or_admin}; use chrono::{DateTime, Utc}; use std::sync::Arc; use uuid::Uuid; @@ -199,6 +201,7 @@ pub struct QueryRoot; #[Object] impl QueryRoot { /// Get a repository by platform, owner, and name + #[graphql(guard = "admin_only")] async fn repository( &self, ctx: &Context<'_>, @@ -216,6 +219,7 @@ impl QueryRoot { } /// List all registered repositories + #[graphql(guard = "admin_only")] async fn repositories(&self, ctx: &Context<'_>, platform: Option) -> Vec { let state = match ctx.data::() { Ok(state) => state, @@ -230,6 +234,7 @@ impl QueryRoot { } /// Get a proof job by ID + #[graphql(guard = "admin_only")] async fn job(&self, ctx: &Context<'_>, id: ID) -> Option { let state = ctx.data::().ok()?; let job_id = Uuid::parse_str(id.as_str()).ok()?; @@ -242,6 +247,7 @@ impl QueryRoot { } /// List jobs for a repository + #[graphql(guard = "admin_only")] async fn jobs_for_repo( &self, ctx: &Context<'_>, @@ -266,6 +272,7 @@ impl QueryRoot { } /// List available provers + #[graphql(guard = "admin_only")] async fn available_provers(&self, ctx: &Context<'_>) -> Vec { let state = match ctx.data::() { Ok(state) => state, @@ -293,6 +300,7 @@ impl QueryRoot { } /// Check prover status + #[graphql(guard = "admin_only")] async fn prover_status(&self, ctx: &Context<'_>, prover: ProverKind) -> ProverStatus { let state = match ctx.data::() { Ok(state) => state, @@ -309,6 +317,7 @@ impl QueryRoot { /// /// Used by LLM agents to inspect historical success rates before suggesting /// a tactic, and by operators to audit the feedback store. + #[graphql(guard = "admin_only")] async fn tactic_outcomes( &self, ctx: &Context<'_>, @@ -337,6 +346,7 @@ impl QueryRoot { /// List recorded tactic outcomes for a specific (prover, tactic) pair /// across all goal fingerprints. Useful for global win-rate queries. + #[graphql(guard = "admin_only")] async fn tactic_outcomes_by_tactic( &self, ctx: &Context<'_>, @@ -424,6 +434,7 @@ pub struct ProofObligationPayload { #[Object] impl MutationRoot { /// Register a repository for monitoring + #[graphql(guard = "admin_only")] async fn register_repository( &self, ctx: &Context<'_>, @@ -446,6 +457,7 @@ impl MutationRoot { } /// Manually trigger a proof check + #[graphql(guard = "admin_only")] async fn trigger_check( &self, ctx: &Context<'_>, @@ -502,6 +514,7 @@ impl MutationRoot { } /// Request ML-powered tactic suggestions + #[graphql(guard = "admin_only")] async fn request_suggestions( &self, ctx: &Context<'_>, @@ -519,6 +532,7 @@ impl MutationRoot { } /// Update repository settings + #[graphql(guard = "admin_only")] async fn update_repo_settings( &self, ctx: &Context<'_>, @@ -561,6 +575,7 @@ impl MutationRoot { } /// Enable or disable repository monitoring + #[graphql(guard = "admin_only")] async fn set_repo_enabled( &self, ctx: &Context<'_>, @@ -592,6 +607,7 @@ impl MutationRoot { /// tactic being applied in a proof session. The outcome feeds the local /// Reranker store so future suggestions for the same goal fingerprint are /// ranked by historical success rate. + #[graphql(guard = "admin_only")] async fn record_tactic_outcome( &self, ctx: &Context<'_>, @@ -628,6 +644,7 @@ impl MutationRoot { /// prover yet, and `inline: true` is recorded but not honoured. Invalid /// input or a store failure is returned as a GraphQL error, because one of /// the two senders reads only `errors` and ignores `success`. + #[graphql(guard = "route_or_admin")] async fn submit_proof_obligation( &self, ctx: &Context<'_>, @@ -644,6 +661,7 @@ impl MutationRoot { ))) } }; + check_repo_scope(ctx, &input.repo)?; if input.claim.trim().is_empty() { return Err(async_graphql::Error::new("claim must not be empty")); } diff --git a/src/api/mod.rs b/src/api/mod.rs index b2b6aa0..9d69e31 100644 --- a/src/api/mod.rs +++ b/src/api/mod.rs @@ -3,6 +3,7 @@ // SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell //! API layer - GraphQL and webhook handlers +pub mod auth; pub mod graphql; pub mod rate_limit; pub mod webhooks; diff --git a/src/config.rs b/src/config.rs index b062bc0..ed4caad 100644 --- a/src/config.rs +++ b/src/config.rs @@ -77,6 +77,15 @@ pub struct Config { /// `OTEL_EXPORTER_OTLP_ENDPOINT` env var (env wins over TOML). #[serde(default)] pub observability: ObservabilityConfig, + + /// GraphQL API access: which repositories the route credential may + /// submit obligations for, and the per-IP rate limit on `/graphql`. + /// The credentials themselves are read only from the environment + /// (`ECHIDNABOT_API_ROUTE_TOKEN`, `ECHIDNABOT_API_ADMIN_TOKEN`). + /// + /// TOML: `[api]\nroute_repos = ["hyperpolymath/*"]\nrate_limit_rpm = 120` + #[serde(default)] + pub api: ApiConfig, } /// Lifecycle settings — how long to wait for in-flight work to drain @@ -311,13 +320,51 @@ impl Default for ServerConfig { } fn default_host() -> String { - "0.0.0.0".to_string() + // Loopback by default: binding every interface is an explicit choice, + // and the daemon refuses it unless API credentials are configured + // (see `api::auth`). + "127.0.0.1".to_string() } fn default_port() -> u16 { 8080 } +/// GraphQL API access settings. The two credentials are not here: they are +/// read only from `ECHIDNABOT_API_ROUTE_TOKEN` and `ECHIDNABOT_API_ADMIN_TOKEN` +/// so they never sit in a config file. +/// +/// ```toml +/// [api] +/// route_repos = ["hyperpolymath/*"] +/// rate_limit_rpm = 120 +/// ``` +#[derive(Debug, Deserialize, Clone)] +pub struct ApiConfig { + /// Repositories the route credential may submit obligations for: + /// exact `owner/name` slugs or `owner/*`. Empty allows none. + #[serde(default)] + pub route_repos: Vec, + + /// Maximum `/graphql` requests per IP per minute. Default 120; set + /// `0` to disable. + #[serde(default = "default_api_rate_limit_rpm")] + pub rate_limit_rpm: u32, +} + +impl Default for ApiConfig { + fn default() -> Self { + Self { + route_repos: Vec::new(), + rate_limit_rpm: default_api_rate_limit_rpm(), + } + } +} + +fn default_api_rate_limit_rpm() -> u32 { + 120 +} + #[derive(Debug, Deserialize, Clone)] pub struct DatabaseConfig { #[serde(default = "default_database_url")] diff --git a/src/main.rs b/src/main.rs index 34b90c7..051c924 100644 --- a/src/main.rs +++ b/src/main.rs @@ -56,7 +56,8 @@ enum Commands { /// Start the webhook server Serve { /// Host to bind to. If omitted, reads `[server].host` from the TOML - /// config (which itself defaults to `0.0.0.0` if unset there). + /// config (which itself defaults to `127.0.0.1` if unset there). A + /// non-loopback host needs API credentials; see `[api]` in the docs. #[arg(short = 'H', long)] host: Option, @@ -251,8 +252,42 @@ async fn serve( port: u16, tracer_hook: Option, ) -> Result<()> { - use async_graphql_axum::{GraphQLRequest, GraphQLResponse}; - use axum::{routing::get, routing::post, Extension, Router}; + use axum::{routing::get, Extension, Router}; + use echidnabot::api::auth::{self as api_auth, ApiCredentials, ApiGate, RepoScope}; + + // GraphQL API credentials. Refuse to start rather than serve the schema + // unauthenticated on a reachable address: before this gate, any caller + // could rewrite a repository webhook secret or write training rows. + let credentials = ApiCredentials::from_env(RepoScope::new(config.api.route_repos.clone())) + .map_err(|e| echidnabot::Error::Config(format!("API credentials: {e}")))?; + if credentials.is_empty() { + if !api_auth::is_loopback_host(host) { + return Err(echidnabot::Error::Config(format!( + "refusing to bind {host}: set {} and/or {} before serving \ + /graphql on a non-loopback address", + api_auth::ROUTE_TOKEN_ENV, + api_auth::ADMIN_TOKEN_ENV + ))); + } + tracing::warn!( + "No API credentials set: every /graphql request will be refused \ + with 401. Set {} / {} to use the API.", + api_auth::ROUTE_TOKEN_ENV, + api_auth::ADMIN_TOKEN_ENV + ); + } + if credentials.has_route_token() && credentials.route_scope().is_empty() { + tracing::warn!( + "{} is set but [api] route_repos is empty: the route credential \ + can submit obligations for no repository.", + api_auth::ROUTE_TOKEN_ENV + ); + } + let api_rate_limit = (config.api.rate_limit_rpm > 0).then_some(config.api.rate_limit_rpm); + if api_rate_limit.is_none() { + tracing::warn!("/graphql rate limiting is disabled ([api] rate_limit_rpm = 0)"); + } + let api_gate = Arc::new(ApiGate::new(credentials, api_rate_limit)); // Webhook signature verification is per-integration (handled in // src/api/webhooks.rs). When no `webhook_secret` is configured for a @@ -329,13 +364,7 @@ async fn serve( .route("/", get(root)) .route( "/graphql", - post( - |Extension(schema): Extension, - req: GraphQLRequest| async move { - GraphQLResponse::from(schema.execute(req.into_inner()).await) - }, - ) - .get(graphql_playground), + api_auth::graphql_post_route(api_gate.clone()).get(graphql_playground), ) .merge(webhook_router(app_state.clone())) .layer(Extension(schema)) diff --git a/src/trust/solver_integrity.rs b/src/trust/solver_integrity.rs index fad4a36..b47d620 100644 --- a/src/trust/solver_integrity.rs +++ b/src/trust/solver_integrity.rs @@ -238,7 +238,7 @@ fn prover_key(prover: &ProverKind) -> String { /// Constant-time byte comparison to prevent timing side channels. /// /// Returns true if both slices are equal in length and content. -fn constant_time_eq(a: &[u8], b: &[u8]) -> bool { +pub(crate) fn constant_time_eq(a: &[u8], b: &[u8]) -> bool { if a.len() != b.len() { return false; } diff --git a/tests/protocol_contract.rs b/tests/protocol_contract.rs index ca7478b..d08a425 100644 --- a/tests/protocol_contract.rs +++ b/tests/protocol_contract.rs @@ -160,9 +160,38 @@ async fn obligation_schema() -> echidnabot::api::graphql::EchidnabotSchema { }) } -/// Execute `query` and return the response as JSON (data + errors). +/// The principal Hypatia holds: the route credential, scoped as a deployment +/// would scope it, plus the slug the contract tests use for invalid inputs. +fn hypatia_principal() -> echidnabot::api::auth::Principal { + echidnabot::api::auth::Principal::Route(echidnabot::api::auth::RepoScope::new([ + "hyperpolymath/*", + "a/b", + ])) +} + +/// Execute `query` as Hypatia and return the response as JSON (data + errors). async fn run(schema: &echidnabot::api::graphql::EchidnabotSchema, query: &str) -> Value { - serde_json::to_value(schema.execute(query).await).unwrap() + run_as(schema, query, Some(hypatia_principal())).await +} + +/// Execute `query` as `principal` (or with none) and return the response. +async fn run_as( + schema: &echidnabot::api::graphql::EchidnabotSchema, + query: &str, + principal: Option, +) -> Value { + let mut request = async_graphql::Request::new(query); + if let Some(p) = principal { + request = request.data(p); + } + serde_json::to_value(schema.execute(request).await).unwrap() +} + +/// The `code` extension of the first error, if any. +fn error_code(resp: &Value) -> Option { + resp["errors"][0]["extensions"]["code"] + .as_str() + .map(str::to_string) } /// FleetDispatcher's mutation; `prover_line` is "" or " prover: X,\n". @@ -272,3 +301,71 @@ async fn invalid_obligations_are_graphql_errors_not_success_false() { ); } } + +// --------------------------------------------------------------------------- +// Authorization inside the schema. The HTTP gate (src/api/auth.rs) answers +// 401 before the schema runs; these tests show the field guards fail closed +// for anything that executes the schema directly. +// --------------------------------------------------------------------------- + +const UPDATE_SETTINGS: &str = + "mutation { updateRepoSettings(repoId: \"00000000-0000-0000-0000-000000000000\", \ + settings: { webhookSecret: \"forged\" }) { id } }"; +const RECORD_OUTCOME: &str = "mutation { recordTacticOutcome(input: { \ + prover: COQ, goalState: \"g\", tactic: \"auto\", succeeded: true, durationMs: 1 }) { id } }"; + +#[tokio::test] +async fn obligation_outside_the_route_scope_is_forbidden() { + let schema = obligation_schema().await; + let q = fleet_mutation("someone-else/repo", "forall x, x = x", "pattern P1", ""); + let resp = run(&schema, &q).await; + assert_eq!(error_code(&resp).as_deref(), Some("FORBIDDEN"), "{resp}"); + assert!(resp["data"].is_null(), "{resp}"); +} + +#[tokio::test] +async fn schema_executed_without_a_principal_refuses_every_field() { + let schema = obligation_schema().await; + let submit = fleet_mutation("hyperpolymath/echidnabot", "c", "d", ""); + for q in [ + submit.as_str(), + UPDATE_SETTINGS, + RECORD_OUTCOME, + "{ repositories { id } }", + ] { + let resp = run_as(&schema, q, None).await; + assert_eq!( + error_code(&resp).as_deref(), + Some("UNAUTHENTICATED"), + "{q:.60}: {resp}" + ); + } +} + +#[tokio::test] +async fn route_credential_cannot_reach_administrative_fields() { + let schema = obligation_schema().await; + for q in [UPDATE_SETTINGS, RECORD_OUTCOME, "{ repositories { id } }"] { + let resp = run(&schema, q).await; + assert_eq!( + error_code(&resp).as_deref(), + Some("FORBIDDEN"), + "{q:.60}: {resp}" + ); + } +} + +#[tokio::test] +async fn admin_credential_passes_the_guards() { + let schema = obligation_schema().await; + let admin = Some(echidnabot::api::auth::Principal::Admin); + let resp = run_as(&schema, "{ repositories { id } }", admin.clone()).await; + assert!( + resp.get("errors") + .is_none_or(|e| e.as_array().unwrap().is_empty()), + "{resp}" + ); + // Any repository, in scope or not. + let q = fleet_mutation("someone-else/repo", "forall x, x = x", "pattern P1", ""); + accepted(&run_as(&schema, &q, admin).await); +} diff --git a/tests/smoke.rs b/tests/smoke.rs index 369ad42..95554d3 100644 --- a/tests/smoke.rs +++ b/tests/smoke.rs @@ -7,9 +7,9 @@ //! Verifies: "does it start, does it respond, are the obvious paths alive?" //! Runs before deeper tests in CI to fail-fast on build regressions. -use async_graphql_axum::{GraphQLRequest, GraphQLResponse}; use axum::{routing::get, Extension, Router}; use axum_test::TestServer; +use echidnabot::api::auth::{graphql_post_route, ApiCredentials, ApiGate, RepoScope}; use echidnabot::api::graphql::GraphQLState; use echidnabot::api::rate_limit::WebhookRateLimiter; use echidnabot::api::webhooks::AppState; @@ -21,6 +21,10 @@ use echidnabot::scheduler::JobScheduler; use echidnabot::store::SqliteStore; use std::sync::Arc; +// Test-only credentials (the `test-` prefix marks them for the secret scanner). +const ROUTE_TOKEN: &str = "test-route-credential-0123456789abcdef"; +const ADMIN_TOKEN: &str = "test-admin-credential-0123456789abcdef"; + async fn make_test_server() -> TestServer { let config = Arc::new(Config::default()); let store = Arc::new(SqliteStore::new("sqlite::memory:").await.unwrap()); @@ -42,17 +46,17 @@ async fn make_test_server() -> TestServer { mode_selector: ModeSelector::default(), }; + let credentials = ApiCredentials::new( + Some(ROUTE_TOKEN.to_string()), + Some(ADMIN_TOKEN.to_string()), + RepoScope::new(["hyperpolymath/*"]), + ) + .unwrap(); + let gate = Arc::new(ApiGate::new(credentials, None)); + let app = Router::new() .route("/health", get(|| async { "OK" })) - .route( - "/graphql", - axum::routing::post( - |Extension(schema): Extension, - req: GraphQLRequest| async move { - GraphQLResponse::from(schema.execute(req.into_inner()).await) - }, - ), - ) + .route("/graphql", graphql_post_route(gate)) .merge(webhook_router(app_state.clone())) .layer(Extension(schema)) .with_state(app_state); @@ -123,6 +127,7 @@ async fn smoke_graphql_typename_query() { let server = make_test_server().await; let response = server .post("/graphql") + .authorization_bearer(ADMIN_TOKEN) .json(&serde_json::json!({ "query": "{ __typename }" })) .await; response.assert_status_ok(); @@ -142,6 +147,7 @@ async fn smoke_graphql_repositories_empty() { let server = make_test_server().await; let response = server .post("/graphql") + .authorization_bearer(ADMIN_TOKEN) .json(&serde_json::json!({ "query": "{ repositories { id name } }" })) .await; response.assert_status_ok(); @@ -215,3 +221,111 @@ async fn smoke_rate_limiting_returns_429_at_limit() { "rate-limited response must include Retry-After header" ); } + +#[tokio::test] +async fn smoke_graphql_without_credential_is_401() { + let server = make_test_server().await; + let response = server + .post("/graphql") + .json(&serde_json::json!({ "query": "{ __typename }" })) + .await; + response.assert_status(axum::http::StatusCode::UNAUTHORIZED); + assert_eq!( + response.header("www-authenticate").to_str().unwrap(), + "Bearer" + ); +} + +#[tokio::test] +async fn smoke_graphql_with_wrong_credential_is_401() { + let server = make_test_server().await; + let response = server + .post("/graphql") + .authorization_bearer("test-not-a-configured-credential-000000") + .json(&serde_json::json!({ "query": "{ __typename }" })) + .await; + response.assert_status(axum::http::StatusCode::UNAUTHORIZED); +} + +#[tokio::test] +async fn smoke_graphql_route_credential_cannot_rewrite_webhook_secret() { + let server = make_test_server().await; + let response = server + .post("/graphql") + .authorization_bearer(ROUTE_TOKEN) + .json(&serde_json::json!({ + "query": "mutation { updateRepoSettings(repoId: \"00000000-0000-0000-0000-000000000000\", \ + settings: { webhookSecret: \"forged\" }) { id } }" + })) + .await; + response.assert_status_ok(); + let body: serde_json::Value = response.json(); + assert_eq!( + body["errors"][0]["extensions"]["code"], + serde_json::json!("FORBIDDEN"), + "{body}" + ); +} + +#[tokio::test] +async fn smoke_graphql_route_credential_submits_in_scope() { + let server = make_test_server().await; + let response = server + .post("/graphql") + .authorization_bearer(ROUTE_TOKEN) + .json(&serde_json::json!({ + "query": "mutation { submitProofObligation(input: { repo: \"hyperpolymath/hypatia\", \ + claim: \"forall x, x = x\", context: \"smoke\" }) { success } }" + })) + .await; + response.assert_status_ok(); + let body: serde_json::Value = response.json(); + assert_eq!( + body["data"]["submitProofObligation"]["success"], + serde_json::json!(true), + "{body}" + ); +} + +#[tokio::test] +async fn smoke_graphql_rate_limit_returns_429() { + let config = Arc::new(Config::default()); + let store = Arc::new(SqliteStore::new("sqlite::memory:").await.unwrap()); + let scheduler = Arc::new(JobScheduler::new(2, 10)); + let echidna = Arc::new(EchidnaClient::new(&config.echidna)); + let schema = create_schema(GraphQLState { + store: store.clone(), + scheduler: scheduler.clone(), + echidna, + }); + let app_state = AppState { + config, + store, + scheduler, + rate_limiter: None, + mode_selector: ModeSelector::default(), + }; + let credentials = + ApiCredentials::new(None, Some(ADMIN_TOKEN.to_string()), RepoScope::default()).unwrap(); + let gate = Arc::new(ApiGate::new(credentials, Some(2))); + let app = Router::new() + .route("/graphql", graphql_post_route(gate)) + .layer(Extension(schema)) + .with_state(app_state); + let server = TestServer::new(app.into_make_service_with_connect_info::()); + + for i in 0..2 { + let r = server + .post("/graphql") + .authorization_bearer(ADMIN_TOKEN) + .json(&serde_json::json!({ "query": "{ __typename }" })) + .await; + assert_eq!(r.status_code(), 200, "request {i} should pass"); + } + // Limited before authentication: an unauthenticated flood is limited too. + let r = server + .post("/graphql") + .json(&serde_json::json!({ "query": "{ __typename }" })) + .await; + r.assert_status(axum::http::StatusCode::TOO_MANY_REQUESTS); +} diff --git a/wiki/Getting-Started.md b/wiki/Getting-Started.md index 5311114..e75fedf 100644 --- a/wiki/Getting-Started.md +++ b/wiki/Getting-Started.md @@ -206,6 +206,8 @@ echidnabot provers list | `ECHIDNABOT_CONFIG` | Path to config file | | `ECHIDNABOT_DATABASE_URL` | Database connection string | | `ECHIDNABOT_ECHIDNA_ENDPOINT` | ECHIDNA Core GraphQL URL | +| `ECHIDNABOT_API_ROUTE_TOKEN` | Bearer credential that may only submit proof obligations, for `[api] route_repos` | +| `ECHIDNABOT_API_ADMIN_TOKEN` | Bearer credential for the whole GraphQL API | | `GITHUB_WEBHOOK_SECRET` | GitHub webhook secret | | `GITLAB_TOKEN` | GitLab access token | From e40f53737396f837a3b74b93de54a337458c8c86 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 23:51:00 +0000 Subject: [PATCH 02/10] fix(deps): bump four crates past RustSec advisories in Cargo.lock The Dependency audit job fails on four advisories published after the lockfile was last updated; none of them is introduced by this branch: - ctutils 0.4.2 -> 0.4.8 (RUSTSEC-2026-0385) - libz-sys 1.1.29 -> 1.1.31 (RUSTSEC-2026-0418) - rustls-webpki 0.103.15 -> 0.103.16 (RUSTSEC-2026-0382) - webpki-roots 1.0.7 -> 1.0.11 (RUSTSEC-2026-0381) All are semver-compatible patch releases (cargo update -p). cargo audit now exits 0 with the same three allowed warnings as before; every named test suite, the lib tests and clippy -D warnings still pass. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- Cargo.lock | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 17dc9a4..f6b7e3b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -923,9 +923,9 @@ dependencies = [ [[package]] name = "ctutils" -version = "0.4.2" +version = "0.4.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7d5515a3834141de9eafb9717ad39eea8247b5674e6066c404e8c4b365d2a29e" +checksum = "261af4dc7a06ea8a527a8717d8cbba3417530d6ea14e1edb3de6b67806be474f" dependencies = [ "cmov", ] @@ -1878,7 +1878,7 @@ dependencies = [ "tokio", "tokio-rustls", "tower-service", - "webpki-roots 1.0.7", + "webpki-roots 1.0.11", ] [[package]] @@ -2280,9 +2280,9 @@ dependencies = [ [[package]] name = "libz-sys" -version = "1.1.29" +version = "1.1.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85bc9657773828b90eeb625adff10eeac83cc21bbfd8e23a03eaa8a33c9e28d9" +checksum = "ff20308ecabd635a2dc1dd5834a86c462cca20efba1d5d3ddab1f8aea3455cb2" dependencies = [ "cc", "libc", @@ -3365,7 +3365,7 @@ dependencies = [ "wasm-bindgen", "wasm-bindgen-futures", "web-sys", - "webpki-roots 1.0.7", + "webpki-roots 1.0.11", ] [[package]] @@ -3539,9 +3539,9 @@ dependencies = [ [[package]] name = "rustls-webpki" -version = "0.103.15" +version = "0.103.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f3c3cf1d8b1e7d4927e2d154c3fcb02979afb9939629c62cd9048d4f07b60ac2" +checksum = "4443b1b6d39d7c663139942cc4558262562d2c84123bb6282ef177009ca8b281" dependencies = [ "ring", "rustls-pki-types", @@ -5038,14 +5038,14 @@ version = "0.26.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "521bc38abb08001b01866da9f51eb7c5d647a19260e00054a8c7fd5f9e57f7a9" dependencies = [ - "webpki-roots 1.0.7", + "webpki-roots 1.0.11", ] [[package]] name = "webpki-roots" -version = "1.0.7" +version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "52f5ee44c96cf55f1b349600768e3ece3a8f26010c05265ab73f945bb1a2eb9d" +checksum = "f5f280bbb2b287bc8e7de7e3852945a0ff50d1bbcb5ed42b6c7a568c546df171" dependencies = [ "rustls-pki-types", ] From 63cc6deec092e0ecf8d97eb7dd933d1ccd6838f2 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 00:04:39 +0000 Subject: [PATCH 03/10] fix(api): apply env config without a file, bound the limiter, trim credentials Review follow-ups on the GraphQL authentication change: - Config::load returned the defaults before adding the ECHIDNABOT__* environment source when the config file was missing. The compose stack ships no file and sets ECHIDNABOT__SERVER__HOST=0.0.0.0 in .env, so the new 127.0.0.1 default made the published port unreachable. The file is now optional and the environment always applies. - WebhookRateLimiter kept an entry for every peer address it ever saw, and the /graphql gate exposes it to unauthenticated callers. Idle peers are now swept when the map grows past max(4096, 2 x its size after the last sweep), so memory follows recent traffic. Webhook routes share the fix. - ApiCredentials::new now trims stored credentials as authenticate trims presented ones, so a value with a trailing newline still matches. - The /graphql limit is documented as per TCP peer address: behind a reverse proxy, limit at the proxy and set rate_limit_rpm = 0. - docs/content/configuration.adoc: `workers` moved back under [server]. - Tests: registerRepository and triggerCheck are now in both guard tests (the no-principal test is renamed to say what it covers); the 429 test also checks an authenticated caller. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- docs/content/configuration.adoc | 4 +- echidnabot.example.toml | 4 +- src/api/auth.rs | 32 ++++++++++-- src/api/rate_limit.rs | 91 ++++++++++++++++++++++++++++++--- src/config.rs | 71 ++++++++++++++++++++++--- tests/protocol_contract.rs | 16 +++++- tests/smoke.rs | 9 +++- 7 files changed, 206 insertions(+), 21 deletions(-) diff --git a/docs/content/configuration.adoc b/docs/content/configuration.adoc index f02959a..d080654 100644 --- a/docs/content/configuration.adoc +++ b/docs/content/configuration.adoc @@ -15,12 +15,12 @@ The main configuration file, located in your repository root or at [server] host = "127.0.0.1" # a non-loopback host needs API credentials port = 8080 +workers = 4 # GraphQL API access (credentials come from the environment only) [api] route_repos = ["hyperpolymath/*"] # "owner/name" or "owner/*" -rate_limit_rpm = 120 # 0 disables -workers = 4 +rate_limit_rpm = 120 # per TCP peer address; 0 disables # Database configuration [database] diff --git a/echidnabot.example.toml b/echidnabot.example.toml index eb01858..b94a998 100644 --- a/echidnabot.example.toml +++ b/echidnabot.example.toml @@ -18,7 +18,9 @@ port = 8080 # Repositories the route credential may submit for: "owner/name" or "owner/*". # Empty allows none. route_repos = ["hyperpolymath/*"] -# /graphql requests per IP per minute (0 disables). +# /graphql requests per minute per TCP peer address (0 disables). The peer is +# the address that connected, so behind a reverse proxy every client shares +# the proxy's budget: limit at the proxy instead and set 0 here. rate_limit_rpm = 120 [database] diff --git a/src/api/auth.rs b/src/api/auth.rs index b97dfbf..a19eef2 100644 --- a/src/api/auth.rs +++ b/src/api/auth.rs @@ -135,7 +135,9 @@ impl std::fmt::Debug for ApiCredentials { } impl ApiCredentials { - /// Validate and hold the two credentials. An empty string counts as unset. + /// Validate and hold the two credentials. Surrounding whitespace is + /// removed, as it is from a presented token, so a value read from a file + /// with a trailing newline still matches. An empty value counts as unset. /// /// # Errors /// [`CredentialError`] when a credential is too short or both are equal. @@ -144,8 +146,10 @@ impl ApiCredentials { admin_token: Option, route_scope: RepoScope, ) -> Result { - let route_token = route_token.filter(|t| !t.is_empty()); - let admin_token = admin_token.filter(|t| !t.is_empty()); + let normalise = + |t: Option| t.map(|t| t.trim().to_string()).filter(|t| !t.is_empty()); + let route_token = normalise(route_token); + let admin_token = normalise(admin_token); if route_token .as_ref() .is_some_and(|t| t.len() < MIN_TOKEN_LEN) @@ -400,6 +404,28 @@ mod tests { assert!(!RepoScope::default().allows("a/b")); } + #[test] + fn stored_credentials_are_trimmed_like_presented_ones() { + // A value read from a secrets file often ends in a newline. + let c = ApiCredentials::new( + Some(format!(" {ROUTE}\n")), + Some(format!("{ADMIN}\n")), + RepoScope::new(["a/*"]), + ) + .unwrap(); + assert_eq!( + c.authenticate(Some(&format!("Bearer {ROUTE}"))), + Some(Principal::Route(RepoScope::new(["a/*"]))) + ); + assert_eq!( + c.authenticate(Some(&format!("Bearer {ADMIN}"))), + Some(Principal::Admin) + ); + // Whitespace alone is unset, not a short credential. + let blank = ApiCredentials::new(Some(" \n".into()), None, RepoScope::default()).unwrap(); + assert!(blank.is_empty()); + } + #[test] fn authenticate_maps_each_credential_to_its_role() { let c = creds(&["hyperpolymath/*"]); diff --git a/src/api/rate_limit.rs b/src/api/rate_limit.rs index f787789..e6ef6f1 100644 --- a/src/api/rate_limit.rs +++ b/src/api/rate_limit.rs @@ -11,7 +11,11 @@ //! //! No external crates: uses a `Mutex>>` //! with lock time bounded by the dequeue sweep. Under webhook load (at most -//! a few hundred requests/minute per IP) this is negligible. +//! a few hundred requests/minute per IP) this is negligible. Idle peers are +//! swept out as the map grows, so its size follows recent traffic. +//! +//! The key is the TCP peer address. Forwarding headers are not trusted, so +//! behind a reverse proxy every client shares the proxy's budget. use std::collections::{HashMap, VecDeque}; use std::net::IpAddr; @@ -32,18 +36,41 @@ use super::webhooks::AppState; // ConnectInfo and SocketAddr are used in the middleware body via // request.extensions().get::>(). +/// Map size below which idle peers are never swept. +const SWEEP_FLOOR: usize = 4096; + +/// Per-peer request times, plus the map size at which idle peers are next +/// swept out. +#[derive(Default)] +struct LimiterState { + peers: HashMap>, + sweep_at: usize, +} + /// Sliding-window per-IP rate limiter (60-second window). +/// +/// Memory is bounded by recent traffic, not by every address ever seen: when +/// the map grows past `max(SWEEP_FLOOR, 2 × size after the last sweep)`, +/// peers with no request inside the window are dropped. Sweeps are therefore +/// amortised O(1) per request. pub struct WebhookRateLimiter { - state: Mutex>>, + state: Mutex, window: Duration, limit: u32, } impl WebhookRateLimiter { pub fn new(requests_per_minute: u32) -> Self { + Self::with_window(requests_per_minute, Duration::from_secs(60)) + } + + fn with_window(requests_per_minute: u32, window: Duration) -> Self { Self { - state: Mutex::new(HashMap::new()), - window: Duration::from_secs(60), + state: Mutex::new(LimiterState { + peers: HashMap::new(), + sweep_at: SWEEP_FLOOR, + }), + window, limit: requests_per_minute, } } @@ -51,11 +78,19 @@ impl WebhookRateLimiter { /// Returns `true` if the request is within the allowed rate. pub fn check_ip(&self, ip: IpAddr) -> bool { let now = Instant::now(); + let cutoff = now.checked_sub(self.window).unwrap_or(now); let mut state = self.state.lock().expect("rate limiter mutex poisoned"); - let timestamps = state.entry(ip).or_default(); + + if state.peers.len() >= state.sweep_at { + state + .peers + .retain(|_, times| times.back().is_some_and(|&t| t >= cutoff)); + state.sweep_at = SWEEP_FLOOR.max(state.peers.len().saturating_mul(2)); + } + + let timestamps = state.peers.entry(ip).or_default(); // Evict entries older than the window - let cutoff = now - self.window; while timestamps.front().map(|&t| t < cutoff).unwrap_or(false) { timestamps.pop_front(); } @@ -68,6 +103,15 @@ impl WebhookRateLimiter { } } + #[cfg(test)] + fn tracked_peers(&self) -> usize { + self.state + .lock() + .expect("rate limiter mutex poisoned") + .peers + .len() + } + pub fn limit(&self) -> u32 { self.limit } @@ -155,4 +199,39 @@ mod tests { assert!(!limiter.check_ip(ip1), "ip1 should be blocked"); assert!(limiter.check_ip(ip2), "ip2 should still be allowed"); } + + fn nth_ip(i: usize) -> IpAddr { + IpAddr::V6(std::net::Ipv6Addr::from(0x2001_0db8_u128 << 96 | i as u128)) + } + + #[test] + fn idle_peers_are_swept_once_the_map_is_large() { + let limiter = WebhookRateLimiter::with_window(5, Duration::from_millis(1)); + for i in 0..SWEEP_FLOOR { + assert!(limiter.check_ip(nth_ip(i))); + } + assert_eq!(limiter.tracked_peers(), SWEEP_FLOOR); + std::thread::sleep(Duration::from_millis(5)); + // Every earlier peer is now idle; the next new peer triggers a sweep. + assert!(limiter.check_ip(nth_ip(SWEEP_FLOOR))); + assert_eq!(limiter.tracked_peers(), 1); + } + + #[test] + fn active_peers_survive_a_sweep_and_stay_limited() { + let limiter = WebhookRateLimiter::new(2); + let busy = IpAddr::V4(Ipv4Addr::new(10, 0, 0, 9)); + assert!(limiter.check_ip(busy)); + assert!(limiter.check_ip(busy)); + for i in 0..SWEEP_FLOOR { + limiter.check_ip(nth_ip(i)); + } + // A sweep has run (the map reached the floor) inside the window, so + // nothing was idle and `busy` is still at its limit. + assert!(limiter.tracked_peers() > SWEEP_FLOOR); + assert!( + !limiter.check_ip(busy), + "a sweep must not reset an active peer" + ); + } } diff --git a/src/config.rs b/src/config.rs index ed4caad..95556f1 100644 --- a/src/config.rs +++ b/src/config.rs @@ -346,8 +346,10 @@ pub struct ApiConfig { #[serde(default)] pub route_repos: Vec, - /// Maximum `/graphql` requests per IP per minute. Default 120; set - /// `0` to disable. + /// Maximum `/graphql` requests per minute per TCP peer address. Default + /// 120; set `0` to disable. Forwarding headers are not trusted, so + /// behind a reverse proxy every client shares the proxy's budget: limit + /// at the proxy and set `0` here. #[serde(default = "default_api_rate_limit_rpm")] pub rate_limit_rpm: u32, } @@ -533,16 +535,33 @@ fn default_queue_size() -> usize { impl Config { /// Load configuration from file pub fn load(path: &str) -> Result { + Self::load_with_env(path, Self::environment()) + } + + /// The `ECHIDNABOT__SECTION__KEY` environment source. + fn environment() -> config::Environment { + config::Environment::with_prefix("ECHIDNABOT").separator("__") + } + + /// [`Config::load`] with the environment source supplied, so tests can + /// pass a fixed map instead of mutating the process environment. + /// + /// The environment applies whether or not the file exists: a container + /// that ships no config file is configured by `ECHIDNABOT__…` variables + /// alone (see `.env.example`). + fn load_with_env(path: &str, env: config::Environment) -> Result { let path = Path::new(path); if !path.exists() { - tracing::warn!("Config file {} not found, using defaults", path.display()); - return Ok(Self::default()); + tracing::warn!( + "Config file {} not found, using defaults and ECHIDNABOT__* overrides", + path.display() + ); } let builder = config::Config::builder() - .add_source(config::File::from(path)) - .add_source(config::Environment::with_prefix("ECHIDNABOT").separator("__")); + .add_source(config::File::from(path).required(false)) + .add_source(env); let config = builder.build()?; let parsed: Config = config.try_deserialize()?; @@ -627,3 +646,43 @@ mod redaction_tests { } } } + +#[cfg(test)] +mod load_tests { + use super::*; + + fn env(pairs: &[(&str, &str)]) -> config::Environment { + let map: config::Map = pairs + .iter() + .map(|(k, v)| ((*k).to_string(), (*v).to_string())) + .collect(); + Config::environment().source(Some(map)) + } + + /// A container ships no config file and sets `ECHIDNABOT__SERVER__HOST` + /// in `.env`: the override must apply, not the loopback default. + #[test] + fn environment_applies_when_the_config_file_is_missing() { + let missing = "/nonexistent/echidnabot-test-config.toml"; + let c = Config::load_with_env( + missing, + env(&[ + ("ECHIDNABOT__SERVER__HOST", "0.0.0.0"), + ("ECHIDNABOT__SERVER__PORT", "9091"), + ]), + ) + .unwrap(); + assert_eq!(c.server.host, "0.0.0.0"); + assert_eq!(c.server.port, 9091); + } + + #[test] + fn missing_file_and_no_overrides_gives_the_defaults() { + let c = + Config::load_with_env("/nonexistent/echidnabot-test-config.toml", env(&[])).unwrap(); + assert_eq!(c.server.host, "127.0.0.1"); + assert_eq!(c.server.port, 8080); + assert_eq!(c.api.rate_limit_rpm, 120); + assert!(c.api.route_repos.is_empty()); + } +} diff --git a/tests/protocol_contract.rs b/tests/protocol_contract.rs index d08a425..6a81032 100644 --- a/tests/protocol_contract.rs +++ b/tests/protocol_contract.rs @@ -313,6 +313,10 @@ const UPDATE_SETTINGS: &str = settings: { webhookSecret: \"forged\" }) { id } }"; const RECORD_OUTCOME: &str = "mutation { recordTacticOutcome(input: { \ prover: COQ, goalState: \"g\", tactic: \"auto\", succeeded: true, durationMs: 1 }) { id } }"; +const REGISTER_REPO: &str = "mutation { registerRepository(input: { \ + platform: GIT_HUB, owner: \"someone-else\", name: \"repo\", webhookSecret: \"forged\" }) { id } }"; +const TRIGGER_CHECK: &str = + "mutation { triggerCheck(repoId: \"00000000-0000-0000-0000-000000000000\") { id } }"; #[tokio::test] async fn obligation_outside_the_route_scope_is_forbidden() { @@ -324,13 +328,15 @@ async fn obligation_outside_the_route_scope_is_forbidden() { } #[tokio::test] -async fn schema_executed_without_a_principal_refuses_every_field() { +async fn schema_executed_without_a_principal_refuses_the_guarded_fields() { let schema = obligation_schema().await; let submit = fleet_mutation("hyperpolymath/echidnabot", "c", "d", ""); for q in [ submit.as_str(), UPDATE_SETTINGS, RECORD_OUTCOME, + REGISTER_REPO, + TRIGGER_CHECK, "{ repositories { id } }", ] { let resp = run_as(&schema, q, None).await; @@ -345,7 +351,13 @@ async fn schema_executed_without_a_principal_refuses_every_field() { #[tokio::test] async fn route_credential_cannot_reach_administrative_fields() { let schema = obligation_schema().await; - for q in [UPDATE_SETTINGS, RECORD_OUTCOME, "{ repositories { id } }"] { + for q in [ + UPDATE_SETTINGS, + RECORD_OUTCOME, + REGISTER_REPO, + TRIGGER_CHECK, + "{ repositories { id } }", + ] { let resp = run(&schema, q).await; assert_eq!( error_code(&resp).as_deref(), diff --git a/tests/smoke.rs b/tests/smoke.rs index 95554d3..501878a 100644 --- a/tests/smoke.rs +++ b/tests/smoke.rs @@ -322,7 +322,14 @@ async fn smoke_graphql_rate_limit_returns_429() { .await; assert_eq!(r.status_code(), 200, "request {i} should pass"); } - // Limited before authentication: an unauthenticated flood is limited too. + // An authenticated caller over the limit is refused... + let r = server + .post("/graphql") + .authorization_bearer(ADMIN_TOKEN) + .json(&serde_json::json!({ "query": "{ __typename }" })) + .await; + r.assert_status(axum::http::StatusCode::TOO_MANY_REQUESTS); + // ...and, limited before authentication, so is an unauthenticated flood. let r = server .post("/graphql") .json(&serde_json::json!({ "query": "{ __typename }" })) From b664f99192a0856ac81ad62954588adf60f1fd52 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:01:35 +0000 Subject: [PATCH 04/10] proofs: check the receipt-boundary theory in all three kernels, in CI MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The receipt-boundary theorem (T-RECEIPT) had an Agda source and Lean and Rocq re-proof candidates, none of them ever checked. This change records the first kernel receipts and gates all three legs on every pull request. - scripts/check-agda-proofs.sh compared the whole `agda --version` output with one line, so it refused the official 2.8.0.2 binary (which prints its build flags after the version). It now compares the first line. - scripts/check-theory-rechecks.sh checks the Lean (4.35.0) and Rocq (Coq 8.18.0) legs and fails unless every `#print axioms` / `Print Assumptions` report is clean. Each leg first runs a negative control (a planted axiom / Admitted) that must fail. - proof-safety.yml gains a `theory` job: digest-verified Agda and Lean release archives, Coq from the Ubuntu archive, then both scripts. It uses only actions/checkout, already locked for this workflow. - docs/PROOF-STATUS.adoc: receipts R-AGDA, R-LEAN, R-ROCQ; T-RECEIPT and both legs `proven`; an agent-drafted statement-correspondence table that keeps both legs BRIDGE-PENDING until owner review (PWG-3 derived until then); PWG wording replaces "Grade 3"; the PROOF-POLICY §6 deviation for installing toolchains outside Guix; and the #192 authorisation obligations, open under the Creusot/Pearlite and Verus default (§1.2). Observed locally at 1443adf: Agda accepted both modules under the strict profile (planted postulate and false proof refused); Lean and Coq accepted their files with no axioms (planted axiom and Admitted refused). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- .github/workflows/proof-safety.yml | 42 +++++ docs/PROOF-STATUS.adoc | 292 ++++++++++++++++++++++------- scripts/check-agda-proofs.sh | 2 +- scripts/check-theory-rechecks.sh | 92 +++++++++ 4 files changed, 359 insertions(+), 69 deletions(-) create mode 100755 scripts/check-theory-rechecks.sh diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml index b145f55..d74a501 100644 --- a/.github/workflows/proof-safety.yml +++ b/.github/workflows/proof-safety.yml @@ -26,3 +26,45 @@ jobs: cargo test --locked --test protocol_contract cargo test --locked --bin echidnabot clone_contract_tests cargo test --locked --lib git_process_tests + + theory: + # Receipt-boundary theory (docs/PROOF-STATUS.adoc T-RECEIPT): the Agda + # source and its Lean and Rocq re-proofs, each checked by its own kernel + # at this commit. Toolchains come from pinned upstream release archives, + # not the Guix manifest: this is the recorded PROOF-POLICY §6 deviation + # D-THEORY-TOOLS in docs/PROOF-STATUS.adoc. Each archive is verified by + # digest, and each script fails if the version it observes differs. + name: Theory proofs (Agda, Lean, Rocq) + runs-on: ubuntu-24.04 + timeout-minutes: 20 + env: + AGDA_URL: https://github.com/agda/agda/releases/download/v2.8.0.2/Agda-v2.8.0.2-linux.tar.xz + AGDA_SHA256: 2bcf24bb561b1be859bba841e5d67962d1616b3251bc147f878e4f60a2fbd9f7 + LEAN_URL: https://releases.lean-lang.org/lean4/v4.35.0/lean-4.35.0-linux.tar.zst + LEAN_SHA256: 7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d + steps: + - uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + - name: Install Agda 2.8.0.2 (digest-verified release) + run: | + mkdir -p "$RUNNER_TEMP/agda" + curl -fsSL -o "$RUNNER_TEMP/agda.tar.xz" "$AGDA_URL" + echo "$AGDA_SHA256 $RUNNER_TEMP/agda.tar.xz" | sha256sum -c - + tar -xJf "$RUNNER_TEMP/agda.tar.xz" -C "$RUNNER_TEMP/agda" + echo "$RUNNER_TEMP/agda" >> "$GITHUB_PATH" + - name: Install Lean 4.35.0 (digest-verified release) + run: | + mkdir -p "$RUNNER_TEMP/lean" + curl -fsSL -o "$RUNNER_TEMP/lean.tar.zst" "$LEAN_URL" + echo "$LEAN_SHA256 $RUNNER_TEMP/lean.tar.zst" | sha256sum -c - + tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP/lean" --strip-components=1 + echo "$RUNNER_TEMP/lean/bin" >> "$GITHUB_PATH" + - name: Install Coq 8.18.0 (Ubuntu 24.04 archive) + run: | + sudo apt-get update -q + sudo apt-get install -y -q coq + - name: Agda source (strict profile) + run: ./scripts/check-agda-proofs.sh + - name: Lean and Rocq recheck legs (with negative controls) + run: ./scripts/check-theory-rechecks.sh diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index fd85057..fec2173 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -4,18 +4,25 @@ == Evidence rules -Updated 2026-11-01 on `arena/68c18146-echidnabot`, based on -`ab26bd54c8bdc04da8cc48c0778a25eb774be268`. New files are working-tree -candidates, not committed or checked proof receipts. No Grade 3 attainment -is claimed. `open` means not checked/done, `argued` means an explicit -assumption, and `tested-only` requires an actual observed bounded check. -ConfidenceLevel::Level3 is a runtime heuristic, NOT Mathesis Grade 3. +First written 2026-11-01 on `arena/68c18146-echidnabot`, based on +`ab26bd54c8bdc04da8cc48c0778a25eb774be268`. Updated 2026-11-09 with the +first kernel receipts for the receipt-boundary theory, taken at +`1443adfabb98a9e0daea562bc8dbe764442c14cc` (<>), and with the +GraphQL authorisation obligations from #192 (<>). + +Tokens are the closed vocabulary of PROOF-POLICY §5: `proven`, +`proven-with-postulates`, `tested-only`, `argued`, `open`. A theory theorem +also carries a Proof Witness Grade (PWG, PROOF-POLICY §8) and, per leg, a +§2.2 correspondence state. The three are separate fields. A PWG is derived +from the receipts below, never asserted. `ConfidenceLevel::Level3` is a +runtime heuristic and is not a PWG. Policies and pinned references are in link:ESTATE-ROUTING-AUDIT.adoc[the routing audit]. Theory requires strict Agda checks, with separately recorded Rocq/Lean statement correspondence and -kernel results. Rust behaviour requires Creusot on actual first-party code; -a mathematical model does not establish runtime refinement. +kernel results. Rust behaviour is verified with Creusot (Pearlite contracts) +and Verus on the actual first-party code (PROOF-POLICY §1.2); a mathematical +model does not establish runtime refinement. == Local obligation ledger @@ -25,22 +32,30 @@ a mathematical model does not establish runtime refinement. |T-RECEIPT |A general evidence token does not imply its claim; `proofs/agda/ReceiptBoundary.agda` -|open -|AGDA-PENDING. `no-unconditional-reflection` constructs a contradiction -from unconditional reflection by instantiating Claim with Empty and evidence -with Unit. `receive-with-soundness` requires an explicit evidence-to-claim -function. This is new local theory, informed by epistemic-types, NOT a port -of that library or proof of the Rust parser. No external library or postulate. -|T-RECEIPT-ROCQ / T-RECEIPT-LEAN +|proven +|AGDA-VERIFIED (<>, R-AGDA). `no-unconditional-reflection` +constructs a contradiction from unconditional reflection by instantiating +Claim with Empty and evidence with Unit. `receive-with-soundness` requires +an explicit evidence-to-claim function. This is new local theory, informed +by epistemic-types, NOT a port of that library or proof of the Rust parser. +Import cone: this module alone, no libraries, no postulates. PWG: `PWG-3`, +derived; it owes both recheck legs until they count (§8.4). +|T-RECEIPT-LEAN |Same statements, quantification, evidence packaging and assumptions as -T-RECEIPT -|open -|Independent re-proof source candidates now exist under -`proofs/theory/{rocq,lean}/ReceiptBoundary.*`, without libraries, axioms or -admitted obligations. Neither was compiled; no transport or checked -correspondence exists. A Prop-only reformulation of Set-level quantification -is not silently interchangeable. The candidates deliberately use Rocq Set -and Lean Type rather than silently shrinking the claims to Prop. +T-RECEIPT; `proofs/theory/lean/ReceiptBoundary.lean` +|proven +|Route `re-proved`. LEAN-CHECKED, no axioms (<>, R-LEAN). +§2.2 state `BRIDGE-PENDING`: the statement comparison in +<> is agent-drafted and awaits owner review. Until then the +leg does not count towards a PWG. +|T-RECEIPT-ROCQ +|Same statements, quantification, evidence packaging and assumptions as +T-RECEIPT; `proofs/theory/rocq/ReceiptBoundary.v` +|proven +|Route `re-proved`. COQ-CHECKED, closed under the global context +(<>, R-ROCQ). §2.2 state `BRIDGE-PENDING`, as for the Lean leg. +The leg was checked with Coq 8.18.0, not a Rocq 9 release; the file uses +only the prelude (`Empty_set`, `unit`). |E-ADAPTER |`VeriSimEchidnaAdapter::prove` validates the gateway payload and propagates failure without calling a direct client @@ -85,10 +100,12 @@ is out of scope does NOT make that scaffolding verified. because there was no Agda record. It is not witness transport. Rocq/Lean Prop and Agda Set differ; correspondence is limited to propositional identity and remains `open` until checked and justified explicitly. - All three current executions are unavailable in this sandbox. + The Agda file checks under the strict profile (<>, R-AGDA); the + Rocq and Lean fixtures are prover test material (PROOF-POLICY §3), not + recheck legs. * `proofs/coq/admitted_stub.v` and `proofs/lean/sorry_stub.lean` are negative fixtures, not candidate proofs. Their escape hatches must stay intact. - They are excluded from Grade 3 counts, not repaired into passing fixtures. + They are excluded from PWG counts, not repaired into passing fixtures. * JSON files under `proofs/test_fixtures` are webhook/prover inputs, not proofs. === ABI scaffold debt (not verified) @@ -121,49 +138,188 @@ or layout contracts are invented in this patch. * Any future claim of theorem truth needs the relevant prover kernel/checker boundary and assumptions, separately from receipt transport. -== Toolchain acquisition attempt - -Published stable releases observed through GitHub's release API on 2026-11-01: -Rust 1.99.1; Agda 2.8.0.2; Creusot 0.14.0; Idris2 0.8.0; -Lean 4.35.0; Rocq 9.3.0; Cubicle 1.2.0. None was installed or run. -Creusot 0.14.0 itself pins `nightly-2026-08-03` with rustc-dev and llvm-tools; -it cannot simply be built against latest stable Rust. Its INSTALL requires -Cargo, opam/OCaml, Why3/Why3find and solver acquisition. - -Actual network observations: - -* `static.rust-lang.org` and `deb.debian.org`: TLS connection failed; - Debian HTTP also returned an empty reply. -* The Agda Linux release asset was requested through api.github.com; - its redirect to `release-assets.githubusercontent.com` failed TLS. -* The sandbox permits GitHub source/API and npm/PyPI registries, not the - distribution/package hosts needed by the normal installers. Unrelated npm - packages named agda/rustup are not substituted for trusted toolchains. - -Required environment help: provision verified toolchains through the session -setup, or allow the official distribution and package hosts (including release -assets and the dependencies required by opam). Cubical Agda is a mode of Agda, -not the separate Cubicle model checker. Full Cubical is not the canonical -proof profile and needs a separately reviewed exception where necessary. -The existing Rust pin is preserved until an actual tested toolchain update; -this is an unmet latest-stable target, not a completed upgrade. + +[[receipts]] +== Kernel receipts (2026-11-09, agent session) + +Taken at `1443adfabb98a9e0daea562bc8dbe764442c14cc` with the scripts below. +These are session receipts, not per-commit CI receipts: the `theory` job in +`.github/workflows/proof-safety.yml` repeats them on every pull request and +push to `main`, and its run is the receipt `PWG-1` would need (§8.2). + +[cols="1,2,3,2",options="header"] +|=== +|ID |Checker |Invocation and input digest |Observed result, axioms + +|R-AGDA +|Agda 2.8.0.2, official Linux release (archive sha256 +`2bcf24bb561b1be859bba841e5d67962d1616b3251bc147f878e4f60a2fbd9f7`) +|`./scripts/check-agda-proofs.sh`: `agda --safe --without-K +--cubical-compatible --exact-split --no-sized-types --no-guardedness +--no-libraries --no-default-libraries --ignore-interfaces`. +`ReceiptBoundary.agda` sha256 +`276ee4b56a9c2c7e7d8878162090785119bbbb141c359afc6d3352b0100c9014`; +`FixtureIdentity.agda` sha256 +`9c7b80b13f3507fc54f08b93e17190fc081c4cee00db0dd63d70c154746a91fb` +|Both modules accepted, exit 0. `--safe` refuses `postulate`; no library is +in the import cone. Negative controls: a planted `postulate` and a false +reflection proof were both refused (exit 42). + +|R-LEAN +|Lean 4.35.0, commit `eb6cafb7290e8bd5f2937522d8d804f58f02bafc` (release +archive sha256 +`7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d`) +|`./scripts/check-theory-rechecks.sh`: `lean +proofs/theory/lean/ReceiptBoundary.lean`. Source sha256 +`00ea31f061473e4ad48d06904c18d302c30d5b1443d6dd71afb863c8e328858f` +|Accepted, exit 0. `#print axioms`: none of the three theorems depends on +any axiom. Negative control: a planted `axiom` makes the leg fail. + +|R-ROCQ +|The Coq Proof Assistant 8.18.0 (OCaml 4.14.1), Ubuntu 24.04 `coq` +package `8.18.0+dfsg-1build2` +|`./scripts/check-theory-rechecks.sh`: `coqc -q ReceiptBoundary.v`. +Source sha256 +`ca65d1dd2c87cee49a10d26c0466b3ba812d183c71d44e965b9d14e99bf3e66d` +|Accepted, exit 0. `Print Assumptions`: all three closed under the global +context. Negative control: a planted `Admitted` makes the leg fail. +|=== + +[[correspondence]] +== Statement correspondence for T-RECEIPT (agent-drafted, awaiting review) + +Both recheck legs are re-proofs, not transports (§2). The comparison below +was made by reading the three files side by side. It was drafted by an agent +and is not yet reviewed, so each leg stays `BRIDGE-PENDING` and does not +count towards a PWG (§2.2, §8.2). On owner review it becomes `RECONCILED`, +and the PWG derived from these receipts would then be `PWG-2ii`. + +[cols="2,2,2,2",options="header"] +|=== +|Item |Agda |Lean 4 |Rocq + +|Small universe of claims and evidence +|`Set` (`--without-K`) +|`Type` (Type 0) +|`Set` (predicative) + +|Warrant record and its universe +|`Warrant Claim : Set₁`, fields `Evidence : Set`, `evidence : Evidence` +|`ReceiptWarrant Claim : Type 1`, same fields +|`ReceiptWarrant Claim : Type`, fields `evidence_type : Set`, +`evidence_token` + +|Soundness structure +|`SoundWarrant w : Set`, field `sound : Evidence w → Claim` +|`SoundReceiptWarrant w`, same field +|`SoundReceiptWarrant w : Type`, same field + +|Empty and unit +|local `Empty` (no constructors), local `Unit` +|core `Empty`, core `Unit` (`PUnit.{1}`) +|prelude `Empty_set`, `unit` + +|`receive-with-soundness` +|`(w : Warrant Claim) → SoundWarrant w → Claim` +|same quantification +|same quantification + +|`no-unconditional-reflection` +|`((Claim : Set) → Warrant Claim → Claim) → Empty` +|same, over `Type` +|same, over `Set` + +|`no-soundness-for-empty-token` +|`SoundWarrant empty-claim-token → Empty` +|same +|same +|=== + +Residual assumptions: none in any leg (no postulates, axioms or admitted +obligations). The match is between small predicative universes; none of the +three statements is about `Prop`, and none is moved there. + +[[rust-auth]] +== GraphQL authorisation obligations (#192) + +#192 added bearer authentication and per-field authorisation. Under +PROOF-POLICY §1.2 its behaviour is verified with Creusot (Pearlite contracts) +and Verus on the shipped functions. No verifier was run on it; it is covered +by unit, contract and smoke tests only, which are not proof receipts. Each +row is `open` until a verifier discharges it. + +[cols="1,3,2,2",options="header"] +|=== +|ID |Entrypoint and specification |Verifiers and assumptions |Status and next action + +|E-AUTH-SCOPE +|`RepoScope::allows` (`src/api/auth.rs`): true iff the slug is `owner/name` +with one `/`, both parts non-empty, and some pattern is that exact slug or +`owner/*` for that owner. No pattern admits every owner. +|Creusot/Pearlite and Verus. Assumes `str` equality, `split_once` and +`contains` behave as std documents (trusted extern specs). +|`open`. Tests: `scope_matches_exact_and_owner_wildcard_only`. Next: Pearlite +contract on a byte-slice core of the matcher. + +|E-AUTH-ROLE +|`ApiCredentials::authenticate`: the admin credential maps to `Admin`, the +route credential to `Route(scope)`, anything else to `None`; credentials +are trimmed on storage and on presentation alike. +|Creusot/Pearlite and Verus. `constant_time_eq` +(`src/trust/solver_integrity.rs`) is assumed to equal byte equality; its +timing property is outside both verifiers. +|`open`. Tests: `authenticate_maps_each_credential_to_its_role`, +`stored_credentials_are_trimmed_like_presented_ones`. + +|E-AUTH-GUARD +|`admin_only`, `route_or_admin`, `check_repo_scope`: with no principal every +guarded field is refused; `Route` reaches only `submitProofObligation`, and +only in scope. +|Creusot/Pearlite and Verus on the guard functions. async-graphql guard +dispatch is a trusted boundary (third party, §1.1). +|`open`. Tests: `schema_executed_without_a_principal_refuses_the_guarded_fields`, +`route_credential_cannot_reach_administrative_fields`. + +|E-RATE-BOUND +|`WebhookRateLimiter::check_ip` (`src/api/rate_limit.rs`): at most `limit` +admissions per peer per window; the peer map is swept when it reaches +`max(4096, 2 × size after the last sweep)`, and a sweep never drops a peer +with a request inside the window. +|Creusot/Pearlite and Verus. `Instant` monotonicity and `HashMap` behaviour +are trusted std boundaries. +|`open`. Tests: `idle_peers_are_swept_once_the_map_is_large`, +`active_peers_survive_a_sweep_and_stay_limited`. +|=== + +[[deviations]] +== Toolchain deviations (PROOF-POLICY §6) + +`D-THEORY-TOOLS`, state `open`. The `theory` job in +`.github/workflows/proof-safety.yml` installs its checkers outside a Guix +manifest or container, because this repository has neither: + +* Agda 2.8.0.2 from the official GitHub release archive, digest above; +* Lean 4.35.0 from `releases.lean-lang.org`, digest above; +* Coq 8.18.0 from the Ubuntu 24.04 archive (pinned by the runner image). + +Each script asserts the version it observes and fails on a mismatch. The +deviation closes when a Guix manifest or a proof-toolchain container provides +the same versions. == Reproduction and completion criteria -`./scripts/check-agda-proofs.sh` requires exactly Agda 2.8.0.2, ignores stale -interfaces, uses no external libraries, and runs the strict policy flags. -It prints source hashes, base revision and invocations. Capture the output -and record the observed result here; do not edit statuses based on expected -success. Its missing-tool failure was observed in this session (exit 127). -This is evidence that absence is not silently skipped, not a proof execution. - -`cargo test --locked dispatcher::verisim_echidna` and the existing protocol -suites remain unrun. Creusot, Idris2 and independent theory rechecks also -remain unrun. CI wiring for the new theory gate and its real positive/negative -controls is still open; a local check command is not an installed CI gate. - -Completion requires: actual checker receipts; backend protocol agreement; -production routing and provenance migration; implementation/interface proofs; -matched theory rechecks; preserved fixture detection; and regression tests. -This session has NOT completed old/new proof updating or the original routing -work. Documentation and unverified source candidates are partial progress only. +`./scripts/check-agda-proofs.sh` requires Agda 2.8.0.2 (first line of +`agda --version`; the official binary prints build flags after it), ignores +stale interfaces, uses no external libraries, and runs the strict policy +flags. `./scripts/check-theory-rechecks.sh` requires Lean at the version in +`proofs/theory/lean/lean-toolchain` and Coq 8.18.0, runs each leg's negative +control first, and fails unless every axiom report is clean. Both print +source hashes, base revision and invocations. Record the observed result +here; do not edit statuses on expected success. + +Still open: `cargo test --locked dispatcher::verisim_echidna`; Creusot and +Verus on any Rust obligation; Idris2 for I-GATEWAY; owner review of the +T-RECEIPT correspondence; and a Rocq 9 recheck if the estate pins one. +Completion requires backend protocol agreement, production routing and +provenance migration, implementation and interface proofs, and preserved +fixture detection. diff --git a/scripts/check-agda-proofs.sh b/scripts/check-agda-proofs.sh index 4ea20c0..d1f9670 100755 --- a/scripts/check-agda-proofs.sh +++ b/scripts/check-agda-proofs.sh @@ -9,7 +9,7 @@ if ! command -v agda >/dev/null; then echo 'OPEN: Agda 2.8.0.2 is required; no proof was checked.' >&2 exit 127 fi -actual=$(agda --version) +actual=$(agda --version | head -n 1) if [[ "$actual" != "$expected" ]]; then printf 'OPEN: expected %s, observed %s. Review the pin explicitly.\n' "$expected" "$actual" >&2 exit 1 diff --git a/scripts/check-theory-rechecks.sh b/scripts/check-theory-rechecks.sh new file mode 100755 index 0000000..731b5e7 --- /dev/null +++ b/scripts/check-theory-rechecks.sh @@ -0,0 +1,92 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Recheck legs of the receipt-boundary theory (PROOF-POLICY §2): Lean and Rocq. +# Each leg is an independent re-proof, not a transport of the Agda term. This +# script checks that each target kernel accepts its file with no axioms; the +# statement correspondence is recorded separately in docs/PROOF-STATUS.adoc. +# +# Both legs also run a negative control first: a planted axiom (Lean) and a +# planted Admitted (Rocq) must make the leg fail, so a green run means the +# check can see the failure it guards against. +set -euo pipefail +cd "$(dirname "${BASH_SOURCE[0]}")/.." + +lean_expected="version $(sed -n 's|^leanprover/lean4:v||p' proofs/theory/lean/lean-toolchain)" +rocq_expected='The Coq Proof Assistant, version 8.18.0' +work=$(mktemp -d) +trap 'rm -rf "$work"' EXIT + +require() { + if ! command -v "$1" >/dev/null; then + echo "OPEN: $1 is required; no proof was checked." >&2 + exit 127 + fi +} + +# lean_leg FILE: the kernel accepts FILE and every `#print axioms` line reports +# no axioms. Prints the observed output. +lean_leg() { + local out + out=$(lean "$1" 2>&1) || { printf '%s\n' "$out"; return 1; } + printf '%s\n' "$out" + local printed clean + printed=$(grep -c '#print axioms' "$1" || true) + clean=$(grep -c 'does not depend on any axioms' <<<"$out" || true) + [[ "$printed" -gt 0 && "$clean" -eq "$printed" ]] +} + +# rocq_leg FILE: coqc accepts FILE and every `Print Assumptions` is closed. +rocq_leg() { + local out + out=$(cd "$(dirname "$1")" && coqc -q "$(basename "$1")" 2>&1) || { printf '%s\n' "$out"; return 1; } + printf '%s\n' "$out" + local printed clean + printed=$(grep -c '^Print Assumptions' "$1" || true) + clean=$(grep -c 'Closed under the global context' <<<"$out" || true) + [[ "$printed" -gt 0 && "$clean" -eq "$printed" ]] +} + +printf 'Base commit (not a clean-tree claim): %s\n' "$(git rev-parse HEAD)" + +require lean +lean_actual=$(lean --version | head -n 1) +if [[ "$lean_actual" != *"$lean_expected,"* ]]; then + printf 'OPEN: expected Lean %s, observed %s.\n' "$lean_expected" "$lean_actual" >&2 + exit 1 +fi +printf 'Tool: %s\n' "$lean_actual" +cat >"$work/Planted.lean" <<'EOF' +axiom planted : False +theorem uses : False := planted +#print axioms uses +EOF +if lean_leg "$work/Planted.lean" >/dev/null; then + echo 'FAIL: the Lean leg accepted a planted axiom.' >&2 + exit 1 +fi +sha256sum proofs/theory/lean/ReceiptBoundary.lean +printf 'Invocation: lean proofs/theory/lean/ReceiptBoundary.lean\n' +lean_leg proofs/theory/lean/ReceiptBoundary.lean + +require coqc +rocq_actual=$(coqc --version | head -n 1) +if [[ "$rocq_actual" != "$rocq_expected" ]]; then + printf 'OPEN: expected %s, observed %s.\n' "$rocq_expected" "$rocq_actual" >&2 + exit 1 +fi +printf 'Tool: %s\n' "$rocq_actual" +cat >"$work/Planted.v" <<'EOF' +Lemma planted : False. +Admitted. +Print Assumptions planted. +EOF +if rocq_leg "$work/Planted.v" >/dev/null; then + echo 'FAIL: the Rocq leg accepted a planted Admitted.' >&2 + exit 1 +fi +cp proofs/theory/rocq/ReceiptBoundary.v "$work/" +sha256sum proofs/theory/rocq/ReceiptBoundary.v +printf 'Invocation: coqc -q ReceiptBoundary.v\n' +rocq_leg "$work/ReceiptBoundary.v" + +printf '%s\n' 'LEAN-CHECKED and COQ-CHECKED for these source hashes only; statement correspondence is recorded in docs/PROOF-STATUS.adoc.' From b9691cf4a8c58ef653155c2fb04ebad5d602cd70 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:15:18 +0000 Subject: [PATCH 05/10] ci(theory): restrict toolchain downloads to HTTPS; name the required tool SonarCloud (githubactions:S6506) flagged both archive downloads: curl -L follows redirects to any protocol. They now pass --proto =https and --tlsv1.2; the sha256 check after each download is unchanged. The script's require() binds $1 to a named local (shell:S7679). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- .github/workflows/proof-safety.yml | 4 ++-- scripts/check-theory-rechecks.sh | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml index d74a501..7b33ae9 100644 --- a/.github/workflows/proof-safety.yml +++ b/.github/workflows/proof-safety.yml @@ -49,14 +49,14 @@ jobs: - name: Install Agda 2.8.0.2 (digest-verified release) run: | mkdir -p "$RUNNER_TEMP/agda" - curl -fsSL -o "$RUNNER_TEMP/agda.tar.xz" "$AGDA_URL" + curl --proto "=https" --tlsv1.2 -fsSL -o "$RUNNER_TEMP/agda.tar.xz" "$AGDA_URL" echo "$AGDA_SHA256 $RUNNER_TEMP/agda.tar.xz" | sha256sum -c - tar -xJf "$RUNNER_TEMP/agda.tar.xz" -C "$RUNNER_TEMP/agda" echo "$RUNNER_TEMP/agda" >> "$GITHUB_PATH" - name: Install Lean 4.35.0 (digest-verified release) run: | mkdir -p "$RUNNER_TEMP/lean" - curl -fsSL -o "$RUNNER_TEMP/lean.tar.zst" "$LEAN_URL" + curl --proto "=https" --tlsv1.2 -fsSL -o "$RUNNER_TEMP/lean.tar.zst" "$LEAN_URL" echo "$LEAN_SHA256 $RUNNER_TEMP/lean.tar.zst" | sha256sum -c - tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP/lean" --strip-components=1 echo "$RUNNER_TEMP/lean/bin" >> "$GITHUB_PATH" diff --git a/scripts/check-theory-rechecks.sh b/scripts/check-theory-rechecks.sh index 731b5e7..e7bf982 100755 --- a/scripts/check-theory-rechecks.sh +++ b/scripts/check-theory-rechecks.sh @@ -17,8 +17,9 @@ work=$(mktemp -d) trap 'rm -rf "$work"' EXIT require() { - if ! command -v "$1" >/dev/null; then - echo "OPEN: $1 is required; no proof was checked." >&2 + local tool=$1 + if ! command -v "$tool" >/dev/null; then + echo "OPEN: $tool is required; no proof was checked." >&2 exit 127 fi } From 8acc85efaa462c2f9a11ef7fdca3cc724f3d1a43 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:01:27 +0000 Subject: [PATCH 06/10] proofs(theory): controls fail for the right reason; reword correspondence rows Review follow-ups on the recheck script and the proof-status ledger: - lean_leg counts only #print axioms commands at the start of a line, so a comment that mentions the command no longer breaks the count. - Both negative controls now require the planted file to compile and the checker to name the planted axiom before lean_leg / rocq_leg must refuse it. A compile error can no longer pass as a rejection. - The Lean and Rocq rows describe themselves as restatements whose match with T-RECEIPT is BRIDGE-PENDING, not as the same statements. - D-THEORY-TOOLS says Coq comes from the Ubuntu archive unpinned, with the script enforcing 8.18.0, instead of claiming the image pins it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- docs/PROOF-STATUS.adoc | 11 ++++++----- scripts/check-theory-rechecks.sh | 22 +++++++++++++++++++--- 2 files changed, 25 insertions(+), 8 deletions(-) diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index fec2173..74320ec 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -41,16 +41,16 @@ by epistemic-types, NOT a port of that library or proof of the Rust parser. Import cone: this module alone, no libraries, no postulates. PWG: `PWG-3`, derived; it owes both recheck legs until they count (§8.4). |T-RECEIPT-LEAN -|Same statements, quantification, evidence packaging and assumptions as -T-RECEIPT; `proofs/theory/lean/ReceiptBoundary.lean` +|A Lean restatement of T-RECEIPT, intended to match it; the match is not +yet confirmed (`BRIDGE-PENDING`). `proofs/theory/lean/ReceiptBoundary.lean` |proven |Route `re-proved`. LEAN-CHECKED, no axioms (<>, R-LEAN). §2.2 state `BRIDGE-PENDING`: the statement comparison in <> is agent-drafted and awaits owner review. Until then the leg does not count towards a PWG. |T-RECEIPT-ROCQ -|Same statements, quantification, evidence packaging and assumptions as -T-RECEIPT; `proofs/theory/rocq/ReceiptBoundary.v` +|A Rocq restatement of T-RECEIPT, intended to match it; the match is not +yet confirmed (`BRIDGE-PENDING`). `proofs/theory/rocq/ReceiptBoundary.v` |proven |Route `re-proved`. COQ-CHECKED, closed under the global context (<>, R-ROCQ). §2.2 state `BRIDGE-PENDING`, as for the Lean leg. @@ -300,7 +300,8 @@ manifest or container, because this repository has neither: * Agda 2.8.0.2 from the official GitHub release archive, digest above; * Lean 4.35.0 from `releases.lean-lang.org`, digest above; -* Coq 8.18.0 from the Ubuntu 24.04 archive (pinned by the runner image). +* Coq from the Ubuntu 24.04 archive. Nothing pins the package version; + `scripts/check-theory-rechecks.sh` requires 8.18.0 and fails otherwise. Each script asserts the version it observes and fails on a mismatch. The deviation closes when a Guix manifest or a proof-toolchain container provides diff --git a/scripts/check-theory-rechecks.sh b/scripts/check-theory-rechecks.sh index e7bf982..1a67cec 100755 --- a/scripts/check-theory-rechecks.sh +++ b/scripts/check-theory-rechecks.sh @@ -24,14 +24,15 @@ require() { fi } -# lean_leg FILE: the kernel accepts FILE and every `#print axioms` line reports -# no axioms. Prints the observed output. +# lean_leg FILE: the kernel accepts FILE and every `#print axioms` command (at +# the start of a line, so comments do not count) reports no axioms. Prints the +# observed output. lean_leg() { local out out=$(lean "$1" 2>&1) || { printf '%s\n' "$out"; return 1; } printf '%s\n' "$out" local printed clean - printed=$(grep -c '#print axioms' "$1" || true) + printed=$(grep -c '^#print axioms' "$1" || true) clean=$(grep -c 'does not depend on any axioms' <<<"$out" || true) [[ "$printed" -gt 0 && "$clean" -eq "$printed" ]] } @@ -61,6 +62,14 @@ axiom planted : False theorem uses : False := planted #print axioms uses EOF +# The control must fail for the right reason: the file compiles and Lean names +# the planted axiom, yet lean_leg still refuses it. A compile error would also +# make lean_leg fail, so it is ruled out first. +planted_out=$(lean "$work/Planted.lean" 2>&1) || { printf '%s\n' "$planted_out" >&2; echo 'FAIL: the Lean control did not compile.' >&2; exit 1; } +if ! grep -q 'depends on axioms: \[planted\]' <<<"$planted_out"; then + echo 'FAIL: Lean did not report the planted axiom.' >&2 + exit 1 +fi if lean_leg "$work/Planted.lean" >/dev/null; then echo 'FAIL: the Lean leg accepted a planted axiom.' >&2 exit 1 @@ -81,6 +90,13 @@ Lemma planted : False. Admitted. Print Assumptions planted. EOF +# As for Lean: the control compiles and coqc lists the admitted lemma as an +# axiom, so the refusal below is the axiom check, not a compile error. +planted_out=$(cd "$work" && coqc -q Planted.v 2>&1) || { printf '%s\n' "$planted_out" >&2; echo 'FAIL: the Rocq control did not compile.' >&2; exit 1; } +if ! grep -q '^planted : False' <<<"$planted_out"; then + echo 'FAIL: coqc did not list the planted Admitted.' >&2 + exit 1 +fi if rocq_leg "$work/Planted.v" >/dev/null; then echo 'FAIL: the Rocq leg accepted a planted Admitted.' >&2 exit 1 From 639742668b051b02aa15fef752febc9ad0579b93 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:05:50 +0000 Subject: [PATCH 07/10] proofs(theory): judge recheck legs by the checker's output The legs compared counts: flush-left query commands in the source against clean reports in the output. A query the source count missed (an indented #print axioms or Print Assumptions) could report an axiom and the leg still passed. Reproduced: appending an axiom-dependent theorem with an indented query to either receipt file was accepted. Each leg now fails on any axiom report in the output (Lean 'depends on axioms', coqc 'Axioms:'), and requires clean reports for at least every query command, indented or not. A query inside a block comment raises that floor without a report, so it fails closed. One control helper now runs flush-left and indented planted files for both legs, each required to compile and to report its axiom before the leg must refuse it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- scripts/check-theory-rechecks.sh | 96 +++++++++++++++++--------------- 1 file changed, 50 insertions(+), 46 deletions(-) diff --git a/scripts/check-theory-rechecks.sh b/scripts/check-theory-rechecks.sh index 1a67cec..754630f 100755 --- a/scripts/check-theory-rechecks.sh +++ b/scripts/check-theory-rechecks.sh @@ -5,9 +5,10 @@ # script checks that each target kernel accepts its file with no axioms; the # statement correspondence is recorded separately in docs/PROOF-STATUS.adoc. # -# Both legs also run a negative control first: a planted axiom (Lean) and a -# planted Admitted (Rocq) must make the leg fail, so a green run means the -# check can see the failure it guards against. +# Both legs also run negative controls first: a planted axiom (Lean) and a +# planted Admitted (Rocq), each queried flush-left and indented, must make the +# leg fail, so a green run means the check can see the failure it guards +# against. set -euo pipefail cd "$(dirname "${BASH_SOURCE[0]}")/.." @@ -24,28 +25,53 @@ require() { fi } -# lean_leg FILE: the kernel accepts FILE and every `#print axioms` command (at -# the start of a line, so comments do not count) reports no axioms. Prints the -# observed output. +# Both legs judge the checker's own output, not the source text, so a query +# the source count misses (indented, or produced some other way) still fails +# the leg if it reports an axiom. The source count only sets a floor: there +# must be at least as many clean reports as query commands. A query inside a +# block comment raises that floor without a report, so it fails closed. + +# lean_leg FILE: the kernel accepts FILE, no `#print axioms` report names an +# axiom, and the clean reports cover every query command. Prints the output. lean_leg() { local out out=$(lean "$1" 2>&1) || { printf '%s\n' "$out"; return 1; } printf '%s\n' "$out" - local printed clean - printed=$(grep -c '^#print axioms' "$1" || true) + local queries clean tainted + queries=$(grep -c '^[[:space:]]*#print axioms' "$1" || true) clean=$(grep -c 'does not depend on any axioms' <<<"$out" || true) - [[ "$printed" -gt 0 && "$clean" -eq "$printed" ]] + tainted=$(grep -c 'depends on axioms' <<<"$out" || true) + [[ "$tainted" -eq 0 && "$queries" -gt 0 && "$clean" -ge "$queries" ]] } -# rocq_leg FILE: coqc accepts FILE and every `Print Assumptions` is closed. +# rocq_leg FILE: coqc accepts FILE, no `Print Assumptions` report lists +# axioms, and the closed reports cover every query command. rocq_leg() { local out out=$(cd "$(dirname "$1")" && coqc -q "$(basename "$1")" 2>&1) || { printf '%s\n' "$out"; return 1; } printf '%s\n' "$out" - local printed clean - printed=$(grep -c '^Print Assumptions' "$1" || true) + local queries clean tainted + queries=$(grep -c '^[[:space:]]*Print Assumptions' "$1" || true) clean=$(grep -c 'Closed under the global context' <<<"$out" || true) - [[ "$printed" -gt 0 && "$clean" -eq "$printed" ]] + tainted=$(grep -c '^Axioms:' <<<"$out" || true) + [[ "$tainted" -eq 0 && "$queries" -gt 0 && "$clean" -ge "$queries" ]] +} + +# control LEG FILE REPORT COMPILE...: FILE must compile under COMPILE, the +# checker must print REPORT (it saw the planted axiom), and LEG must still +# refuse FILE. A compile error therefore cannot pass as a refusal. +control() { + local leg=$1 file=$2 report=$3 out + shift 3 + out=$("$@" 2>&1) || { printf '%s\n' "$out" >&2; echo "FAIL: control $(basename "$file") did not compile." >&2; exit 1; } + if ! grep -q -- "$report" <<<"$out"; then + echo "FAIL: control $(basename "$file") did not report its planted axiom." >&2 + exit 1 + fi + if "$leg" "$file" >/dev/null; then + echo "FAIL: $leg accepted control $(basename "$file")." >&2 + exit 1 + fi } printf 'Base commit (not a clean-tree claim): %s\n' "$(git rev-parse HEAD)" @@ -57,23 +83,11 @@ if [[ "$lean_actual" != *"$lean_expected,"* ]]; then exit 1 fi printf 'Tool: %s\n' "$lean_actual" -cat >"$work/Planted.lean" <<'EOF' -axiom planted : False -theorem uses : False := planted -#print axioms uses -EOF -# The control must fail for the right reason: the file compiles and Lean names -# the planted axiom, yet lean_leg still refuses it. A compile error would also -# make lean_leg fail, so it is ruled out first. -planted_out=$(lean "$work/Planted.lean" 2>&1) || { printf '%s\n' "$planted_out" >&2; echo 'FAIL: the Lean control did not compile.' >&2; exit 1; } -if ! grep -q 'depends on axioms: \[planted\]' <<<"$planted_out"; then - echo 'FAIL: Lean did not report the planted axiom.' >&2 - exit 1 -fi -if lean_leg "$work/Planted.lean" >/dev/null; then - echo 'FAIL: the Lean leg accepted a planted axiom.' >&2 - exit 1 -fi +printf 'axiom planted : False\ntheorem uses : False := planted\n#print axioms uses\n' >"$work/Planted.lean" +printf 'axiom planted : False\ntheorem uses : False := planted\n #print axioms uses\n' >"$work/Indented.lean" +for f in Planted Indented; do + control lean_leg "$work/$f.lean" 'depends on axioms: \[planted\]' lean "$work/$f.lean" +done sha256sum proofs/theory/lean/ReceiptBoundary.lean printf 'Invocation: lean proofs/theory/lean/ReceiptBoundary.lean\n' lean_leg proofs/theory/lean/ReceiptBoundary.lean @@ -85,22 +99,12 @@ if [[ "$rocq_actual" != "$rocq_expected" ]]; then exit 1 fi printf 'Tool: %s\n' "$rocq_actual" -cat >"$work/Planted.v" <<'EOF' -Lemma planted : False. -Admitted. -Print Assumptions planted. -EOF -# As for Lean: the control compiles and coqc lists the admitted lemma as an -# axiom, so the refusal below is the axiom check, not a compile error. -planted_out=$(cd "$work" && coqc -q Planted.v 2>&1) || { printf '%s\n' "$planted_out" >&2; echo 'FAIL: the Rocq control did not compile.' >&2; exit 1; } -if ! grep -q '^planted : False' <<<"$planted_out"; then - echo 'FAIL: coqc did not list the planted Admitted.' >&2 - exit 1 -fi -if rocq_leg "$work/Planted.v" >/dev/null; then - echo 'FAIL: the Rocq leg accepted a planted Admitted.' >&2 - exit 1 -fi +printf 'Lemma planted : False.\nAdmitted.\nPrint Assumptions planted.\n' >"$work/Planted.v" +printf 'Lemma planted : False.\nAdmitted.\n Print Assumptions planted.\n' >"$work/Indented.v" +for f in Planted Indented; do + # shellcheck disable=SC2016 # $1 and $2 are expanded by the inner sh, not here. + control rocq_leg "$work/$f.v" '^planted : False' sh -c 'cd "$1" && coqc -q "$2"' _ "$work" "$f.v" +done cp proofs/theory/rocq/ReceiptBoundary.v "$work/" sha256sum proofs/theory/rocq/ReceiptBoundary.v printf 'Invocation: coqc -q ReceiptBoundary.v\n' From 6b867753d77230b8210aa21b0e70d89fb14ec07d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:16:05 +0000 Subject: [PATCH 08/10] proofs(theory): query named theorems from the script, not the proof file The recheck legs still trusted the proof file in two ways: a theorem the file never queried went unchecked, and the file's own output could print a fake clean report. Both reproduced against 6397426's approach on paper; both are now refused in practice. Each leg now compiles the proof file as a module (lean -o; coqc -Q) and then runs a query file the script writes, asking #print axioms / Print Assumptions about a fixed list of the theorems the T-RECEIPT-LEAN and T-RECEIPT-ROCQ rows claim. Every named theorem must report no axioms; a missing name fails. The proof file's own output is not read. Checked locally: a required Lean theorem replaced by sorry, with its queries deleted and a forged clean line printed, is refused (sorryAx); a required Rocq theorem Admitted with its queries deleted is refused; a renamed theorem is refused; non-compiling controls fail the script. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- docs/PROOF-STATUS.adoc | 16 ++-- scripts/check-theory-rechecks.sh | 122 ++++++++++++++++--------------- 2 files changed, 74 insertions(+), 64 deletions(-) diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index 74320ec..64ce3df 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -169,20 +169,22 @@ reflection proof were both refused (exit 42). |Lean 4.35.0, commit `eb6cafb7290e8bd5f2937522d8d804f58f02bafc` (release archive sha256 `7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d`) -|`./scripts/check-theory-rechecks.sh`: `lean -proofs/theory/lean/ReceiptBoundary.lean`. Source sha256 +|`./scripts/check-theory-rechecks.sh`: `lean -o` compiles the file as a +module; a query file the script writes runs `#print axioms` on the three +named theorems. Source sha256 `00ea31f061473e4ad48d06904c18d302c30d5b1443d6dd71afb863c8e328858f` -|Accepted, exit 0. `#print axioms`: none of the three theorems depends on -any axiom. Negative control: a planted `axiom` makes the leg fail. +|Accepted, exit 0. None of the three theorems depends on any axiom. +Negative control: a planted `axiom` is reported and refused. |R-ROCQ |The Coq Proof Assistant 8.18.0 (OCaml 4.14.1), Ubuntu 24.04 `coq` package `8.18.0+dfsg-1build2` -|`./scripts/check-theory-rechecks.sh`: `coqc -q ReceiptBoundary.v`. -Source sha256 +|`./scripts/check-theory-rechecks.sh`: `coqc -q -Q . Recheck` compiles the +file as a module; one query file per theorem, written by the script, runs +`Print Assumptions` on it. Source sha256 `ca65d1dd2c87cee49a10d26c0466b3ba812d183c71d44e965b9d14e99bf3e66d` |Accepted, exit 0. `Print Assumptions`: all three closed under the global -context. Negative control: a planted `Admitted` makes the leg fail. +context. Negative control: a planted `Admitted` is reported and refused. |=== [[correspondence]] diff --git a/scripts/check-theory-rechecks.sh b/scripts/check-theory-rechecks.sh index 754630f..8b438a8 100755 --- a/scripts/check-theory-rechecks.sh +++ b/scripts/check-theory-rechecks.sh @@ -2,16 +2,27 @@ # SPDX-License-Identifier: MPL-2.0 # Recheck legs of the receipt-boundary theory (PROOF-POLICY §2): Lean and Rocq. # Each leg is an independent re-proof, not a transport of the Agda term. This -# script checks that each target kernel accepts its file with no axioms; the -# statement correspondence is recorded separately in docs/PROOF-STATUS.adoc. +# script checks that each target kernel accepts its file and that each named +# theorem below depends on no axioms; the statement correspondence is recorded +# separately in docs/PROOF-STATUS.adoc. # -# Both legs also run negative controls first: a planted axiom (Lean) and a -# planted Admitted (Rocq), each queried flush-left and indented, must make the -# leg fail, so a green run means the check can see the failure it guards -# against. +# The axiom queries are not taken from the proof file. Each leg compiles the +# file as a module, then asks about a fixed list of names from a query file +# this script writes. What the proof file prints, or leaves unqueried, cannot +# change the verdict. Both legs first run a negative control (a planted axiom, +# a planted Admitted) that must compile, be reported, and still be refused. set -euo pipefail cd "$(dirname "${BASH_SOURCE[0]}")/.." +# The theorems the T-RECEIPT-LEAN and T-RECEIPT-ROCQ rows claim. Keep these +# in step with docs/PROOF-STATUS.adoc. +lean_names=( + EchidnabotReceiptBoundary.receiveWithSoundness + EchidnabotReceiptBoundary.noUnconditionalReflection + EchidnabotReceiptBoundary.noSoundnessForEmptyToken +) +rocq_names=(receive_with_soundness no_unconditional_reflection no_soundness_for_empty_token) + lean_expected="version $(sed -n 's|^leanprover/lean4:v||p' proofs/theory/lean/lean-toolchain)" rocq_expected='The Coq Proof Assistant, version 8.18.0' work=$(mktemp -d) @@ -25,51 +36,52 @@ require() { fi } -# Both legs judge the checker's own output, not the source text, so a query -# the source count misses (indented, or produced some other way) still fails -# the leg if it reports an axiom. The source count only sets a floor: there -# must be at least as many clean reports as query commands. A query inside a -# block comment raises that floor without a report, so it fails closed. - -# lean_leg FILE: the kernel accepts FILE, no `#print axioms` report names an -# axiom, and the clean reports cover every query command. Prints the output. +# lean_leg FILE NAME...: Lean compiles FILE as a module, and a separate query +# file reports each NAME as depending on no axioms. Prints the query output. lean_leg() { - local out - out=$(lean "$1" 2>&1) || { printf '%s\n' "$out"; return 1; } + local file=$1 dir mod out name + shift + dir=$(mktemp -d -p "$work") + mod=$(basename "$file" .lean) + cp "$file" "$dir/$mod.lean" + (cd "$dir" && lean -o "$mod.olean" "$mod.lean" >/dev/null 2>&1) || { echo "lean rejected $file" >&2; return 1; } + { printf 'import %s\n' "$mod"; printf '#print axioms %s\n' "$@"; } >"$dir/Query.lean" + out=$(cd "$dir" && LEAN_PATH="$dir" lean Query.lean 2>&1) || { printf '%s\n' "$out"; return 1; } printf '%s\n' "$out" - local queries clean tainted - queries=$(grep -c '^[[:space:]]*#print axioms' "$1" || true) - clean=$(grep -c 'does not depend on any axioms' <<<"$out" || true) - tainted=$(grep -c 'depends on axioms' <<<"$out" || true) - [[ "$tainted" -eq 0 && "$queries" -gt 0 && "$clean" -ge "$queries" ]] + if grep -q 'depends on axioms' <<<"$out"; then return 1; fi + for name in "$@"; do + grep -qxF "'$name' does not depend on any axioms" <<<"$out" || return 1 + done } -# rocq_leg FILE: coqc accepts FILE, no `Print Assumptions` report lists -# axioms, and the closed reports cover every query command. +# rocq_leg FILE NAME...: coqc compiles FILE as a module, and one query file +# per NAME reports it closed under the global context. Prints the output. rocq_leg() { - local out - out=$(cd "$(dirname "$1")" && coqc -q "$(basename "$1")" 2>&1) || { printf '%s\n' "$out"; return 1; } - printf '%s\n' "$out" - local queries clean tainted - queries=$(grep -c '^[[:space:]]*Print Assumptions' "$1" || true) - clean=$(grep -c 'Closed under the global context' <<<"$out" || true) - tainted=$(grep -c '^Axioms:' <<<"$out" || true) - [[ "$tainted" -eq 0 && "$queries" -gt 0 && "$clean" -ge "$queries" ]] + local file=$1 dir mod out name + shift + dir=$(mktemp -d -p "$work") + mod=$(basename "$file" .v) + cp "$file" "$dir/$mod.v" + (cd "$dir" && coqc -q -Q . Recheck "$mod.v" >/dev/null 2>&1) || { echo "coqc rejected $file" >&2; return 1; } + for name in "$@"; do + printf 'From Recheck Require %s.\nPrint Assumptions Recheck.%s.%s.\n' "$mod" "$mod" "$name" >"$dir/Query.v" + out=$(cd "$dir" && coqc -q -Q . Recheck Query.v 2>&1) || { printf '%s\n' "$out"; return 1; } + printf '%s: %s\n' "$name" "$out" + [[ "$out" == 'Closed under the global context' ]] || return 1 + done } -# control LEG FILE REPORT COMPILE...: FILE must compile under COMPILE, the -# checker must print REPORT (it saw the planted axiom), and LEG must still -# refuse FILE. A compile error therefore cannot pass as a refusal. +# control LEG FILE NAME REPORT: LEG must refuse FILE, and its query output must +# contain REPORT, so the refusal is the axiom check and not a compile error. control() { - local leg=$1 file=$2 report=$3 out - shift 3 - out=$("$@" 2>&1) || { printf '%s\n' "$out" >&2; echo "FAIL: control $(basename "$file") did not compile." >&2; exit 1; } - if ! grep -q -- "$report" <<<"$out"; then - echo "FAIL: control $(basename "$file") did not report its planted axiom." >&2 + local leg=$1 file=$2 name=$3 report=$4 out + if out=$("$leg" "$file" "$name" 2>&1); then + echo "FAIL: $leg accepted control $(basename "$file")." >&2 exit 1 fi - if "$leg" "$file" >/dev/null; then - echo "FAIL: $leg accepted control $(basename "$file")." >&2 + if ! grep -q -- "$report" <<<"$out"; then + printf '%s\n' "$out" >&2 + echo "FAIL: control $(basename "$file") was refused without reporting its planted axiom." >&2 exit 1 fi } @@ -83,14 +95,13 @@ if [[ "$lean_actual" != *"$lean_expected,"* ]]; then exit 1 fi printf 'Tool: %s\n' "$lean_actual" -printf 'axiom planted : False\ntheorem uses : False := planted\n#print axioms uses\n' >"$work/Planted.lean" -printf 'axiom planted : False\ntheorem uses : False := planted\n #print axioms uses\n' >"$work/Indented.lean" -for f in Planted Indented; do - control lean_leg "$work/$f.lean" 'depends on axioms: \[planted\]' lean "$work/$f.lean" -done +printf 'axiom planted : False\ntheorem uses : False := planted\n' >"$work/Planted.lean" +control lean_leg "$work/Planted.lean" uses "'uses' depends on axioms: \[planted\]" sha256sum proofs/theory/lean/ReceiptBoundary.lean -printf 'Invocation: lean proofs/theory/lean/ReceiptBoundary.lean\n' -lean_leg proofs/theory/lean/ReceiptBoundary.lean +printf 'Invocation: lean -o ReceiptBoundary.olean ReceiptBoundary.lean, then #print axioms for:' +printf ' %s' "${lean_names[@]}" +printf '\n' +lean_leg proofs/theory/lean/ReceiptBoundary.lean "${lean_names[@]}" require coqc rocq_actual=$(coqc --version | head -n 1) @@ -99,15 +110,12 @@ if [[ "$rocq_actual" != "$rocq_expected" ]]; then exit 1 fi printf 'Tool: %s\n' "$rocq_actual" -printf 'Lemma planted : False.\nAdmitted.\nPrint Assumptions planted.\n' >"$work/Planted.v" -printf 'Lemma planted : False.\nAdmitted.\n Print Assumptions planted.\n' >"$work/Indented.v" -for f in Planted Indented; do - # shellcheck disable=SC2016 # $1 and $2 are expanded by the inner sh, not here. - control rocq_leg "$work/$f.v" '^planted : False' sh -c 'cd "$1" && coqc -q "$2"' _ "$work" "$f.v" -done -cp proofs/theory/rocq/ReceiptBoundary.v "$work/" +printf 'Lemma planted : False.\nAdmitted.\n' >"$work/Planted.v" +control rocq_leg "$work/Planted.v" planted '^Planted.planted : False' sha256sum proofs/theory/rocq/ReceiptBoundary.v -printf 'Invocation: coqc -q ReceiptBoundary.v\n' -rocq_leg "$work/ReceiptBoundary.v" +printf 'Invocation: coqc -q -Q . Recheck ReceiptBoundary.v, then Print Assumptions for:' +printf ' %s' "${rocq_names[@]}" +printf '\n' +rocq_leg proofs/theory/rocq/ReceiptBoundary.v "${rocq_names[@]}" printf '%s\n' 'LEAN-CHECKED and COQ-CHECKED for these source hashes only; statement correspondence is recorded in docs/PROOF-STATUS.adoc.' From 8947051f52f55c119e467d1c15be2f11e7f20ba6 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:22:23 +0000 Subject: [PATCH 09/10] docs(proof-status): record why both T-RECEIPT recheck legs are re-proved MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PROOF-POLICY §2 asks for Dedukti transport first and for the reason of any re-proof. The transport was tried on 2026-11-09 and failed at both steps: - Agda2Dedukti (c7c7d671, Agda 2.6.3 fork) translates its own tests, which Dedukti 2.7 accepts, but hits an internal Agda error on ReceiptBoundary.agda. Minimal modules isolate the trigger: a parameterised record in Set1. A data-type variant fails differently. - Lambdapi 4.0.0's new Lean exporter and its Rocq exporter drop rewrite rules, so Agda's rewrite-based encoding has no route out; a minimal rewrite theory exports to Lean that fails to type-check and Rocq that fails to parse. The Lean and Rocq rows now name the route and point at the record. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- docs/PROOF-STATUS.adoc | 37 +++++++++++++++++++++++++++++++++++-- 1 file changed, 35 insertions(+), 2 deletions(-) diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index 64ce3df..b738aaf 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -44,7 +44,8 @@ derived; it owes both recheck legs until they count (§8.4). |A Lean restatement of T-RECEIPT, intended to match it; the match is not yet confirmed (`BRIDGE-PENDING`). `proofs/theory/lean/ReceiptBoundary.lean` |proven -|Route `re-proved`. LEAN-CHECKED, no axioms (<>, R-LEAN). +|Route `re-proved`; transport was tried and failed (<>). +LEAN-CHECKED, no axioms (<>, R-LEAN). §2.2 state `BRIDGE-PENDING`: the statement comparison in <> is agent-drafted and awaits owner review. Until then the leg does not count towards a PWG. @@ -52,7 +53,8 @@ leg does not count towards a PWG. |A Rocq restatement of T-RECEIPT, intended to match it; the match is not yet confirmed (`BRIDGE-PENDING`). `proofs/theory/rocq/ReceiptBoundary.v` |proven -|Route `re-proved`. COQ-CHECKED, closed under the global context +|Route `re-proved`; transport was tried and failed (<>). +COQ-CHECKED, closed under the global context (<>, R-ROCQ). §2.2 state `BRIDGE-PENDING`, as for the Lean leg. The leg was checked with Coq 8.18.0, not a Rocq 9 release; the file uses only the prelude (`Empty_set`, `unit`). @@ -241,6 +243,37 @@ Residual assumptions: none in any leg (no postulates, axioms or admitted obligations). The match is between small predicative universes; none of the three statements is about `Prop`, and none is moved there. +[[transport]] +=== Why both legs are re-proved: the Dedukti transport attempt (2026-11-09) + +PROOF-POLICY §2 asks for transport through Dedukti first. It was tried for +T-RECEIPT in an agent session and failed at both steps, so both legs fall +back to re-proof (§2, "Re-proof as fallback"). + +. *Agda to Dedukti.* Agda2Dedukti at `c7c7d671` (the only Agda-to-Dedukti + translator; it builds against a Deducteam fork of Agda reporting 2.6.3) + translates its own test files (`dependantRecord`, `box`), and Dedukti 2.7 + accepts them. It does not translate `ReceiptBoundary.agda`: + * the fork rejects `--cubical-compatible`; a copy differing only by that + flag was used; + * on that copy the translator stops with an internal Agda error + (`__IMPOSSIBLE__`, `Agda/TypeChecking/Sort.hs:216`), in both its plain + and eta modes. Minimal modules isolate the trigger: a parameterised + record in `Set₁`, which is how `Warrant` is declared; + * a variant with `Warrant` as a `data` type (checked by Agda 2.8.0.2, so + a different source, not T-RECEIPT) fails differently: "Expected a + unrestricted argument, but found an erased argument". +. *Dedukti to Rocq and Lean.* Even a translated term would have no route + out. Lambdapi 4.0.0 (2026-11-05) adds a Lean exporter beside its Rocq + one, but both drop rewrite rules ("Command not translated") and turn + the theory's symbols into axioms. Agda's Dedukti encoding is built on + rewrite rules. On a three-line rewrite theory the exported Lean fails to + type-check, and the exported Rocq fails to parse. + +The statement comparison above is therefore by reading, and the legs stay +`BRIDGE-PENDING` until the owner reviews it. Retry the transport when +Agda2Dedukti tracks a current Agda or Lambdapi exports rewrite theories. + [[rust-auth]] == GraphQL authorisation obligations (#192) From 797276d300ca2a6e3e59a54c26475ff025fca47d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:35:29 +0000 Subject: [PATCH 10/10] docs(proof-status): correct the Lambdapi export failure The earlier Rocq parse error came from the test theory naming a symbol Prop, a keyword in Rocq and Lean. With the symbol renamed, both the Lean and the Rocq export fail to type-check, for the reason that matters: the rewrite rule is dropped, so the proof term loses its stated type. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- docs/PROOF-STATUS.adoc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc index b738aaf..8fd5d7e 100644 --- a/docs/PROOF-STATUS.adoc +++ b/docs/PROOF-STATUS.adoc @@ -267,8 +267,9 @@ back to re-proof (§2, "Re-proof as fallback"). out. Lambdapi 4.0.0 (2026-11-05) adds a Lean exporter beside its Rocq one, but both drop rewrite rules ("Command not translated") and turn the theory's symbols into axioms. Agda's Dedukti encoding is built on - rewrite rules. On a three-line rewrite theory the exported Lean fails to - type-check, and the exported Rocq fails to parse. + rewrite rules. On a five-line rewrite theory both exports fail to + type-check: with the rule gone, the proof term no longer has its stated + type. The statement comparison above is therefore by reading, and the legs stay `BRIDGE-PENDING` until the owner reviews it. Retry the transport when