###############################################################################################
#                                                                                             #
#                                                                                             #
#   ____        _                 _     ____        __      _          ____                   #
#  |  _ \  __ _| |_ __ _ ___  ___| |_  / ___|  __ _/ _| ___| |_ _   _/ ___| _ __   ___  ___   #
#  | | | |/ _` | __/ _` / __|/ _ \ __| \___ \ / _` | |_ / _ \ __| | | \___ \| '_ \ / _ \/ __| #
#  | |_| | (_| | || (_| \__ \  __/ |_   ___) | (_| |  _|  __/ |_| |_| |___) |_) |  __/ (__  #
#  |____/ \__,_|\__\__,_|___/\___|\__| |____/ \__,_|_|  \___|\__|\__, |____/| .__/ \___|\___| #
#                                                                 |___/      |_|              #
#                                                                                             #
#                                                                                             #
###############################################################################################

Formal methods and runtime enforcement for safe data and model pipelines.

dataset-safety-specs is Lean-first: policy, lineage, optimizer, and shape specs live under src/DatasetSafetySpecs. Rust and Python guards in extracted/ are generated from those specs.

At a Glance

Area	What it provides
Formal specifications	Lean modules for lineage, policy predicates, optimizer invariants, and shape safety
Guard generation	Lean-first extraction to Rust and Python guard libraries
Runtime enforcement	Python safety kernel, compliance bundle generation, operational endpoints
Delivery controls	Strict CI, proof gating, dependency audits, and security scanning

Prerequisites

Tool	Notes
elan / Lean 4.7.0	Pin is in lean-toolchain
Python 3.9+	Runtime guards, parsers, regression suite
Rust stable	Optional; for extracted/rust tests
WSL2 (Windows)	Recommended for lake build / executables if native Windows linking fails

Quick Start (single path)

git clone https://github.com/SentinelOps-CI/dataset-safety-specs.git
cd dataset-safety-specs

# 1) Python toolchain (installs package from extracted/python via pyproject.toml)
pip install -r requirements-dev.txt
pip install -e .

# 2) Formal project
lake build

# 3) Quality gates (unified local DX)
make check
# or: bash scripts/dev_check.sh
#
# Equivalent pieces:
#   lake exe test_suite && lake exe lineage_regression_test
#   lake exe extract_guard && git diff --exit-code extracted/
#   pytest python/ extracted/python/tests -m "not slow"
#   cd extracted/rust && cargo test
#   python scripts/semantic_proof_gate.py

On Windows, if lake build fails at link/PE export time, run the same Lean commands under WSL2 from the mounted repo path. Native Windows PE linking is not a supported success criterion for this project; Python and Rust tests may still run natively. See docs/CAPABILITY_TEST_PLAN.md §15.

Common Workflows

Generate Guards (canonical)

lake exe extract_guard

Writes Lean-derived artifacts under:

• extracted/rust — Rust crate (ds_guard)
• extracted/python — Python package (ds_guard)

python/ds_guard/ is only a thin import shim that re-exports the generated package.

Verify Model Shape Safety

# End-to-end: Python ONNX parse on stdout → Lean verify_graph_shapes
lake exe shapesafe_verify path/to/model.onnx

# Optional: emit a Lean sketch (Bool check, not a forged trivial theorem)
python python/onnx2lean_shape.py path/to/model.onnx out.lean

Build Distribution Bundles

./bundle.sh bundle

Repository Layout

Path	Purpose
src/DatasetSafetySpecs	Lean source of truth (lineage, policy, optimizer, shape, guard extract)
python/	Parsers, safety kernel, compliance tooling, regression driver
extracted/	Generated Rust/Python guards and deploy packaging
tests/fixtures	Shared fixtures (e.g. PHI corpus)
.github/workflows	CI, formal verification, security, release

Runtime Operations

Generated server endpoints (ds_guard.server):

• /health
• /ready
• /metrics

Aligned with Docker/Kubernetes manifests under extracted/.

Quality and Security Standards

• Required CI checks fail hard (no permissive pass-through).
• Production proof-gated optimizer modules must not contain sorry / undocumented axiom.
• Policy guards are executable predicates from Policy.lean; PHI detection is corpus-evaluated in CI (recall/precision gates), not formal HIPAA/GDPR verification.
• Shape verification uses fail-closed graph propagation (verify_graph_shapes) with constraint unification for symbolic dims; wrong contracting dims are rejected.
• The Lean verify_gpt2_* helpers exercise a toy GPT-2-like Gemm/MatMul chain, not a full GPT-2 ONNX export. Real models: lake exe shapesafe_verify (MNIST + fixtures under test_models/).
• Security checks include static analysis, dependency audits, and secret scanning.

Documentation

• Module/API reference: docs/index.md
• Capability / soak / security test plan: docs/CAPABILITY_TEST_PLAN.md
• Contribution guide: CONTRIBUTING.md
• Risk register: RISK_REGISTER.md
• Security policy: SECURITY.md
• Release history: CHANGELOG.md

License

Licensed under MIT. See LICENSE.