For 4/20/05:
Title:
Deeply embedding Cryptol in ACL2: A challenge problem.
John Matthews
Abstract:
Cryptol is a declarative domain-specific language developed at Galois
Connections, Inc. for specifying crypto algorithms
(http://www.cryptol.net). In collaboration with Rockwell Collins, Inc.
and UT Austin, we are building a verifying compiler that will compile
Cryptol programs to efficient AAMP7 assembly code, and then generate an
ACL2 proof script that proves the compiled assembly code faithfully
implements the original Cryptol program.
To carry this out, we need to deeply embed the semantics of Cryptol in
ACL2. However, we have hit a roadblock. Simply put, we don't know how
to give a semantics for Cryptol streams in the finite-valued logic of
ACL2, that still lets us prove the expected stream laws in a reasonably
straightforward way. I'll present a stripped-down subset of Cryptol
that is just large enough to illustrate the issues, and then hopefully
we can all discuss possible solutions.