noethers-turnstile 0.3.0

Admissibility compiler: Γ ⊢ z : p until ε

Noethers Turnstile

Noethers Turnstile is an admissibility compiler for approximate consequential systems. Given a proof context Γ — a set of gap records, profiles, proof tokens, and authority constraints — it produces the strongest permission p the evidence supports and a binding expiry ε. The answer is a judgment in a typed form that the Rust borrow checker prevents from being read after it expires.

This library is for teams building systems where autonomous or consequential actions should be gated on structured evidence: calibration certificates, negative-control results, role assertions, scope restrictions. Noethers Turnstile handles the algebra; your domain supplies the certifiers.

Judgment form: Γ ⊢ z : p until ε

---

Documentation

Document	Description
docs/guide/introduction.md	When this design is needed, the basic idea, and when it does not fit
docs/guide/core-concepts.md	Vocabulary: bounded evidence, certifiable claims, gaps, profiles, tokens, envelopes, compilers, algebra
docs/guide/how-this-is-implemented.md	Judgment form, permission chain, gaps and profiles, tokens and provenance, structural non-promotion, certifier boundary, getting started
docs/guide/a-concrete-example.md	PGM inference memory-budget demo (OOC/DIA/AEX), AEX vs ALR distinction, model specification gap lesson
docs/papers/admissibility_compilers_for_approximate_consequential_systems.md	Core compiler paper: judgment form, permission algebra, gap/profile/token machinery, 19 structural theorems, PGM benchmark results
docs/papers/admissible_compilability_representation_theorem.md	Representation theorem: characterizes exactly when a domain admits a bounded sharp monotone compiler; WQO and semialgebraic corollaries
examples/epic/README.md	EPIC sepsis model experiment: blind gap induction from deployment failures, 100% FDA/NHS/EU AI Act coverage
examples/credit/README.md	Credit adverse-action experiment: 1-step induction recovers ECOA reason-traceability requirement
examples/ils/README.md	ILS approach geometry blind audit: compiler recovers FAA CAT I boundary from physics
examples/inference/README.md	Probabilistic inference compiler benchmarks: Ising, UAI, named Bayesian networks, 3GPP turbo codes, 150 tests

---

Permission Chain

Total order. OOC is the bottom (weakest). AAA is the top (strongest). Meet = min.

OOC < EXP < REF < UNS < ETA < ESC < ROL < DIA < REV < AEX < ALR < AAA

---

Parameterized permission chains

The compiler is parameterized over a permission chain — a validated total order of named levels plus role anchors (Bottom, ExpiryFloor, Refused, Unsatisfied, DisallowedUsesCeiling, BlockerThreshold, Top). The historical 12-level chain is the default and lives at PermissionChain::default_chain(). Callers may supply their own chain via compile_with_chain / compose_with_chain.

Every emitted Judgment carries the chain_hash of the chain that authorized it. A ChainRegistry trait + verify_published function let auditors mechanically check that the chain referenced by a judgment is published — publication is API, not prose.

See docs/specs/permission_chain_refactor_spec.md for the full design.

Quick Start — Rust (default chain)

use noethers_turnstile_core::{
    compile,
    context::{Membership, ProofContext, Scope},
    expiry::{Expiry, LiveJudgment, RuntimeContext},
    gap::{GapRecord, GapRequirement, Profile, RequiredStatus},
    permission::Permission,
    token::{compute_provenance_hash, ProofToken, TokenStatus},
};
use chrono::Utc;

// 1. Build a context with one gap that needs closing.
let claim_id = "my-claim";
let candidate_id = "z-001";
let context_id = "ctx-001";
let allowed_use = "diagnostics";

let hash = compute_provenance_hash(claim_id, candidate_id, context_id, allowed_use);

