• Verifying Higher-order Programs with the Dijkstra Monad
  N. Swamy, J. Weinberger, C. Schlesinger, J. Chen and B. Livshits

This paper consolidates and extends work described in two MSR technical reports into a single conference submission.

• Verification Condition Generation with the Dijkstra State Monad This report includes the metatheory of the Dijkstra state monad, including an elaboration into pure F*, a soundness theorem, a completeness theorem (of which the completeness result for JS* is a special case), and the first-order VC theorem.
• Towards JavaScript Verification with the Dijkstra State Monad This report provides more details about each of our examples, including a description of the VC generation algorithm specialized for JS*. We also discuss (in Section 6) a query compilation procedure mentioned in our submission that shows how a certain class of higher-order VCs can be compiled to a sequence of first-order queries.

In addition to the technical reports above, we refer readers to the following code samples and downloads for more information about our work.

prims.fst: This F* module includes the signature of the Dijkstra State Monad, a main contribution of our submission. The specific variant we use here shows a Dijkstra monad carrying a rich two-state invariant on the heap, the use of the same monad to reason about exceptions, exception handlers, and fatal errors. This is a combination of the "iDST" and "eDST" monads described in the paper.

JSVerify.fst: This is an extended version of the JSPrims library shown in our submission. As mentioned in that paper, due to space limitations, we presented a simplified version of JavaScript semantics, ignoring prototype chains, getters/setters, functions-as-objects, and other features of the language. JSVerify.fst shows our full specification, incorporating all these features. We also show an implementation of the library, verified mechanically against its specification using F*'s typechecker for the Dijkstra state monad. As mentioned in the paper, JSVerify.fst is the foundation for a verified compiler from F* to JavaScript, proven fully abstract in a POPL 2013 paper, described here.

The latest download (version 0.6-alpha) of the F* compiler and verifier, together with all our examples is available here. In the download zip file, the examples relevant to our submission can be found in the following directories---a Makefile in the relevant directories indicates how the examples can be verified:

• ex0--ex25 can be found in the directory examples/monadic
• ac can be found in the file examples/monadic/authac.fst
• automaton can be found in the file examples/monadic/automaton.fst
• iflow can be found in the file examples/monadic/iflow.fst
• auth can be found in the file examples/misc/auth.fst
• auth2 can be found in the file examples/misc/auth2.fst
• JSVerify can be found in the directory examples/jsverify
• Untiny can be found in the file examples/monadic/js/Untiny.js
• Delicious can be found in the file examples/monadic/js/Delicious.js
• Passward can be found in the file examples/monadic/js/Passward.js
• HoverMagn can be found in the file examples/monadic/js/HoverMagnifier.js
• Typograf can be found in the file examples/monadic/js/Typograf.js
• Facepalm can be found in the file examples/monadic/js/Facepalm.js

Forthcoming material:

• An updated web-facing version of our compiler, with JS tools