<story><title>A Hoare Logic for Rust</title><url>http://ticki.github.io/blog/a-hoare-logic-for-rust/</url></story><parent_chain></parent_chain><comment><author>Animats</author><text>Nice. It makes sense to try to formalize the semantics of Rust&amp;#x27;s new intermediate representation, MIR.  It&amp;#x27;s much easier to get unambiguous semantics at that level. All name issues such as shadowing are gone, type issues have been resolved, and operations are machine-level unambiguous (not &amp;quot;+&amp;quot;, &amp;quot;32 bit unsigned add&amp;quot;).&lt;p&gt;An old project I worked on, the Pascal-F verifier,[1] from the early 1980s, worked in a similar way. We took the output from the first pass of the compiler, which was something like Java bytecode, and verified from that.&lt;p&gt;I found some old 9-track tapes of the sources recently, and I&amp;#x27;m going to run them through a data recovery service in Morgan Hill next week and see if I can bring the system back to life. It&amp;#x27;s a historical curiosity, but should be fun to play with on today&amp;#x27;s machines.  It was just too slow in 1982.  Meanwhile, I brought the original Boyer-Moore theorem prover back to life and put it on Github.[2]&lt;p&gt;Some of our lessons learned were:&lt;p&gt;1. Integrate the verification statements into the programming language.  Don&amp;#x27;t try to do it 
with comments. You want the language&amp;#x27;s regular syntax, type and variable checking to apply to the verification statements. We added the keywords ASSERT, ENTRY, EXIT, MEASURE, STATE, EFFECT, INVARIANT, DEPTH, and PROOF, EXTRA, and RULE.&lt;p&gt;2. Make verification program-like, not math-like. For example, if we wanted to verify the structure of a tree, we would add fields for a back-pointer and a tree depth to the data structure each node.  We&amp;#x27;d put in all the code to maintain them, and verify that the forward pointers and back pointers were consistent and that child objects always had a greater depth than their parents.  This would all be done by writing ordinary-looking code
with ASSERT statements.  But the new data fields would have the EXTRA attribute, and the code manipulating those fields would have PROOF in front of it.  This meant it was there only for verification purposes.  No executable code could depend on that data, so it could all be stripped out for execution.&lt;p&gt;3. Use two theorem provers.  One prover was an Oppen-Nelson decision procedure. This is
fully automatic proving for integer +, -, multiplication by constants, inequalities, conditionals, logic operators, structures, and arrays.  This subset of mathematics is decidable and there&amp;#x27;s a fast, complete decision procedure for it. That knocks off all the easy stuff automatically.  Easy stuff usually includes subscript checks and overflow checks.
The second prover was the Boyer-Moore prover, which is semi-automatic; you have to propose lemmas to help it along.  This is hard.  By using ASSERT statements to narrow the area
of trouble, you could reach the point where you had two successive ASSERTs, one of which should imply the other, but the Oppen-Nelson prover couldn&amp;#x27;t prove it and there was no
previously proved rule on file to cover it. But now the problem had been narrowed to an abstract mathematical problem - prove the second ASSERT from the first. Someone could work on that in the Boyer-Moore prover and then export the rule for use in the main system.
This provided a separation of functions - you could have mathematically oriented people to struggle with the theorem prover, independent of the code.  You could reuse
that rule elsewhere, and change other code without having to re-prove it.  Today, we&amp;#x27;d put files of useful theorems on Github.  We never let the user add &amp;quot;axioms&amp;quot;. That opens a huge hole.&lt;p&gt;4. Expect to do a lot of compiler-type analysis and bookkeeping as part of the verification process.  For example, the static analysis to determine that a function is pure (&amp;quot;pure&amp;quot; means x = y implies f(x) = f(y), and no side effects.) is something to do as a routine compiler operation.  Potential aliasing has to be discovered. Do this using compiler techniques; don&amp;#x27;t dump it into the theorems-to-be-proved mill, where it&amp;#x27;s much harder to give the programmer good error messages.&lt;p&gt;5. Don&amp;#x27;t fall in love with the formalism. Too much work in verification has been done by people who wanted to publish math papers, not kill program bugs.  This is about creating bug-free code.  I think people will get this now, but when I was doing this, everybody else involved was an academic.&lt;p&gt;[1] &lt;a href=&quot;http:&amp;#x2F;&amp;#x2F;www.animats.com&amp;#x2F;papers&amp;#x2F;verifier&amp;#x2F;verifiermanual.pdf&quot; rel=&quot;nofollow&quot;&gt;http:&amp;#x2F;&amp;#x2F;www.animats.com&amp;#x2F;papers&amp;#x2F;verifier&amp;#x2F;verifiermanual.pdf&lt;/a&gt;
[2] &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;John-Nagle&amp;#x2F;nqthm&amp;#x2F;tree&amp;#x2F;master&amp;#x2F;nqthm-1992&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;github.com&amp;#x2F;John-Nagle&amp;#x2F;nqthm&amp;#x2F;tree&amp;#x2F;master&amp;#x2F;nqthm-1992&lt;/a&gt;</text></comment>
<story><title>A Hoare Logic for Rust</title><url>http://ticki.github.io/blog/a-hoare-logic-for-rust/</url></story><parent_chain></parent_chain><comment><author>nickpsecurity</author><text>Nice description and first steps. Ideal moves would probably be the following:&lt;p&gt;1.Modifying front-end for Frama-C flow or similar tool to take a subset of Rust with specs, generate the VC’s, and feed them to supported provers. He seems to be doing something similar but Im sure there’s some good tools to build on.&lt;p&gt;2. For manual and high-assurance, embed Rust into Simpl&amp;#x2F;HOL that seL4 used. Do an AutoCorres tool with that. You now have ability to pull similar effort with translation validation to machine code. Next, extend COGENT to generate Rust subset Simpl supports. You can now do, like their C example, a whole filesystem functionally that outputs verified Rust or machine code. Optionally extend the COGENT tool with QuickCheck, QuickSpec, etc esp where tests&amp;#x2F;specs can translate to Rust to. Quite a foundation for other Rust developments to build on. Including redoing Rust compiler in COGENT at least for certified, reference version. ;)</text></comment>