Module package 

The portable proof package (logos-lean-package/1 and /2) and its replay.

Pure: a package is a map from published relative path to bytes. Writing it to disk atomically and running replay in a fresh process are the caller’s (largo lean); everything a replay decides is decided here, from the bytes alone, with no importer state.

Two proof contracts

The export decides which contract a package states, never the manifest. When the target’s closure, as LOGOS checks it, re-derives Lean’s native_decide steps by kernel evaluation (native_decide), the package is logos-lean-package/2; otherwise it is logos-lean-package/1.

• /1, the export’s proof as exported. lean_print_axioms, when the producing run observed Lean, names exactly the transitive assumptions.
• /2, the export’s proof with every native decision of the target’s closure re-derived. Its two assumption sets are kept apart: lean_print_axioms is Lean’s own report for the proof it replaced, required, naming ELIMINATED_AXIOM; and transitive is what the checked replacement rests on, which is exactly Lean’s report without that escape. Every declaration holding re-derived steps is disclosed as one INFORMATION_CATEGORY information change.

The schema is the result identity’s domain, so one set of files never carries both contracts’ identities.

What a package holds

manifest.json          schema, result id, the SHA-256 of every other file, source identity,
                       target (Lean name, kernel name, kind, universe parameters, statement,
                       LOGOS name), toolchain, transitive assumptions, information losses, the
                       trusted computing base, and the producing run's receipt
<Target>.lg            the LOGOS document: literate prose, English forms and kernel vernacular
certificate.json       the environment certificate (`logos-environment-certificate/1` or `/2`)
correspondence.json    Lean name ↔ kernel name ↔ LOGOS name (and document lines)
source/export.ndjson   the exact export the result was produced from
source/*.lean          the original Lean source, when the producing run had it

What a replay establishes, and what it does not

A replay reads nothing but the package. Before any checking work it enforces the file-count, byte, path and term limits, verifies every digest and the result identity, and requires every JSON file to be in its one canonical encoding. Then:

• primary_check — the certificate’s environment is rebuilt from the bare kernel, every inductive, constructor, definition, recursor, opaque theorem, structure η and quotient primitive kernel-validated under exact (not cumulative) conversion, with no obligation left.
• independent_recheck — every checked term was also inferred by the second kernel (recheck) to its declared type. A term outside that checker’s fragment makes the stage unsupported, never passed.
• translated — the statement is BOUND to the source: the reference translator (which shares no code with the importer) reads the target’s type from source/export.ndjson, and it must be exactly convertible with the certificate’s statement. Every other certificate declaration with a source counterpart is bound the same way, and the correspondence must agree. The manifest states the contract the carried export decides: its schema, and exactly the native re-derivations recomputed from the export.
• assumption_policy — the transitive assumptions of statement AND proof, traced through opaque theorems and definitions, are exactly Lean’s propext, Quot.sound and Classical.choice in their canonical form; an admission (sorryAx or anything of its universal-inhabitant shape) and an axiom stating the goal are refused by structure, not by spelling. Lean’s recorded report agrees with them as the contract says, and the manifest lists exactly them.
• emission_reparsed — the LOGOS document is exactly what the emitter writes for the rebuilt environment, it reparses in a fresh LOGOS session, and its target states the reference translation.
• fresh_replay — every stage above passed, from the package bytes alone.

lean_accepted is not_run: a replay never runs Lean. The producing run’s receipt is in the manifest, and a replay repeats what it says without adopting it.

Structs

AssumptionRecord

Build

A built package and the producing run’s receipt. A build never claims more than its receipt: assemble is the door that refuses to hand out a package whose receipt is not clean.

BuildOptions

What the producing run knows that the export does not say.

CorrespondenceFile

CorrespondenceRow

EmissionRecord

InformationLoss

LeanRun

A pinned Lean toolchain’s run over the original source.

Manifest

PackageLimits

Limits enforced on a package before any work.

SourceIdentity

StageRecord

TargetIdentity

Toolchain

Constants

ALLOWED_AXIOMS

Lean’s three standard axioms, in the kernel’s spelling of their Lean names — the only assumptions a verified result may rest on.

CERTIFICATE

CORRESPONDENCE

CORRESPONDENCE_SCHEMA

EXPORT

MANIFEST

NATIVE_REDERIVED_SCHEMA

The schema of a package whose proof is the export’s with the native decisions of the target’s closure re-derived by kernel evaluation.

PACKAGE_SCHEMA

The schema of a package whose proof is the export’s own, checked as exported.

PACKAGE_SCHEMAS

Every package schema this crate writes and replays.

REPLAY_SCHEMA

TRUSTED_BASE

The trusted computing base shared by the checks a package’s receipt names. Two checkers that share this much are two implementations of typing, not two independent theorem provers, and the manifest says so in every package.

Functions

assemble

Build the package for target from a Lean export, and require that every stage the producing run can establish passed. A package is returned only when it would replay clean.

assemble_observed

assemble_with, holding the result’s assumptions against what the pinned Lean’s own #print axioms reported for the target (Lean names), as the package’s contract says: any difference in either direction, and a native-rederived proof without Lean’s report, is an assumption_disagreement, and no package is handed out.

assemble_with

assemble with the producing run’s own evidence.

build

Build a package and its producing receipt. Refuses only when no package can be formed at all (an export the importer does not accept, a target it does not declare); a package whose checks fail is returned with the failure on its receipt, so a refusal can be inspected and replayed.

build_observed

build, with the pinned Lean’s #print axioms for the target when the producing run has it.

canonical_certificate

The certificate’s canonical encoding: compact, newline-terminated.

canonical_json

The one canonical encoding of a package JSON file: pretty-printed, newline-terminated.

document_path

The document’s file name for a Lean target: its name with anything outside letters, digits, _, - and . written as _, then .lg.

publish

Write a package to dir atomically: every file is written and synced in a staging directory beside it, which is then renamed into place. An existing dir is never replaced — a published result is immutable — and a failure leaves nothing behind.

publishable

The package of build, when every stage the producing run can establish passed and the package replays clean in this process; otherwise the first stage that did not pass, as a refusal.

read_directory

Read a package directory, enforcing the file-count, size and path limits before reading any content. Symbolic links and special files are refused.

receipt_document

The replay receipt as a logos-lean-replay/1 document.

replay

Replay a package from its bytes alone, under the default limits.

replay_with

Replay a package from its bytes alone, under limits.

result_id

The result identity of a logos-lean-package/1 package: the target and every non-manifest file’s path and digest.

result_id_in

The result identity under schema, which is the preimage’s domain: the same files under two contracts have two identities.

sha256_hex

The lowercase hexadecimal SHA-256 of bytes.

Type Aliases

PackageFiles

A package’s files, keyed by published relative path.