diff --git a/.gitignore b/.gitignore index 9c9baff..146d0b9 100644 --- a/.gitignore +++ b/.gitignore @@ -17,3 +17,5 @@ output.s *.runtimeconfig.json tools/ std_lib/ +!gen/riscv_modexp.s +!gen/otbn_modexp.s \ No newline at end of file diff --git a/arch/otbn/printer.s.dfy b/arch/otbn/printer.s.dfy index df82a42..0882a27 100644 --- a/arch/otbn/printer.s.dfy +++ b/arch/otbn/printer.s.dfy @@ -413,6 +413,9 @@ class Printer { method Main() { + var comment := "/*\n This code is generated by the veri-titan project: https://github.com/secure-foundations/veri-titan\n*/\n"; + print(comment); + var p := new Printer({"modexp_var_3072_f4", "montmul"}); reveal va_code_modexp_var_3072_f4(); diff --git a/arch/riscv/printer.s.dfy b/arch/riscv/printer.s.dfy index 2a4d802..e8880ba 100644 --- a/arch/riscv/printer.s.dfy +++ b/arch/riscv/printer.s.dfy @@ -215,10 +215,14 @@ class Printer { var lcount: int; var depth: int; - constructor() + var printed: set; + var globls: set; + + constructor(globals: set) { lcount := 0; depth := 1; + globls := globals; } method printIndent() @@ -277,8 +281,30 @@ class Printer { print("call "); print(name); print("\n"); case Comment(com) => print(com); } -} + method printProc(code:code) + requires code.Function? + modifies this + { + var defs, res := getFunctions(code, {}, []); + + var i := 0; + while i < |res| + { + var func_name := res[i].0; + if func_name !in printed { + printed := printed + {func_name}; + if func_name in globls { + print(".globl "); print(func_name); print("\n"); + } + print(func_name); print(":\n"); + printCode(Block(res[i].1)); + printIndent(); print("ret\n\n"); + } + i := i + 1; + } + } +} method getFunctionsFromCodes(block: codes, defs: set, res: seq<(string, codes)>) returns (defs': set, res': seq<(string, codes)>) @@ -318,27 +344,15 @@ method getFunctions(c: code, defs: set, res: seq<(string, codes)>) defs', res' := defs, res; } -method printProc(code:code) - requires code.Function? -{ - print(".globl mod_pow"); print("\n"); - var defs, res := getFunctions(code, {}, []); - var printer := new Printer(); - - var i := 0; - while i < |res| - { - print(res[i].0); print(":\n"); - printer.printCode(Block(res[i].1)); - i := i + 1; - printer.printIndent(); print("ret\n\n"); - } -} method Main() { + var comment := "/*\n This code is generated by the veri-titan project: https://github.com/secure-foundations/veri-titan\n\n The mod_pow assembly snippet expects arguments in the following way:\n\n a0:\n @param d0inv Precomputed Montgomery constant, considered part of key d0inv=-n^(-1) mod R\n\n a1: \n @param out Output message as little-endian array\n\n a2:\n @param workbuf32 Work buffer, caller must verify this is 2 x RSANUMWORDS elements long.\n\n a3:\n @param rr Precomputed constant, (R*R) mod n, considered part of key\n\n a4:\n @param n Modulus of key\n\n a5:\n @param in Input signature as little-endian array\n\n It should correspond to this C signature:\n\n void mod_pow(const uint32_t d0inv,\n uint32_t *out,\n uint32_t *workbuf32,\n const uint32_t * rr,\n const uint32_t *n,\n uint32_t *in)\n*/\n"; + print(comment); + reveal va_code_mod_pow(); - printProc(va_code_mod_pow()); + var printer := new Printer({"mod_pow"}); + printer.printProc(va_code_mod_pow()); } } diff --git a/build.py b/build.py index 2eb7c9d..32579f1 100755 --- a/build.py +++ b/build.py @@ -44,10 +44,10 @@ def rules(): command = otbn-ld $in -o $out """ -OTBN_ASM_PATH = "gen/arch/otbn/otbn_modexp.s" -RISCV_ASM_PATH = "gen/arch/riscv/riscv_modexp.s" +OTBN_ASM_PATH = "gen/otbn_modexp.s" +RISCV_ASM_PATH = "gen/riscv_modexp.s" OTBN_TEST_ASM_PATH = "impl/otbn/run_modexp.s" -OUTPUT_ELF_PATH = "gen/impl/otbn/run_modexp.elf" +OUTPUT_ELF_PATH = "gen/run_modexp.elf" DLL_SOURCES = { "arch/otbn/printer.s.dfy": OTBN_ASM_PATH, @@ -372,8 +372,7 @@ def verify_dafny_proc(proc): def verify_single_file(target): if not os.path.exists(target): return - generate_dot_ninja() - target = os.path.relpath(target) + target = os.path.relpath(target) if target.endswith(".dfy"): target = get_ver_path(target) os.system("ninja -v " + target) diff --git a/gen/otbn_modexp.s b/gen/otbn_modexp.s new file mode 100644 index 0000000..8130eb8 --- /dev/null +++ b/gen/otbn_modexp.s @@ -0,0 +1,166 @@ +/* + This code is generated by the veri-titan project: https://github.com/secure-foundations/veri-titan +*/ +.globl modexp_var_3072_f4 +modexp_var_3072_f4: + bn.xor w31, w31, w31 << 0, FG0 + li x8, 4 + li x9, 3 + li x10, 4 + li x11, 2 + addi x19, x23, 0 + addi x20, x26, 0 + addi x21, x24, 0 + jal x1, montmul + loopi 12, 3 + bn.sid x8, 0(x21++) + addi x8, x8, 1 + nop + loopi 16, 9 + addi x19, x24, 0 + addi x20, x24, 0 + addi x21, x24, 0 + jal x1, montmul + loopi 12, 3 + bn.sid x8, 0(x21++) + addi x8, x8, 1 + nop + nop + addi x19, x23, 0 + addi x20, x24, 0 + addi x21, x24, 0 + jal x1, montmul + bn.add w31, w31, w31 << 0, FG0 + li x17, 16 + loopi 12, 5 + bn.movr x11, x8++ + bn.lid x9, 0(x16++) + bn.subb w2, w2, w3 << 0, FG0 + bn.movr x17++, x11 + nop + csrrs x2, 1984, x0 + andi x2, x2, 1 + li x8, 4 + bne x2, x0, label_0 + li x8, 16 + label_0: + addi x21, x24, 0 + loopi 12, 3 + bn.sid x8, 0(x21++) + addi x8, x8, 1 + nop + ret + +.globl montmul +montmul: + bn.lid x9, 0(x17) + bn.mov w2, w31 + loopi 12, 2 + bn.movr x10++, x11 + nop + loopi 12, 7 + bn.lid x11, 0(x20++) + addi x6, x16, 0 + addi x7, x19, 0 + jal x1, mont_loop + addi x16, x6, 0 + addi x19, x7, 0 + nop + li x8, 4 + li x10, 4 + ret + +mont_loop: + addi x22, x16, 0 + li x12, 30 + li x13, 24 + li x8, 4 + li x10, 4 + bn.lid x12, 0(x19++) + jal x1, mul256_w30xw2 + bn.movr x13, x8++ + bn.add w30, w27, w24 << 0, FG0 + bn.addc w29, w26, w31 << 0, FG0 + bn.mov w25, w3 + jal x1, mul256_w30xw25 + bn.mov w25, w27 + bn.mov w24, w30 + bn.lid x12, 0(x16++) + jal x1, mul256_w30xw25 + bn.add w27, w27, w24 << 0, FG0 + bn.addc w28, w26, w31 << 0, FG0 + loopi 11, 15 + bn.lid x12, 0(x19++) + bn.movr x13, x8++ + jal x1, mul256_w30xw2 + bn.add w27, w27, w24 << 0, FG0 + bn.addc w26, w26, w31 << 0, FG0 + bn.add w24, w27, w29 << 0, FG0 + bn.addc w29, w26, w31 << 0, FG0 + bn.lid x12, 0(x16++) + jal x1, mul256_w30xw25 + bn.add w27, w27, w24 << 0, FG0 + bn.addc w26, w26, w31 << 0, FG0 + bn.add w24, w27, w28 << 0, FG0 + bn.addc w28, w26, w31 << 0, FG0 + bn.movr x10++, x13 + nop + bn.add w24, w29, w28 << 0, FG1 + bn.movr x10++, x13 + bn.add w31, w31, w31 << 0, FG0 + csrrs x2, 1985, x0 + andi x2, x2, 1 + beq x2, x0, label_1 + li x12, 30 + li x13, 24 + addi x16, x22, 0 + li x8, 4 + loopi 12, 5 + bn.lid x13, 0(x16++) + bn.movr x12, x8 + bn.subb w24, w30, w24 << 0, FG0 + bn.movr x8++, x13 + nop + label_1: + li x8, 4 + li x10, 4 + ret + +mul256_w30xw2: + bn.mulqacc.z w30.0, w2.0, 0 + bn.mulqacc w30.1, w2.0, 64 + bn.mulqacc.so w27.L, w30.0, w2.1, 64, FG0 + bn.mulqacc w30.2, w2.0, 0 + bn.mulqacc w30.1, w2.1, 0 + bn.mulqacc w30.0, w2.2, 0 + bn.mulqacc w30.3, w2.0, 64 + bn.mulqacc w30.2, w2.1, 64 + bn.mulqacc w30.1, w2.2, 64 + bn.mulqacc.so w27.U, w30.0, w2.3, 64, FG0 + bn.mulqacc w30.3, w2.1, 0 + bn.mulqacc w30.2, w2.2, 0 + bn.mulqacc w30.1, w2.3, 0 + bn.mulqacc w30.3, w2.2, 64 + bn.mulqacc.so w26.L, w30.2, w2.3, 64, FG0 + bn.mulqacc.so w26.U, w30.3, w2.3, 0, FG0 + ret + +mul256_w30xw25: + bn.mulqacc.z w30.0, w25.0, 0 + bn.mulqacc w30.1, w25.0, 64 + bn.mulqacc.so w27.L, w30.0, w25.1, 64, FG0 + bn.mulqacc w30.2, w25.0, 0 + bn.mulqacc w30.1, w25.1, 0 + bn.mulqacc w30.0, w25.2, 0 + bn.mulqacc w30.3, w25.0, 64 + bn.mulqacc w30.2, w25.1, 64 + bn.mulqacc w30.1, w25.2, 64 + bn.mulqacc.so w27.U, w30.0, w25.3, 64, FG0 + bn.mulqacc w30.3, w25.1, 0 + bn.mulqacc w30.2, w25.2, 0 + bn.mulqacc w30.1, w25.3, 0 + bn.mulqacc w30.3, w25.2, 64 + bn.mulqacc.so w26.L, w30.2, w25.3, 64, FG0 + bn.mulqacc.so w26.U, w30.3, w25.3, 0, FG0 + ret + diff --git a/crypto_examples/rsa_verify/rv32imc/mod_pow.s b/gen/riscv_modexp.s similarity index 81% rename from crypto_examples/rsa_verify/rv32imc/mod_pow.s rename to gen/riscv_modexp.s index 63d985e..90001af 100644 --- a/crypto_examples/rsa_verify/rv32imc/mod_pow.s +++ b/gen/riscv_modexp.s @@ -1,3 +1,35 @@ +/* + This code is generated by the veri-titan project: https://github.com/secure-foundations/veri-titan + + The mod_pow assembly snippet expects arguments in the following way: + + a0: + @param d0inv Precomputed Montgomery constant, considered part of key d0inv=-n^(-1) mod R + + a1: + @param out Output message as little-endian array + + a2: + @param workbuf32 Work buffer, caller must verify this is 2 x RSANUMWORDS elements long. + + a3: + @param rr Precomputed constant, (R*R) mod n, considered part of key + + a4: + @param n Modulus of key + + a5: + @param in Input signature as little-endian array + + It should correspond to this C signature: + + void mod_pow(const uint32_t d0inv, + uint32_t *out, + uint32_t *workbuf32, + const uint32_t * rr, + const uint32_t *n, + uint32_t *in) +*/ .globl mod_pow mod_pow: addi sp, sp, -32