Andrew Kennedy
ABSTRACT
We describe a Coq formalization of a subset of the x86 architecture. One emphasis of the model is brevity: using dependent types, type classes and notation we give the x86 semantics a makeover that counters its reputation for baroqueness. We model bits, bytes, and memory concretely using functions that can be computed inside Coq itself; concrete representations are mapped across to mathematical objects in the SSReflect library (naturals, and integers modulo 2n) to prove theorems. Finally, we use notation to support conventional assembly code syntax inside Coq, including lexically-scoped labels. Ordinary Coq definitions serve as a powerful "macro" feature for everything from simple conditionals and loops to stack-allocated local variables and procedures with parameters. Assembly code can be assembled within Coq, producing a sequence of hex bytes. The assembler enjoys a correctness theorem relating machine code in memory to a separation-logic formula suitable for program verification.
- B. Aydemir, A. Bohannon, M. Fairbairn, J. Foster, B. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. In 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 3603 of LNCS. Springer, 2005. Google Scholar
Digital Library
- N. Benton. A typed, compositional logic for a stack-based abstract machine. In 3rd Asian Symposium on Programming Languages and Systems (APLAS), volume 3780 of LNCS, 2005. Google ScholarDigital Library
- N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In 14th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM, 2009. Google ScholarDigital Library
- N. Benton, C-K. Hur, A. J. Kennedy, and C. McBride. Strongly typed term representations in Coq. J. Automated Reasoning, 49, 2011. Google ScholarDigital Library
- J. Boender and C. S. Coen. On the correctness of a branch displacement algorithm. Preprint arXiv:1209.5920, 2012.Google Scholar
- E. Brady and K. Hammond. Resource-safe systems programming with embedded domain specific languages. In 14th International Symposium on Practical Aspects of Declarative Languages (PADL), volume 7149 of LNCS. Springer, 2012. Google ScholarDigital Library
- T. Braibant and D. Pous. An efficient Coq tactic for deciding Kleene algebras. In 1st International Conference on Interactive Theorem Proving (ITP), volume 6172 of LNCS. Springer, 2010. Google ScholarDigital Library
- A. Chlipala. Modular development of certified program verifiers with a proof assistant. J. Functional Programming, 18(5/6), 2008. Google ScholarDigital Library
- A. Chlipala. Ur: statically-typed metaprogramming with type-level record computation. In 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 2010. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 2011. Google ScholarDigital Library
- Intel Corp. Intel 64 and IA-32 Architectures Software Developer's Manual. Volume 2 (2A, 2B & 2C): Instruction Set Reference, January 2013.Google Scholar
- P.-E. Dagand, A. Baumann, and T. Roscoe. Filet-o-Fish: practical and dependable domain-specific languages for OS development. SIGOPS Oper. Syst. Rev., 43(4):35--39, 2010. Google ScholarDigital Library
- A. Fox and M. O. Myreen. A trustworthy monadic formalization of the ARMv7 instuction set architecture. In 1st International Conference on Interactive Theorem Proving (ITP), volume 6172 of LNCS. Springer, 2010. Google ScholarDigital Library
- G. Gonthier. Advances in the formalization of the odd order theorem. In 2nd International Conference on Interactive Theorem Proving (ITP), volume 6898 of LNCS. Springer, 2011. Google ScholarDigital Library
- G. Gonthier, A. Mahboubi, and E. Tassi. A small scale reflection extension for the Coq system. Technical Report 6455, INRIA, 2011.Google Scholar
- J. B. Jensen, N. Benton, and A. J. Kennedy. High-level separation logic for low-level code. In 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 2013. Google ScholarDigital Library
- X. Leroy. Formal verification of a realistic compiler. Comm. ACM, 52 (7):107--115, 2009. Google ScholarDigital Library
- J. Strother Moore. Piton: A Verified Assembly-Level Language. Kluwer, 1996. Google ScholarDigital Library
- G. Morrisett, G. Tan, J. Tassarotti, J. B. Tristan, and E. Gan. Rocksalt: Better, faster, stronger SFI for the x86. In 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 2012. Google ScholarDigital Library
- D. P. Mulligan and C. Sacerdoti Coen. On the correctness of an assembler for the MCS-51 microprocessor. In 2nd International Conference on Certified Programs and Proofs (CPP), volume 7679 of LNCS. Springer, 2012. Google ScholarDigital Library
- M. O. Myreen. Verified just-in-time compiler on x86. In 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 2010. Google ScholarDigital Library
- R. Olinsky, C. Lindig, and N. Ramsey. Staged allocation: A compositional technique for specifying and implementing procedure calling conventions. In 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 2006. Google ScholarDigital Library
- N. Oury and W. Swierstra. The power of pi. In 13th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM, 2008. Google ScholarDigital Library
- L. Pike, N. Wegmann, S. Niller, and A. Goodloe. Experience report: a do-it-yourself high-assurance compiler. In 17th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM, 2012. Google ScholarDigital Library
- B. Spitters and van der Weegen. E. Type classes for mathematics in type theory. Math. Structures in Comp. Sci., 21:1--31, 2011.Google ScholarCross Ref
- G. Tan and A. W. Appel. A compositional logic for control flow. In 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 3855 of LNCS, 2006. Google ScholarDigital Library
- The Coq Development Team. The Coq Reference Manual, version 8.4, 2012. URL http://coq.inria.fr.Google Scholar
- H. Tuch, G. Klein, and M. Norrish. Types, bytes and separation logic. In 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 2007. Google ScholarDigital Library
Index Terms
- Coq: the world's best macro assembler?
Recommendations
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and ProofsThe completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Call-by-push-value in Coq: operational, equational, and denotational theory
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and ProofsCall-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) ...
LOGIC: A Coq Library for Logics
Dependable Software Engineering. Theories, Tools, and ApplicationsAbstractLOGIC is a Coq library for formalizing logic studies, concerning both logics’ applications and logics themselves (meta-theories). For applications, users can port derived rules and efficient proof automation tactics from LOGIC to their own program-...
Comments