let ctx = ProofContext {
    claim_id: claim_id.into(),
    candidate_id: candidate_id.into(),
    context_id: context_id.into(),
    context_fingerprint: "fp-001".into(),
    allowed_use: allowed_use.into(),
    disallowed_uses: vec![],
    scope: Scope::default(),
    gaps: vec![GapRecord::closed("calibration-gap", "calibration_gap")],
    profiles: vec![Profile {
        permission: Permission::DIA(),
        required_gaps: vec![GapRequirement {
            gap_id: "calibration-gap".into(),
            minimum_status: RequiredStatus::ClosedRequired,
        }],
    }],
    tokens: vec![ProofToken {
        token_id: "tok-1".into(),
        token_type: "CALIBRATION_CERT".into(),
        schema_version: "0.1".into(),
        status: TokenStatus::Valid,
        closes_gaps: vec!["calibration-gap".into()],
        bounds_gaps: vec![],
        provenance_hash: hash,
        issued_at: Utc::now(),
        expires_at: None,
        issuer: "domain-certifier".into(),
        details: serde_json::Value::Null,
        is_negative_control: false,
    }],
    expiry: Expiry::never(),
    authority_ceiling: None,           // None = chain top (unconstrained)
    permission_ceiling: None,
    membership: Membership::InClass,
    expected_chain_hash: None,
};

// 2. Compile. The bare `compile` uses the default chain and stamps the
//    judgment with default_chain().chain_hash() so the decision is recorded
//    even when the default is implicit.
let judgment = compile(ctx).unwrap();
assert_eq!(judgment.permission, Permission::DIA());

// 3. Read through LiveJudgment (expiry check enforced by Rust borrow checker).
let rt = RuntimeContext::new(Utc::now(), "fp-001");
let live = noethers_turnstile_core::expiry::LiveJudgment::new(judgment, &rt);
assert_eq!(live.permission(), Permission::DIA());

Quick Start — Rust (custom chain)

use std::collections::HashMap;
use noethers_turnstile_core::{
    compile_with_chain,
    permission::{ChainRole, Permission, PermissionChain},
};

// Paper-style 5-level chain: REF < DIA < REV < AEX < ALR.
let levels = vec![
    Permission::new("REF"),
    Permission::new("DIA"),
    Permission::new("REV"),
    Permission::new("AEX"),
    Permission::new("ALR"),
];
let mut roles = HashMap::new();
roles.insert(ChainRole::Bottom, 0);
roles.insert(ChainRole::ExpiryFloor, 0);
roles.insert(ChainRole::Refused, 0);
roles.insert(ChainRole::Unsatisfied, 0);
roles.insert(ChainRole::DisallowedUsesCeiling, 0);
roles.insert(ChainRole::BlockerThreshold, 1);  // DIA
roles.insert(ChainRole::Top, 4);                // ALR
let chain = PermissionChain::new(levels, roles).expect("valid");

// Now compile against `chain` — the compiler's structural anchors come from
// the chain, never from naming a level literal.
// let judgment = compile_with_chain(ctx, &chain)?;

Audit-time publication check

use noethers_turnstile_core::{
    compile_with_chain, verify_published,
    permission::{InMemoryChainRegistry, PermissionChain},
};

let mut registry = InMemoryChainRegistry::new();
let chain = PermissionChain::default_chain().clone();
let hash = registry.publish(chain.clone());

// Compile a judgment under that chain.
// let judgment = compile_with_chain(ctx, &chain)?;
// verify_published(&judgment, &registry)?; // Ok — chain is published.

Composition

use noethers_turnstile_core::compose;

let composed = compose(ctx1, ctx2)?;
// Composition is non-promoting:
// compile(composed).permission <= min(compile(ctx1).permission, compile(ctx2).permission)

---

Quick Start — Python

import time
import noethers_turnstile as ts

# Compute provenance hash.
h = ts.compute_provenance_hash("my-claim", "z-001", "ctx-001", "diagnostics")

# Build a ProofToken.
token = ts.ProofToken(
    token_id="tok-1",
    token_type="CALIBRATION_CERT",
    schema_version="0.1",
    status="valid",
    closes_gaps=["calibration-gap"],
    bounds_gaps=[],
    provenance_hash=h,
    issued_at=time.time(),
    issuer="domain-certifier",
)

# Build the context.
ctx = ts.ProofContext(
    claim_id="my-claim",
    candidate_id="z-001",
    context_id="ctx-001",
    allowed_use="diagnostics",
    membership=ts.Membership.InClass,
    authority_ceiling=ts.Permission.AAA,
    expiry=ts.Expiry.never(),
    gaps=[ts.GapRecord("calibration-gap", "calibration_gap", status="closed")],
    profiles=[ts.Profile(
        ts.Permission.DIA,
        [ts.GapRequirement("calibration-gap", "closed")],
    )],
    tokens=[token],
)

