Skip to content

Commit

Permalink
update the build slightly, add riscv printer output
Browse files Browse the repository at this point in the history
yizhou7 committed Feb 1, 2022

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
1 parent a1e2b09 commit 64a0f48
Showing 6 changed files with 240 additions and 24 deletions.
2 changes: 2 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -17,3 +17,5 @@ output.s
*.runtimeconfig.json
tools/
std_lib/
!gen/riscv_modexp.s
!gen/otbn_modexp.s
3 changes: 3 additions & 0 deletions arch/otbn/printer.s.dfy
Original file line number Diff line number Diff line change
@@ -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();
52 changes: 33 additions & 19 deletions arch/riscv/printer.s.dfy
Original file line number Diff line number Diff line change
@@ -215,10 +215,14 @@ class Printer {
var lcount: int;
var depth: int;

constructor()
var printed: set<string>;
var globls: set<string>;

constructor(globals: set<string>)
{
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<string>, res: seq<(string, codes)>)
returns (defs': set<string>, res': seq<(string, codes)>)
@@ -318,27 +344,15 @@ method getFunctions(c: code, defs: set<string>, 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());
}

}
9 changes: 4 additions & 5 deletions build.py
Original file line number Diff line number Diff line change
@@ -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)
166 changes: 166 additions & 0 deletions gen/otbn_modexp.s
Original file line number Diff line number Diff line change
@@ -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

Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 64a0f48

Please sign in to comment.