Tony's Wiki

Source-to-Source Encoding Correctness (double vision)

3 min read

Source-to-Source Encoding Correctness

The central correctness statement (2026-06-04) for the double-vision elaboration: a single-vision source-to-source encoding faithfully captures the double-vision rule.

The core claim

For a double-vision recursive module accepted by E-Typ-Rec-Double-Rec, the generated single-vision source encoding typechecks iff the two remaining double-vision obligations are satisfied: premise (5) is exactly the typing of the generated functor bodies F1/F2 under the strengthened internal view; premise (6) is exactly the final ascription/subtyping check when exporting I.X1/I.X2 back to the external signatures S1/S2. The intermediate recursive package I : Str is intentionally transparent; the abstraction boundary is restored only by the final module rec X1 : S1 = I.X1 and X2 : S2 = I.X2 export.

Proof-sketch skeleton

  1. Translation invariant. Str is the transparent internal recursive signature from the static pass + locator anchoring; generated F_i package component bodies behind functor arguments, so each body sees its own strengthened internal view and only the external view of siblings.
  2. Premise (5) ⇒ functor-body typing. By thm:locator-anchor, each anchor_L(τ_k) elaborates to the same canonical substitution as the lookup equations in premises (3)–(4); so checking sM_i in the double-vision rule is the same derivation as checking F_i’s body by E-Typ-Mod-AppFct.
  3. I is not where sealing happens. I = rec I : Str { X1=F1(I); X2=F2(I) } checks by single vision because Str exposes all witnesses; the argument coercion is a refinement check.
  4. Premise (6) ⇒ final export. Projection I.X1 has transparent signature Cup; E-Typ-Mod-Ascr against S1 requires exactly the subtyping judgment of premise (6). Symmetric for X2/S2.
  5. Conservativity / abstraction. Str exposes the internal view only inside I; generated functors stop components observing siblings’ private strengthening; final ascription hides the concrete view externally.

Open framing choices

Proofs (draft, for review)

Case-by-case proof attempt: the Modrec Proof Dossier — specifically Proof - Encoding adequacy iff (the iff above, with the two null-check lemmas), consuming Proof - Locator anchoring roundtrip and Proof - Double vision elaboration soundness. Caveat surfaced by the proof: the iff holds only on the double-vision fragment (where the static pass leaves Str fully transparent); this precondition needs adding to manual.tex:4956.

Double-Vision Recursive Modules · Locator-Anchored Signatures · Partial Recursive Signatures · project notes Source-to-source Encoding Examples Audit, Recursive Modules Paper Writing Log

Sources

2026-05-28, 2026-05-30, 2026-05-31, 2026-06-04

Graph View

Backlinks