# Compile.
live = ts.compile(ctx)
rt = ts.RuntimeContext(now_unix=time.time(), context_fingerprint="ctx-001")
print(live.permission_str(rt))  # "DIA"

Composition in Python

composed = ts.compose(ctx1, ctx2)
live = ts.compile(composed)
# Non-promotion guarantee holds automatically.

---

The 4 Structural Guarantees

Property	Description
Non-promotion under composition	compile(Γ₁ ⊗ Γ₂).permission ≤ min(compile(Γ₁), compile(Γ₂)) — composition cannot launder permission
Provenance enforcement	Tokens are accepted only when their SHA-256 provenance hash exactly matches (claim_id, candidate_id, context_id, allowed_use); no fuzzy matching
Expiry fires at boundary	LiveJudgment::permission() returns EXP for all now ≥ deadline; Rust borrow checker prevents stale reads
Evidence monotonicity	Adding a closed proof token to a context never lowers the emitted permission

All four properties are checked by proptest property-based tests on every run:

cargo test -p noethers-turnstile-tests

1098 tests total — 998 Rust (85 files) + 100 Python (8 files). Every test passes on every commit (ubuntu + macos CI matrix). The examples/inference/ benchmark adds a further 150 pytest tests.

---

Implementing a Certifier

The Certifier trait is the primary extension point. A certifier is the domain component that issues and validates proof tokens. Neither method is called by compile() — turnstile operates on tokens already present in the ProofContext snapshot. Your domain layer calls issue() to produce tokens before constructing the context, and may call validate() for pre-flight checks.

use noethers_turnstile_core::certifier::{Certifier, Evidence, IssueError, ValidationResult};
use noethers_turnstile_core::context::ProofContext;
use noethers_turnstile_core::token::{compute_provenance_hash, ProofToken, TokenStatus};
use chrono::Utc;

struct CalibrationCertifier;

impl Certifier for CalibrationCertifier {
    fn name(&self) -> &str { "calibration" }

    fn issue(&self, evidence: Evidence) -> Result<ProofToken, IssueError> {
        // Inspect evidence.payload, run domain checks, then emit a token.
        let ctx_tuple = serde_json::from_value::<(String,String,String,String)>(
            evidence.payload.clone()
        ).map_err(|e| IssueError::Internal(e.to_string()))?;

        Ok(ProofToken {
            token_id: uuid::Uuid::new_v4().to_string(),
            token_type: "CALIBRATION_CERT".into(),
            schema_version: "0.1".into(),
            status: TokenStatus::Valid,
            closes_gaps: vec!["calibration-gap".into()],
            bounds_gaps: vec![],
            provenance_hash: compute_provenance_hash(
                &ctx_tuple.0, &ctx_tuple.1, &ctx_tuple.2, &ctx_tuple.3,
            ),
            issued_at: Utc::now(),
            expires_at: None,
            issuer: "calibration-certifier".into(),
            details: evidence.payload,
            is_negative_control: false,
        })
    }

    fn validate(&self, token: &ProofToken, _ctx: &ProofContext) -> ValidationResult {
        if token.token_type == "CALIBRATION_CERT" {
            ValidationResult::ok()
        } else {
            ValidationResult::fail("wrong token type")
        }
    }
}

Turnstile's compiler does not call certifiers directly — it only inspects token provenance hashes and gap membership. Certifiers are called by your domain layer before tokens are placed in a ProofContext.

---

Caller Responsibilities

Two checks that the compiler does not enforce internally — callers must invoke them:

1. Scope candidate admission

The compiler does not verify that candidate_id ∈ scope.allowed_candidates. After compiling, check before acting on the judgment:

// Returns true when allowed_candidates is empty (unconstrained) or contains candidate_id.
fn candidate_in_scope(scope: &Scope, candidate_id: &str) -> bool {
    scope.allowed_candidates.is_empty()
        || scope.allowed_candidates.iter().any(|c| c == candidate_id)
}

if !candidate_in_scope(&ctx.scope, &ctx.candidate_id) {
    // reject — candidate is outside declared scope
}

