Native compilation changes how a program represents values and performs operations from processor to processor. In our view, proofs that justify source-level decisions must remain connected to those changes. We develop fixed-point scaffolding for this continuity in Clef and our Composer compiler. Our Program Semantic Graph retains types, joint constraints and proof dependencies. A thin MLIR middle end witnesses their settled consequences for native CPU, GPU, NPU and FPGA realization. The account connects nanopass traversal with preservation contracts, structural theorems and adjoint interfaces between reasoning modes. Four verification tiers organize automatic inference and reusable domain and system proofs, with probabilistic relations admitted at Tier 4. Established lower-tier facts can directly support richer derivations. We state conditions for composing lowering contracts and assembling compatible program segments, then show how their dependencies govern differential compilation after an edit. A worked foreign-call boundary follows source ranges through argument marshaling, the actual call and return conversion. Current FFI mechanisms bind checking evidence to those witnessed operations. A recent paper from Urschel provides elimination-growth bounds that supply a quantitative example. Reusable premises inform representation and error contracts that retain their sampling, arithmetic and exceptional-path assumptions. A further example admits value-indexed pairing through ordinary MLIR operations, connecting this scaffold to negative and fractional types. Together these constructions explain how a thin middle end can carry the consequences of rich source proofs into unboxed computation graphs. Integrity and efficiency share the same retained evidence. It justifies native realizations and identifies which analyses, proofs and lowered fragments remain reusable during development.

翻译：暂无翻译