SAIL questions

[ben-marshall]

This is an issue to track on-going questions around the SAIL model.

• Q: Where is the best place to ask questions about SAIL?
• Q: Where is the best place to ask questions about the RISC-V model, implemented in SAIL?
• Q: What is the best way to tell if I have a problem with SAIL, or a problem with how RISC-V is specified using SAIL?
• Q: Why is SAIL able to generate a C-model for a given input X, but not an SMT model for the same input? This was a problem around the type checker and how side-effects of functions were declared.
• Q: What is the recommended way to structure instruction implementations to best support other uses of the SAIL model? e.g. is there a pattern for instruction implementation which lends itself well to partial extraction of that instruction from the rest of the model? Is this pattern different from the concise definitions which lend themselves well to being in-lined into the specification document?
• Q: How do we manage clarity v.s conciseness of the definitions? Some instructions will require substantial supporting code to implement e.g. AES, SHA2 vector instructions.
• Q: How can I know that by adding new instruction X, I haven't altered the behavior of existing instruction Y? The same question applies to underlying / supporting functions.
• Q: How should the pollentropy instruction be modeled, given that it's results are intrinsically non-deterministic? Can the model pre-load a set of prescribed return values? Could it be modeled as a simple LFSR? Do we need to support hinting of values?

[ben-marshall]

The following code snippet passes the SAIL compiler checks, but causes SAIL to generate invalid C-code.

/* AES Round Constant values, used by RV64 scalar AES instructions */
let aes_round_constants_table : list(bits(32)) = [|
0x00000001, 0x00000002, 0x00000004, 0x00000008, 0x00000010,
0x00000020, 0x00000040, 0x00000080, 0x0000001b, 0x00000036
|]

/* Lookup function - takes an index and a list, and retrieves the
 * x'th element of that list.
 */
val      rcon_lookup : (bits(4), list(bits(32))) -> bits(32)
function rcon_lookup (x, table) = {
    match (x, table) {
        (0x0 , t0::tn) => t0,
        ( y  , t0::tn) => rcon_lookup(x - 0x1,tn),
        (0x0 , _     ) => 0x00000000 /* Return 0 if out of bounds */
    }
}

val         aes_decode_rcon_imm : bits(4) -> bits(32)
function    aes_decode_rcon_imm (r) = {
    if(r==0xA) then 0x00000000 else rcon_lookup(r, aes_round_constants_table)
}

Error from GCC:

gcc -g  -I /opt/local/include -I /home/work/.opam/ocaml-base-compiler.4.06.1/share/sail/lib -I c_emulator -I c_emulator/SoftFloat-3e/source/include -fcommon -O3 -flto generated_definitions/c/riscv_model_RV64.c c_emulator/riscv_prelude.c c_emulator/riscv_platform_impl.c c_emulator/riscv_platform.c c_emulator/riscv_softfloat.c c_emulator/riscv_sim.c /home/work/.opam/ocaml-base-compiler.4.06.1/share/sail/lib/*.c -L /opt/local/lib -lgmp -lz c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC/softfloat.a -o c_emulator/riscv_sim_RV64
generated_definitions/c/riscv_model_RV64.c:41096:17: error: conflicting types for ‘pick_fbits’
 static uint64_t pick_fbits(const zz5listz8z5bv8z9 xs) { return xs->hd; }
                 ^~~~~~~~~~
generated_definitions/c/riscv_model_RV64.c:40922:17: note: previous definition of ‘pick_fbits’ was here
 static uint64_t pick_fbits(const zz5listz8z5bv32z9 xs) { return xs->hd; }
                 ^~~~~~~~~~
Makefile:254: recipe for target 'c_emulator/riscv_sim_RV64' failed

[kdockser]

These are really SAIL questions. Closing as there is nothing specific to do in the Vector Crypto Spec.