2. Profile monotonicity (Law G01)

The compiler does not validate that profiles are monotone (stronger permissions require at least as strong evidence as weaker ones). Validate on profile construction:

// Returns an error message if profiles[i].permission > profiles[j].permission but
// profiles[i] declares a weaker gap requirement than profiles[j] for the same gap_id.
fn check_profile_monotonicity(profiles: &[Profile]) -> Option<String> {
    for i in 0..profiles.len() {
        for j in 0..profiles.len() {
            if profiles[i].permission <= profiles[j].permission { continue; }
            for req_j in &profiles[j].required_gaps {
                if let Some(req_i) = profiles[i].required_gaps.iter()
                    .find(|r| r.gap_id == req_j.gap_id)
                {
                    let rank = |r: RequiredStatus| match r {
                        RequiredStatus::OpenAllowed     => 0u8,
                        RequiredStatus::BoundedRequired => 1u8,
                        RequiredStatus::ClosedRequired  => 2u8,
                    };
                    if rank(req_i.minimum_status) < rank(req_j.minimum_status) {
                        return Some(format!(
                            "gap '{}': {} requires {:?} but {} requires {:?}",
                            req_j.gap_id,
                            profiles[i].permission, req_i.minimum_status,
                            profiles[j].permission, req_j.minimum_status,
                        ));
                    }
                }
            }
        }
    }
    None
}

---

Building

Rust

# Build everything.
cargo build

# Run all tests (unit + structural + property).
cargo test
cargo test -p noethers-turnstile-tests

# Run benchmarks.
cargo bench -p noethers-turnstile-core

Python (via maturin)

# Install maturin if needed.
pip install maturin

# Build and install in development mode.
python3 -m venv .venv && .venv/bin/pip install maturin pytest
.venv/bin/maturin develop

# Run the Python integration test suite.
.venv/bin/pytest

# Build a release wheel.
.venv/bin/maturin build --release

After maturin develop, the noethers_turnstile package is importable in the active environment.

---

Architecture

docs/guide/              Conceptual guides
  introduction.md        When this design is needed, the basic idea, where it does not fit
  core-concepts.md       Vocabulary: bounded evidence, certifiable claims, gaps, profiles, tokens, algebra
  how-this-is-implemented.md  Judgment form, permission chain, provenance, certifier boundary, getting started
  a-concrete-example.md  Concrete walkthrough: OOC/DIA/AEX, AEX vs ALR, model specification gap
docs/papers/             Research papers
  admissibility_judgement_for_approximate_consequential_systems_v10.md
                         Compiler paper: judgment form, 19 theorems, blind recovery results
  admissible_compilability_representation_theorem.md
                         Representation theorem: when a domain admits a sharp compiler

examples/epic/           EPIC sepsis model: blind gap induction from deployment failures
examples/credit/         Credit adverse-action: 1-step induction recovers ECOA requirement
examples/ils/            ILS approach geometry: blind audit recovers FAA CAT I boundary
examples/inference/      Probabilistic inference benchmarks (Ising/UAI/named nets/3GPP, 150 tests)

noethers-turnstile-core/          Pure Rust library (no PyO3 dependency)
  permission.rs          Permission enum + total order + algebra
  gap.rs                 GapStatus, GapRecord, Profile, GapRequirement
  token.rs               ProofToken, provenance hashing
  context.rs             ProofContext (Γ), Scope, Membership
  compiler.rs            compile() — descending search + structural meets
  composition.rs         compose() — lax monoidal composition
  expiry.rs              Expiry, RuntimeContext, LiveJudgment<'ctx>
  error.rs               TurnstileError hierarchy
  registry.rs            Append-only schema registry
  audit.rs               AuditEntry, Derivation, AuditStore trait
  certifier.rs           Certifier trait (main extension point)

noethers-turnstile-py/            PyO3 bindings (thin wrapper over turnstile-core)
  src/lib.rs             #[pymodule] + all #[pyclass] wrappers

