Decidable By Construction：面向真正无惧系统的设计时验证

View PDF HTML (experimental)

Abstract:Concurrency, parallelism and distributed execution become truly fearless when the compiler tracks wait-for edges, proves multi-threaded work is sound and preserves distributed boundary contracts. In this design, our Composer compiler preserves proofs while lowering Clef directly to native CPU, GPU, NPU and FPGA code, without translation through C or vendor APIs. Our Program Semantic Graph retains the values, relationships and premises that justify BAREWire's unboxed boundary contracts. And C & C++ interfacing is an explicit marshaling boundary, with proofs tied to actual arguments, conversions and returned values.
Four verification tiers connect an account of our design. Tier 1 supplies structural inference, founded on principal dimensional types. Tier 2 generates and checks local arithmetic, representation, and computational integrity at the node level. Tier 3 instantiates reusable domain and system lemmas, including distributed proofs supported by Iris, Actris and Aneris. Tiers 1-3 require no developer annotations, with a quotation based lemma library design to extend coverage as use cases expand. Tier 4 admits computational and probabilistic relational proofs, with project annotations identifying the required relations. We extend the same library direction toward recognizing relational constructions from hypergraph structure.
A formal composition rule connects arithmetic, ownership, protocol and realization evidence. Our worked distributed reduction preserves one specified result across concurrent workers, reordered arrivals and boundary mappings. Its probabilistic extension carries worker and conversion error with an explicit failure budget. With recent work by Urschel, we show bounds supply a relevant source of reusable proof terms. These constructions make verification a core engineering discipline for truly fearless programs and systems across a variety of hardware targets.

Comments:	33 pages, 0 figures, 4 tables. Major revision: expanded four-tier verification. Added exact and probabilistic distributed examples
Subjects:	Programming Languages (cs.PL); Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Logic in Computer Science (cs.LO)
Cite as:	arXiv:2603.25414 [cs.PL]
	(or arXiv:2603.25414v5 [cs.PL] for this version)
	https://doi.org/10.48550/arXiv.2603.25414 arXiv-issued DOI via DataCite

Submission history

From: Houston Haynes [view email]
[v1] Thu, 26 Mar 2026 13:09:36 UTC (21 KB)
[v2] Mon, 13 Apr 2026 23:17:30 UTC (23 KB)
[v3] Sun, 19 Apr 2026 15:17:01 UTC (24 KB)
[v4] Tue, 16 Jun 2026 01:22:57 UTC (24 KB)
[v5] Thu, 8 Oct 2026 14:51:48 UTC (43 KB)