L4YAML

3.2. Key Theorems🔗

The following capstone theorems represent the main formal guarantees established by L4YAML. Each is machine-checked by the Lean kernel with zero axioms beyond the built-in foundations.

Each theorem is accompanied by a bipartite dependency graph showing the implementation functions it proves properties about (blue, left) and the supporting theorems used in its proof (green, right). Stdlib lemmas surface in orange when they are domain-relevant.

3.2.1. Pipeline Composition🔗

These theorems establish that the scanner and parser compose correctly into a single end-to-end pipeline.

Theorem

Module

Statement

parseYaml_pipeline

Composition

End-to-end: scan then parse composes correctly. If scanFiltered produces tokens and parseStream accepts them, then parseYaml succeeds with the same result.

parseYamlRaw_pipeline

Composition

Raw pipeline variant without schema resolution.

parseYamlRaw_ok_decompose

Composition

Every successful parseYamlRaw result decomposes into a successful scan step followed by a successful parse step.

parseYaml_ok_iff

Completeness

parseYaml succeeds if and only if the input is valid YAML — the bridge between the implementation and the specification.

3.2.1.1. parseYaml_pipeline🔗

parseYaml_pipeline dependency graph

3.2.1.2. parseYamlRaw_pipeline🔗

parseYamlRaw_pipeline dependency graph

3.2.1.3. parseYamlRaw_ok_decompose🔗

parseYamlRaw_ok_decompose dependency graph

3.2.1.4. parseYaml_ok_iff🔗

parseYaml_ok_iff dependency graph

3.2.2. Scanner Correctness🔗

Properties of the character-to-token scanner:

Theorem

Module

Statement

scan_produces_valid_tokens

ScannerCorrectness

The scanner output satisfies ValidTokenStream: every emitted token is well-formed, positions are monotonically increasing, and the stream is bracketed by STREAM_START/STREAM_END.

advance_offset_lt

ScannerProgress

Scanner advance strictly increases the byte offset when the offset is within bounds — this is the core termination lemma.

scanLoop_success_emits_streamEnd

ScannerCorrectness

A successful scan loop always terminates with a STREAM_END token.

3.2.2.1. scan_produces_valid_tokens🔗

scan_produces_valid_tokens dependency graph

3.2.2.2. advance_offset_lt🔗

advance_offset_lt dependency graph

3.2.2.3. scanLoop_success_emits_streamEnd🔗

scanLoop_success_emits_streamEnd dependency graph

3.2.3. Parser Correctness🔗

Properties of the token-to-AST parser:

Theorem

Module

Statement

parseStream_sound

ParserSoundness

If the parser produces an AST, it corresponds to a valid YAML grammar derivation.

parseNode_anchors_grow

ParserNodeProofs

The anchor set grows monotonically through parseNode — anchors are never lost during parsing.

parseNode_aliases_resolve'

ParserNodeProofs

Every alias (*name) in the output of parseNode resolves to a previously defined anchor (&name).

parseStream_output_anchors_wellformed

ParserWfaProofs

After parseStream completes, all output anchors are well-formed: every alias target exists and every anchor body is Grammable.

3.2.3.1. parseStream_sound🔗

parseStream_sound dependency graph

3.2.3.2. parseNode_anchors_grow🔗

parseNode_anchors_grow dependency graph

3.2.3.3. parseNode_aliases_resolve'🔗

parseNode_aliases_resolve' dependency graph

3.2.3.4. parseStream_output_anchors_wellformed🔗

parseStream_output_anchors_wellformed dependency graph

3.2.4. Soundness🔗

Theorems establishing that the AST-to-value conversion faithfully implements the YAML specification:

Theorem

Module

Statement

toYamlValue_correct

Soundness

The toYamlValue function correctly implements the specification's construction rules.

nodeToValue_total

Soundness

Every well-formed AST node can be converted to a YamlValue — the conversion is total.

nodeToValue_deterministic

Soundness

AST-to-value conversion is deterministic: the same input always produces the same output.

scalar_content_preserved

Soundness

Scalar string content is preserved through the parsing pipeline — no characters are added, dropped, or reordered.

3.2.4.1. toYamlValue_correct🔗

toYamlValue_correct dependency graph

3.2.4.2. nodeToValue_total🔗

nodeToValue_total dependency graph

3.2.4.3. nodeToValue_deterministic🔗

nodeToValue_deterministic dependency graph

3.2.4.4. scalar_content_preserved🔗

scalar_content_preserved dependency graph

3.2.5. Round-Trip Properties🔗

Theorems about the parse → emit → parse cycle:

Theorem

Module

Statement

contentEq_refl

RoundTrip

Content equality is reflexive: every YAML value is content-equal to itself.

contentEq_symm

RoundTrip

Content equality is symmetric.

contentEq_trans

RoundTrip

Content equality is transitive — together with reflexivity and symmetry, this makes contentEq an equivalence relation.

emit_content_invariant

ScannerEmitBridge

The emitter preserves content equality: if two values are content-equal, their emitted canonical forms are identical.

escapeTag_roundtrip

RoundTrip

Tag URI escape and unescape are inverse operations.

3.2.5.1. contentEq_refl🔗

contentEq_refl dependency graph

3.2.5.2. contentEq_symm🔗

contentEq_symm dependency graph

3.2.5.3. contentEq_trans🔗

contentEq_trans dependency graph

3.2.5.4. emit_content_invariant🔗

emit_content_invariant dependency graph

3.2.5.5. escapeTag_roundtrip🔗

escapeTag_roundtrip dependency graph