noethers-turnstile-tests/         Structural and property-based tests (998 Rust tests)
  ec003*/                EC-003 theorem suite (composition algebra,
                         provenance, expiry, token status, OOC variants, …)
  ec004_*/               EC-004 profile well-formedness
  ec005_*/               EC-005 domain admission
  ec006_*                Law G01 profile monotonicity validator
  ec007_*                Derivation chain soundness (non-increasing steps)
  ec008_*                Concurrent AuditStore integrity
  ec009_*                Permission::from_str exhaustive coverage
  ec010_*                Scope candidate admission (rule [ADMISSIBLE])
  ec011_*                GapStatus min_status algebra invariants
  ec012_*                Priority tier dominance (T8, T10)
  ec013_*                Composition fail-closed on all conflict types
  ec014_*                SchemaRegistry append-only invariants R1–R7
  ec015_*                Disallowed-use accumulation (T13)
  ec016_*                Compile determinism (sequential + concurrent)
  ec017_*                Error type coverage (all variants reachable)
  ec018_*                Large-context stress (100–500 gaps, 200 tokens)
  ec019_*                T11 diagnostic/action separation (exhaustive)
  ec020_*                Token and context expiry edge cases
  ec021_*                MalformedContext validation (all 4 conditions)
  ec022_*                LiveJudgment<'ctx> runtime T15 contract
  ec023_*                descending() order stability (pinned sequence)
  ec024_*                Token expiry masking in composition
  ec025_*                BoundKind variant coverage (Numeric/SetValued/Infinity)
  ec026_*                Dead-token expiry semantics (only Valid triggers EXP)
  ec027_*                Compose claim_id/candidate_id semantics
  ec028_*                Provenance hash unicode and large inputs
  ec029_*                Poisoned-mutex recovery (SchemaRegistry + AuditStore)
  ec030_*                compile()/compose() never panic (adversarial inputs)
  ec031_*                Adversarial families A1–A10 (EC-001 §34)
  ec032_*                Positive families P1–P10 (EC-001 §34, in-class domains)
  ec033_*                Negative families N1–N10 (EC-001 §34, OOC exact)
  ec034_*                Permission tier semantics (T8, exhaustive 144-pair meet)
  ec035_*                Multi-profile descending search (determinism, S7–S12)
  ec036_*                Token liveness and freshness (L1–L15, EXP floor)
  ec037_*                Serde round-trip and wire-format stability (W1–W12)
  ec038_*                Scope intersection semantics (SI1–SI10, T14)
  ec039_*                Derivation and audit trail integrity (D1–D12, T18)
  ec040_*                Composition identity laws (CI1–CI8, T6 end-to-end)
  ec041_*                Allowed-use soundness (AU1–AU14, T12, byte-exact binding)
  ec042_*                Heterogeneous anti-laundering (H1–H16, T16, OOC absorbing)
  ec043_*                Audit-not-authority exhaustive (A1–A9, T18, replay attacks)
  ec044_*                Authority ceiling exhaustive (C1–C14, T19, hard cap)
  ec045_*                Permission triples exhaustive (TR1–TR5, all 1728 triples)
  ec046_*                Meet GLB property exhaustive (GLB1–GLB5, T8, greatest lower bound)
  ec047_*                Step 11 assembler truth table (S1–S16, T8/T11, tier dominance)
  ec048_*                Theorem 2 greatest-satisfiable (T2-1–T2-11, T5/T10)
  ec049_*                Admission contract A1–A9 depth (T6/T19, bounded-time, adversarial)
  ec050_*                Schema version adversarial (SV1–SV12, T2, mismatch/concurrent)
  proptest_*/            Property-based tests for the 4 structural guarantees
  step11_assembler       Assembler integration tests

python/tests/            Python integration tests (100 tests, pytest)
  test_py001_permission  Permission ordering, meet, from_str, hash
  test_py002_compile_basic  compile() outcomes: OOC/DIA/EXP/MalformedContext
  test_py003_live_judgment  LiveJudgment expiry, fingerprint, idempotence
  test_py004_compose     compose() identity inheritance, g2 token rejection
  test_py005_timestamps  Timestamp precision and EXP floor boundary behavior
  test_py006_exceptions  Exception hierarchy and message quality
  test_py007_types       GapRecord/Membership/NegativeControlStatus/ProofToken
  test_py008_derivation  Derivation steps, compiled_at, permission match

---

License

Apache 2.0. See LICENSE.