Skip to content

KYAML step 2/6 — comment-preservation proof (shared by Y-2 and Y-3) #1021

Description

@hyperpolymath

Step 2 of 6 in the KYAML adoption order fixed by 3-practice/YAML-POLICY.adoc §5.
Blocked by #1020 (landed ✅).

Work

The comment-preservation proof of §4 — shared by Y-2 (yq for writing) and
Y-3 (KYAML). Per §4 this proof is written once and satisfies both rules:
"Whichever of Y-2 or Y-3 reaches it first pays for it; the other inherits it.
Do not commission two proofs."

Gate (§5)

Round trip preserves every comment and its line association; idempotent under
cmp; a dropped-comment mutant dies.

Why this is the load-bearing step

§2.1: the pin comment is load-bearing. A rewrite that emits valid, running,
comment-stripped workflows has failed — §4 is explicit that parse-clean is
not the bar
. KEP-5295 itself warns that automated reformatting is lossy, because
go-yaml "does not always handle comments properly", so comments may be "formatted
wrongly, or lost entirely".

Acceptance criteria

  • Round-trip over the estate's real pin-comment corpus, not a toy fixture.
  • Every comment survives with its line association — a comment that
    survives but migrates to another key is a failure, not a pass.
  • Idempotent: a second pass is byte-identical under cmp.
  • A dropped-comment mutant dies. A green proof with no dead mutant is
    not evidence; assert the mutation was actually applied, and that the
    mutant parses, before believing its red.
  • The proof states which rewriter it covers (yq -i, a KYAML formatter, or
    both) — it does not generalise for free to a rewriter it never ran.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WRvDivYwLSeVCJUrfjic3f

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    priority:p2Normal - queue itproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtscope:estateAffects many or all repos across the estatestatus:readyFully specified and ready to be picked up

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions