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.