Saw python api

[weaversa]

No description provided.

[WeeknightMVP]

Marking as Draft while changes remain underway.

Comments forthcoming...

[WeeknightMVP]

from saw_client import *

We should avoid wildcard imports. Import the package and use qualified names, or list each definition (with aliases to avoid any conflicts). Some relevant guiding principles from Tim Peters's Zen of Python:

Explicit is better than implicit.
Flat is better than nested.
Readability counts.
Special cases aren't special enough to break the rules.
Although practicality beats purity.
In the face of ambiguity, refuse the temptation to guess.
Namespaces are one honking great idea -- let's do more of those!

But the list of commonly used imports is a good idea. It should include ones from saw_client like (llvm_load_module, cryptol_load_file, llvm_verify, etc.)

[WeeknightMVP]

cry_f and friends are mostly a wrapper around formatted string literals called "f-strings". Mentioning this will give experienced Python programmers a quick head start.

[WeeknightMVP]

To check, we need to make a test:

Regarding unittest integration, saying that we need to do so is a bit strong. I'd go so far as to claim that such integration is more for developers to test the SAW Remote API than for users that call it. (Users can integrate it with other testing frameworks or omit testing frameworks entirely.) But it's convenient in this case.

self.assertTrue(result.is_success()) is a more compact form. (This assumes is_success returns a bool; otherwise self.assertIs(result.is_success(), True) is stronger due to "truthiness" interpretation of other types.)

[WeeknightMVP]

Good examples. Worth noting that they are so simple as to not really require loading a Cryptol file, though that demonstrates how one would organize a more complex verification effort. We might need to be ready to answer the question of what to do when definitions from multiple Cryptol files are needed...

[WeeknightMVP]

SAW does not have inductive reasoning capabilities.

For SAWScript and the SAW Remote API, this is true. But SAWCore terms can be formalized in Coq, a much more powerful theorem prover that has inductive reasoning (and many more) capabilities. This is obviously well beyond the scope of the course; I just think this statement should be clarified.

[WeeknightMVP]

An alternative to passing in lemmas is uninterpreting a funciton [sic]. This is useful when you don't care about the specifics of the values produced by a total function, but rather, the types of the value produced.

This is one case, yes. It is also useful in conjunction with overrides, reducing proof complexity by decomposing a complex specification into manageable logical steps (constrained by the overrides), much as verifying function implementations and using results as overrides does for the corresponding implementation. I am trying to communicate this in the pending salsa20-markdown salsa20-galois branch for Galois's Salsa20 example, which (when adapted to instruct the solver to uninterpret functions) naturally demonstrates the value of doing so for the same reason it so effectively demonstrates overrides -- the implementation was derived directly from the specification.

SMT: Equality Logic With Uninterpreted Functions describes how uninterpreted functions and constraints are applied to Satisfiability Modulo Theories.

[WeeknightMVP]

We use 3 double quotes """ in our cry_f call. This technique is useful when we want to separate our expected Cryptol-defined behaviors over multiple lines to improve code readability.

Nice! This results in wide open spaces when debugging strings passed to cry, cry_f, and friends, which can be mitigated using dedent from the textwrap package that comes with Python, e.g.:

from textwrap import dedent
# ...

    self.returns(cry(dedent("""
      (y, z)
        where
          y = "foo"
          z = "bar"
    """).strip()))

This renders (without leading/trailing whitespace) as:

(y, z)
  where
    y = "foo"
    z = "bar"

[WeeknightMVP]

character       = self.alloc(alias_ty("struct.character_t"))

This is probably supposed to be character_p.

[WeeknightMVP]

So maybe we tried being too fancy showing off our associative property knowledge.

One of those arithmetic properties, anyway...

[WeeknightMVP]

That is, was our assumption a fair one to make? If not, change the C code (possibly using different library functions) to match lg2 in Cryptol.

...and verify it!

[WeeknightMVP]

class ceilLog2Contract(Contract):

Initial-lowercase class names violate PEP 8 and coding practices in Python and most other OO languages. I usually name Contract instances Contract_{function}, which...also has its pros and cons:

Capitalized_Words_With_Underscores (ugly!)

(One of the pros is that you can dynamically associate a function name to its Contract subclass, for example to cache instances by arguments, and use that to defer lemma verification until verifying its caller. One of the cons is that it's bad practice to stovepipe associations in this way; probably better to use a decorator or metadata registry.)

[djmorel]

SAW alerted us about potentially undefined behavior mentioned in the C specification has the following to say about bit shifts:

This is a phrasal portmanteau, more commonly known as a grammatical error. Perhaps it could be rephrased to:

"SAW alerted us about potentially undefined behavior; the C99 standard specifies the following about bit shifts:"

(ISO 9899:2017 (C17) is a current specification with the same text.)

Updated SAW.md!

[djmorel]

SAW is telling us we forgot to add a precondition to assert our symbolic length agrees with our Python parameter self.length. This is an easy fix:

It is, but it's redundant, bad for checking (because all but one length chosen at random will ever satisfy the precondition, rendering most quickchecks vacuous), and imposes an unnecessary burden on the solver for proving. A more direct approach is to just execute self.length as a concrete value:

  self.execute_func(a_p, b_p, cry(self.length))

Updated SAW.md!

[djmorel]

We use 3 double quotes """ in our cry_f call. This technique is useful when we want to separate our expected Cryptol-defined behaviors over multiple lines to improve code readability.

Nice! This results in wide open spaces when debugging strings passed to cry, cry_f, and friends, which can be mitigated using dedent from the textwrap package that comes with Python, e.g.:

from textwrap import dedent
# ...

    self.returns(cry(dedent("""
      (y, z)
        where
          y = "foo"
          z = "bar"
    """).strip()))

This renders (without leading/trailing whitespace) as:

(y, z)
  where
    y = "foo"
    z = "bar"

Updated SAW.md!

[djmorel]

character       = self.alloc(alias_ty("struct.character_t"))

This is probably supposed to be character_p.

Taylor and I discussed renaming the variable earlier. All artifacts have been updated to be consistent.

[djmorel]

That is, was our assumption a fair one to make? If not, change the C code (possibly using different library functions) to match lg2 in Cryptol.

...and verify it!

Updated SAW.md! Also included CLZ (mentioned earlier in this pull request) as a hint.