L4YAML

3.4. What L4YAML Proves🔗

This page is the front-door answer to what L4YAML proves. Each card below embeds one headline theorem's functorial chain graph — the proof-term dependency structure extracted by the FGM theoremgraph tool — together with its plain-English summary and a ChainDepth tag that classifies how tightly the theorem's proof is pinned to the pipeline functions it names. The ChainDepth tags carry the honesty labelling from §Mind the Fibration Gap: deep theorems are canaries for silent behavioural drift, propBridge theorems delegate that role to a wrapped predicate, and weak theorems do not participate in the fibration at all.

Only the headline + categoryCapstone entries (~11 theorems) are embedded here; the full catalogue is published as the theorem-graphs-all.tar.gz asset on the graphs-latest release of L4YAML.FGM and is downloadable on demand. Per-module hierarchical browsing of the full catalogue inside this site is a planned step.

3.4.1. Pipeline Composition🔗

3.4.1.1. parseYaml_pipeline — deep🔗

1.1 — parseYaml decomposes as parseStream ∘ scanFiltered. The pipeline's decomposition capstone: every downstream soundness/completeness headline routes through it.

parseYaml_pipeline chain graph

  • ChainDepth: deep

  • Module: L4YAML.Proofs.Composition

3.4.2. Scanner🔗

3.4.2.1. scan_full_consumption — deep🔗

2.1 — a successful scan consumes the entire input. Rules out the common correctness trap where a scanner returns .ok after stopping early on an unexpected character.

scan_full_consumption chain graph

  • ChainDepth: deep

  • Module: L4YAML.Proofs.Scanner.ScanStrictCoupling

3.4.3. Parser🔗

3.4.3.1. parseStream_respects_grammar_unconditional — deep🔗

3.1 — the parser respects the YAML 1.2.2 grammar with no well-formedness precondition. The root anchor for the grammar- production chain.

parseStream_respects_grammar_unconditional chain graph

  • ChainDepth: deep

  • Module: L4YAML.Proofs.EndToEndCorrectness

3.4.4. End-to-End Correctness🔗

The two soundness variants (parse_sound_shallow and parse_sound_deep) are the fibration-gap worked example — see §Fibration Gap — Worked Example for the side-by-side walkthrough.

3.4.4.1. parse_sound_shallow — propBridge🔗

4.1 — parse .ok → ValidYamlProp. The shallow variant hides the pipeline stages inside the ValidYamlProp predicate; the chain walker cannot descend. Useful as a minimal soundness statement; not the canary.

parse_sound_shallow chain graph

  • ChainDepth: propBridge

  • Module: L4YAML.Proofs.EndToEndCorrectness

3.4.4.2. parse_sound_deep — deep🔗

4.1d — same soundness claim with every pipeline stage exposed in the type and each stage's lemma cited in the proof. The canary for silent code changes along parseYaml → parseYamlRaw → parseStream.

parse_sound_deep chain graph

  • ChainDepth: deep

  • Module: L4YAML.Proofs.EndToEndCorrectness

3.4.4.3. parse_complete — propBridge🔗

4.2 — ValidYamlProp → parse .ok. Completeness with the same Prop-wrapping shape as parse_sound_shallow; an engineering follow-up analogous to parse_sound_deep would expose the pipeline stages and cite the completeness lemmas directly.

parse_complete chain graph

  • ChainDepth: propBridge

  • Module: L4YAML.Proofs.EndToEndCorrectness

3.4.4.4. parse_deterministic — weak🔗

4.3 — parse is a function (same input, same output). Structurally weak: the proof is tactic-only and cites no project lemmas, so no functorial chain exists. Serves as a type-level sanity check on the API shape, not as a canary.

parse_deterministic chain graph

  • ChainDepth: weak (structural)

  • Module: L4YAML.Proofs.EndToEndCorrectness

3.4.5. Values — Soundness🔗

3.4.5.1. validYaml_construct — weak🔗

5.1 — constructing ValidYaml from a parse result is well-defined. Establishes that the packaging step from docs to ValidYaml respects the underlying invariants; the proof is structural and carries no fibration signal.

validYaml_construct chain graph

  • ChainDepth: weak (structural)

  • Module: L4YAML.Proofs.Soundness

3.4.6. Roundtrip🔗

3.4.6.1. universal_roundtrip — deep (🚧 sorry-reachable via 6.9)🔗

6.1 — the universal YAML round-trip property: emit ∘ parse is content-preserving up to contentEq. Fibration-aligned against the emitter/parser composition; carries a sorry marker via 6.9 pending the final stage's proof.

universal_roundtrip chain graph

  • ChainDepth: deep

  • Module: L4YAML.Proofs.Output.EmitterScannability

3.4.7. Grammar Production🔗

3.4.7.1. parse_strict_proof — deep (🚧 sorry-reachable via 7.2, 7.6)🔗

7.1 — parser acceptance implies InYamlLanguage. Bridges the parser-level chain to the grammar-production relation used by the Blueprint. Sorry-reachable via the scanner-side 7.2/7.6 lemmas.

parse_strict_proof chain graph

  • ChainDepth: deep

  • Module: L4YAML.Proofs.Production.DocumentProduction

3.4.8. Surface Coupling🔗

3.4.8.1. SIndent_zero — weak🔗

8.1 — bundle representative for character-level indent/character predicates. Structural lemma connecting the scanner's character-class tests to the SIndent surface predicate; does not itself expose a call chain.

SIndent_zero chain graph

  • ChainDepth: weak (structural)

  • Module: L4YAML.Proofs.Coupling.SurfaceCoupling

3.4.9. Generating graphs locally🔗

The theoremgraph tool lives in the L4YAML.FGM bridge project; see its tools/README.md for invocations. Common starting points:

cd ../L4YAML.FGM
lake build theoremgraph
lake exe theoremgraph --list                       # catalogue
lake exe theoremgraph --chain parse_sound_deep     # one chain DOT
lake exe theoremgraph --tier headline tmp/out      # headline tarball contents
lake exe theoremgraph tmp/graphs                   # full tree (≈400 DOTs)