reveal_strlit

Syntax

reveal_strlit_stmt ::= reveal_strlit ( string_literal ) ;

Proof operation

This reveals the contents of the string literal to the prover, including the length and the sequence of characters that compose the string. Otherwise, the string literal is treated as opaque data to avoid polluting the prover’s context with too much information.

Example

fn test() {
    let s = "abc";
    proof { reveal_strlit("abc"); }
    assert(s@[0] == 'a');
}