SleanSlean

5. Format and API🔗

Choose a command for the question

  • validate <case.json>: does the case pass the supported rules? Output has ok: true or an error with code, event_id, and object_id; errors exit nonzero.

  • replay <case.json> <N>: what was the state after the first N events?

  • view <case.json> agent|owner: which observations, decisions, and relations are visible to that audience?

  • export <case.json> agent|owner: produce a versioned envelope with the canonical case and Lean version. Review it before sharing. Use export-case only when a consumer needs the legacy raw case.

  • timeline <case.json> agent|owner: get checked states at every visible prefix for the local Explorer.

  • proof <case.json> and proof-statement: inspect declared claims, local attestation eligibility, direct project dependencies and the project's one pinned theorem statement. For a clean committed build, python3 tools/attest_proof.py examples/formal-claim.json issues kernel_checked only with exact build and audience-filtered export digests. This uses trusted Lake, CLI and Python code; it is not an independent recheck.

Commands that read a case also accept - for standard input. For example, from the repository root:

lake exe slean view examples/valid.json agent

examples/valid.json uses schema 0.1.0. Schema 0.2.0 adds owner-only source records; 0.3.0 adds dependency_gate_recorded with all_of or any_of. In each case, schema_version and semantics_version must be a supported pair; Slean does not migrate cases implicitly. See schema/v0.1.0.schema.json, schema/v0.2.0.schema.json, and schema/v0.3.0.schema.json in the repository for exact fields. Exact decimals such as "0.002" are strings; null remains distinct from "0".

If you write Lean

The typed API can build the same kind of case. These declarations are checked as this manual compiles:

Slean.CaseFile : Type#check Slean.CaseFile Slean.replay (caseFile : Slean.CaseFile) (count : Nat := caseFile.events.size) : Except Slean.Diagnostic Slean.State#check Slean.replay Slean.assessExact (protocol : Slean.FrozenProtocol) (observation : Slean.Observation) : Except String String#check Slean.assessExact Slean.project (caseFile : Slean.CaseFile) (audience : String) : Slean.CaseFile#check Slean.project Slean.DependencyGate : Type#check Slean.DependencyGate

examples/Synthetic.lean contains the complete typed case. bash tests/check.sh compiles it and compares its bytes with the JSON fixture's export-case agent projection. Imported JSON proof-status text never grants kernel_checked; the CLI keeps even a matching local declaration at declared until the clean-build attester binds its receipt to exact artifacts.