Skip to content

README.md

Latest commit

 

History

History
73 lines (51 loc) · 3.44 KB

README.md

File metadata and controls

73 lines (51 loc) · 3.44 KB
################################################################################################
#            ____              _   _                ____        __      _                      #
#           |  _ \ _   _ _ __ | |_(_)_ __ ___   ___/ ___|  __ _/ _| ___| |_ _   _              #
#           | |_) | | | | '_ \| __| | '_ ` _ \ / _ \___ \ / _` | |_ / _ \ __| | | |            #
#           |  _ <| |_| | | | | |_| | | | | | |  __/___) | (_| |  _|  __/ |_| |_| |            #
#           |_| \_\\__,_|_| |_|\__|_|_| |_| |_|\___|____/ \__,_|_|  \___|\__|\__, |            #
#                                                                             |___/            #
################################################################################################

Lean-based runtime kernels engineered for reliability, auditability, and deterministic validation.

The project focuses on safety-critical runtime behavior across policy, concurrency, and shape handling, with strict documentation-to-gate alignment.

Why This Repository Exists

Runtime systems fail in production when guarantees are implicit, tests are brittle, or builds are environment-sensitive.
This repository hardens that path by making reliability properties explicit and mechanically checkable.

Reliability Guarantees

  • Canonical contracts: shared runtime-critical aliases live in src/RuntimeSafetyKernels/Contracts.lean.
  • Proof-hole enforcement: safety-critical modules must stay free of sorry, enforced by python scripts/check_proof_completeness.py.
  • Contract consistency: extraction paths are checked by python scripts/check_contract_consistency.py.
  • Resilient execution: validation runs with diagnostics, retry/backoff, and fallback runtime checks for unstable environments.

Quick Start

Run the full local reliability pipeline:

python scripts/validate_local.py

This command orchestrates diagnostics, gate checks, build, and runtime verification through a primary path plus fallback path where needed.

Build and Validation Tooling

Tool Purpose Output/Behavior
scripts/lake_doctor.py Collect environment, toolchain, and network diagnostics Writes build/lake-diagnostics.json
scripts/lake_resilient.py Execute lake commands with retry/backoff and timeout Improves reliability under flaky fetch/toolchain states
scripts/run_runtime_checks.py Run tests, fuzz, benchmarks Uses Windows-safe fallback from lake exe to lake env lean --run when native linking fails
scripts/validate_local.py Orchestrate full local validation Runs primary sequence, then fallback sequence on failure

Project Entry Points

  • Main module: src/RuntimeSafetyKernels.lean
  • Tests: src/RuntimeSafetyKernels/Tests.lean
  • Fuzz checks: src/RuntimeSafetyKernels/Fuzz.lean
  • Benchmarks: src/RuntimeSafetyKernels/Benchmarks.lean
  • Canonical contracts: src/RuntimeSafetyKernels/Contracts.lean

Fallback Lean runners used by runtime checks:

  • src/RuntimeSafetyKernels/Runner/TestsMain.lean
  • src/RuntimeSafetyKernels/Runner/FuzzMain.lean
  • src/RuntimeSafetyKernels/Runner/BenchmarksMain.lean

Documentation Map

  • API surface: docs/api.md
  • Contribution standards: CONTRIBUTING.md

Contribution Expectations

All changes are expected to preserve reliability guarantees, provide verification evidence, and keep documentation aligned with implementation reality.