Adds a SAW demo with exercises to adapt (a variant of) Galois's existing SAW script verifying their own Salsa20 implementation. This implementation is straightforwardly derived from their Cryptol spec, which in turn closely matches Dr. Daniel J. Bernstein's original Salsa20 specification, lending itself nicely to a compositional verification with overrides and uninterpreted functions that reflects the specification and implementation.
Adds a SAW demo with exercises to adapt (a variant of) Galois's existing SAW script verifying their own Salsa20 implementation. This implementation is straightforwardly derived from their Cryptol spec, which in turn closely matches Dr. Daniel J. Bernstein's original Salsa20 specification, lending itself nicely to a compositional verification with overrides and uninterpreted functions that reflects the specification and implementation.