https://github.com/mit-plv/fiat-crypto
Tip revision: dd63ba33834de270f2f167ac4b91aeb34fce9a09 authored by Jason Gross on 09 October 2021, 02:20:20 UTC
Rearrange code a bit
Rearrange code a bit
Tip revision: dd63ba3
Crypto.Bedrock.Test_X25519_64.mulmod_bedrock.expected
= bedrock_func_body:((((("x0" =
(load( constr:(expr.var "y0") +
constr:(expr.literal 0))));
("x1" =
(load( constr:(expr.var "y0") +
constr:(expr.literal 8))));
("x2" =
(load( constr:(expr.var "y0") +
constr:(expr.literal 16))));
("x3" =
(load( constr:(expr.var "y0") +
constr:(expr.literal 24))));
("x4" =
(load( constr:(expr.var "y0") +
constr:(expr.literal 32))));
/*skip*/);
(("x5" =
(load( constr:(expr.var "y1") +
constr:(expr.literal 0))));
("x6" =
(load( constr:(expr.var "y1") +
constr:(expr.literal 8))));
("x7" =
(load( constr:(expr.var "y1") +
constr:(expr.literal 16))));
("x8" =
(load( constr:(expr.var "y1") +
constr:(expr.literal 24))));
("x9" =
(load( constr:(expr.var "y1") +
constr:(expr.literal 32))));
/*skip*/);
/*skip*/);
("x10" =
(constr:(expr.var "x4") *
(constr:(expr.var "x9") *
constr:(expr.literal 19))));
("x11" =
(constr:(expr.op bopname.mulhuu (expr.var "x4")
bedrock_expr:(constr:(expr.var "x9") *
constr:(expr.literal 19)))));
("x12" =
(constr:(expr.var "x4") *
(constr:(expr.var "x8") *
constr:(expr.literal 19))));
("x13" =
(constr:(expr.op bopname.mulhuu (expr.var "x4")
bedrock_expr:(constr:(expr.var "x8") *
constr:(expr.literal 19)))));
("x14" =
(constr:(expr.var "x4") *
(constr:(expr.var "x7") *
constr:(expr.literal 19))));
("x15" =
(constr:(expr.op bopname.mulhuu (expr.var "x4")
bedrock_expr:(constr:(expr.var "x7") *
constr:(expr.literal 19)))));
("x16" =
(constr:(expr.var "x4") *
(constr:(expr.var "x6") *
constr:(expr.literal 19))));
("x17" =
(constr:(expr.op bopname.mulhuu (expr.var "x4")
bedrock_expr:(constr:(expr.var "x6") *
constr:(expr.literal 19)))));
("x18" =
(constr:(expr.var "x3") *
(constr:(expr.var "x9") *
constr:(expr.literal 19))));
("x19" =
(constr:(expr.op bopname.mulhuu (expr.var "x3")
bedrock_expr:(constr:(expr.var "x9") *
constr:(expr.literal 19)))));
("x20" =
(constr:(expr.var "x3") *
(constr:(expr.var "x8") *
constr:(expr.literal 19))));
("x21" =
(constr:(expr.op bopname.mulhuu (expr.var "x3")
bedrock_expr:(constr:(expr.var "x8") *
constr:(expr.literal 19)))));
("x22" =
(constr:(expr.var "x3") *
(constr:(expr.var "x7") *
constr:(expr.literal 19))));
("x23" =
(constr:(expr.op bopname.mulhuu (expr.var "x3")
bedrock_expr:(constr:(expr.var "x7") *
constr:(expr.literal 19)))));
("x24" =
(constr:(expr.var "x2") *
(constr:(expr.var "x9") *
constr:(expr.literal 19))));
("x25" =
(constr:(expr.op bopname.mulhuu (expr.var "x2")
bedrock_expr:(constr:(expr.var "x9") *
constr:(expr.literal 19)))));
("x26" =
(constr:(expr.var "x2") *
(constr:(expr.var "x8") *
constr:(expr.literal 19))));
("x27" =
(constr:(expr.op bopname.mulhuu (expr.var "x2")
bedrock_expr:(constr:(expr.var "x8") *
constr:(expr.literal 19)))));
("x28" =
(constr:(expr.var "x1") *
(constr:(expr.var "x9") *
constr:(expr.literal 19))));
("x29" =
(constr:(expr.op bopname.mulhuu (expr.var "x1")
bedrock_expr:(constr:(expr.var "x9") *
constr:(expr.literal 19)))));
("x30" =
(constr:(expr.var "x4") * constr:(expr.var "x5")));
("x31" =
(constr:(expr.op bopname.mulhuu (expr.var "x4")
(expr.var "x5"))));
("x32" =
(constr:(expr.var "x3") * constr:(expr.var "x6")));
("x33" =
(constr:(expr.op bopname.mulhuu (expr.var "x3")
(expr.var "x6"))));
("x34" =
(constr:(expr.var "x3") * constr:(expr.var "x5")));
("x35" =
(constr:(expr.op bopname.mulhuu (expr.var "x3")
(expr.var "x5"))));
("x36" =
(constr:(expr.var "x2") * constr:(expr.var "x7")));
("x37" =
(constr:(expr.op bopname.mulhuu (expr.var "x2")
(expr.var "x7"))));
("x38" =
(constr:(expr.var "x2") * constr:(expr.var "x6")));
("x39" =
(constr:(expr.op bopname.mulhuu (expr.var "x2")
(expr.var "x6"))));
("x40" =
(constr:(expr.var "x2") * constr:(expr.var "x5")));
("x41" =
(constr:(expr.op bopname.mulhuu (expr.var "x2")
(expr.var "x5"))));
("x42" =
(constr:(expr.var "x1") * constr:(expr.var "x8")));
("x43" =
(constr:(expr.op bopname.mulhuu (expr.var "x1")
(expr.var "x8"))));
("x44" =
(constr:(expr.var "x1") * constr:(expr.var "x7")));
("x45" =
(constr:(expr.op bopname.mulhuu (expr.var "x1")
(expr.var "x7"))));
("x46" =
(constr:(expr.var "x1") * constr:(expr.var "x6")));
("x47" =
(constr:(expr.op bopname.mulhuu (expr.var "x1")
(expr.var "x6"))));
("x48" =
(constr:(expr.var "x1") * constr:(expr.var "x5")));
("x49" =
(constr:(expr.op bopname.mulhuu (expr.var "x1")
(expr.var "x5"))));
("x50" =
(constr:(expr.var "x0") * constr:(expr.var "x9")));
("x51" =
(constr:(expr.op bopname.mulhuu (expr.var "x0")
(expr.var "x9"))));
("x52" =
(constr:(expr.var "x0") * constr:(expr.var "x8")));
("x53" =
(constr:(expr.op bopname.mulhuu (expr.var "x0")
(expr.var "x8"))));
("x54" =
(constr:(expr.var "x0") * constr:(expr.var "x7")));
("x55" =
(constr:(expr.op bopname.mulhuu (expr.var "x0")
(expr.var "x7"))));
("x56" =
(constr:(expr.var "x0") * constr:(expr.var "x6")));
("x57" =
(constr:(expr.op bopname.mulhuu (expr.var "x0")
(expr.var "x6"))));
("x58" =
(constr:(expr.var "x0") * constr:(expr.var "x5")));
("x59" =
(constr:(expr.op bopname.mulhuu (expr.var "x0")
(expr.var "x5"))));
("x60" =
(constr:(expr.var "x22") +
constr:(expr.var "x16")));
("x61" =
(constr:(expr.var "x60") <
constr:(expr.var "x22")));
("x62" =
(constr:(expr.var "x61") +
constr:(expr.var "x23")));
("x63" =
(constr:(expr.var "x62") +
constr:(expr.var "x17")));
("x64" =
(constr:(expr.var "x26") +
constr:(expr.var "x60")));
("x65" =
(constr:(expr.var "x64") <
constr:(expr.var "x26")));
("x66" =
(constr:(expr.var "x65") +
constr:(expr.var "x27")));
("x67" =
(constr:(expr.var "x66") +
constr:(expr.var "x63")));
("x68" =
(constr:(expr.var "x28") +
constr:(expr.var "x64")));
("x69" =
(constr:(expr.var "x68") <
constr:(expr.var "x28")));
("x70" =
(constr:(expr.var "x69") +
constr:(expr.var "x29")));
("x71" =
(constr:(expr.var "x70") +
constr:(expr.var "x67")));
("x72" =
(constr:(expr.var "x58") +
constr:(expr.var "x68")));
("x73" =
(constr:(expr.var "x72") <
constr:(expr.var "x58")));
("x74" =
(constr:(expr.var "x73") +
constr:(expr.var "x59")));
("x75" =
(constr:(expr.var "x74") +
constr:(expr.var "x71")));
("x76" =
(constr:(expr.var "x72") >>
constr:(expr.literal 51)
| constr:(expr.var "x75") <<
constr:(expr.literal 13)));
("x77" =
(constr:(expr.var "x72") &
constr:(expr.literal 2251799813685247)));
("x78" =
(constr:(expr.var "x32") +
constr:(expr.var "x30")));
("x79" =
(constr:(expr.var "x78") <
constr:(expr.var "x32")));
("x80" =
(constr:(expr.var "x79") +
constr:(expr.var "x33")));
("x81" =
(constr:(expr.var "x80") +
constr:(expr.var "x31")));
("x82" =
(constr:(expr.var "x36") +
constr:(expr.var "x78")));
("x83" =
(constr:(expr.var "x82") <
constr:(expr.var "x36")));
("x84" =
(constr:(expr.var "x83") +
constr:(expr.var "x37")));
("x85" =
(constr:(expr.var "x84") +
constr:(expr.var "x81")));
("x86" =
(constr:(expr.var "x42") +
constr:(expr.var "x82")));
("x87" =
(constr:(expr.var "x86") <
constr:(expr.var "x42")));
("x88" =
(constr:(expr.var "x87") +
constr:(expr.var "x43")));
("x89" =
(constr:(expr.var "x88") +
constr:(expr.var "x85")));
("x90" =
(constr:(expr.var "x50") +
constr:(expr.var "x86")));
("x91" =
(constr:(expr.var "x90") <
constr:(expr.var "x50")));
("x92" =
(constr:(expr.var "x91") +
constr:(expr.var "x51")));
("x93" =
(constr:(expr.var "x92") +
constr:(expr.var "x89")));
("x94" =
(constr:(expr.var "x34") +
constr:(expr.var "x10")));
("x95" =
(constr:(expr.var "x94") <
constr:(expr.var "x34")));
("x96" =
(constr:(expr.var "x95") +
constr:(expr.var "x35")));
("x97" =
(constr:(expr.var "x96") +
constr:(expr.var "x11")));
("x98" =
(constr:(expr.var "x38") +
constr:(expr.var "x94")));
("x99" =
(constr:(expr.var "x98") <
constr:(expr.var "x38")));
("x100" =
(constr:(expr.var "x99") +
constr:(expr.var "x39")));
("x101" =
(constr:(expr.var "x100") +
constr:(expr.var "x97")));
("x102" =
(constr:(expr.var "x44") +
constr:(expr.var "x98")));
("x103" =
(constr:(expr.var "x102") <
constr:(expr.var "x44")));
("x104" =
(constr:(expr.var "x103") +
constr:(expr.var "x45")));
("x105" =
(constr:(expr.var "x104") +
constr:(expr.var "x101")));
("x106" =
(constr:(expr.var "x52") +
constr:(expr.var "x102")));
("x107" =
(constr:(expr.var "x106") <
constr:(expr.var "x52")));
("x108" =
(constr:(expr.var "x107") +
constr:(expr.var "x53")));
("x109" =
(constr:(expr.var "x108") +
constr:(expr.var "x105")));
("x110" =
(constr:(expr.var "x18") +
constr:(expr.var "x12")));
("x111" =
(constr:(expr.var "x110") <
constr:(expr.var "x18")));
("x112" =
(constr:(expr.var "x111") +
constr:(expr.var "x19")));
("x113" =
(constr:(expr.var "x112") +
constr:(expr.var "x13")));
("x114" =
(constr:(expr.var "x40") +
constr:(expr.var "x110")));
("x115" =
(constr:(expr.var "x114") <
constr:(expr.var "x40")));
("x116" =
(constr:(expr.var "x115") +
constr:(expr.var "x41")));
("x117" =
(constr:(expr.var "x116") +
constr:(expr.var "x113")));
("x118" =
(constr:(expr.var "x46") +
constr:(expr.var "x114")));
("x119" =
(constr:(expr.var "x118") <
constr:(expr.var "x46")));
("x120" =
(constr:(expr.var "x119") +
constr:(expr.var "x47")));
("x121" =
(constr:(expr.var "x120") +
constr:(expr.var "x117")));
("x122" =
(constr:(expr.var "x54") +
constr:(expr.var "x118")));
("x123" =
(constr:(expr.var "x122") <
constr:(expr.var "x54")));
("x124" =
(constr:(expr.var "x123") +
constr:(expr.var "x55")));
("x125" =
(constr:(expr.var "x124") +
constr:(expr.var "x121")));
("x126" =
(constr:(expr.var "x20") +
constr:(expr.var "x14")));
("x127" =
(constr:(expr.var "x126") <
constr:(expr.var "x20")));
("x128" =
(constr:(expr.var "x127") +
constr:(expr.var "x21")));
("x129" =
(constr:(expr.var "x128") +
constr:(expr.var "x15")));
("x130" =
(constr:(expr.var "x24") +
constr:(expr.var "x126")));
("x131" =
(constr:(expr.var "x130") <
constr:(expr.var "x24")));
("x132" =
(constr:(expr.var "x131") +
constr:(expr.var "x25")));
("x133" =
(constr:(expr.var "x132") +
constr:(expr.var "x129")));
("x134" =
(constr:(expr.var "x48") +
constr:(expr.var "x130")));
("x135" =
(constr:(expr.var "x134") <
constr:(expr.var "x48")));
("x136" =
(constr:(expr.var "x135") +
constr:(expr.var "x49")));
("x137" =
(constr:(expr.var "x136") +
constr:(expr.var "x133")));
("x138" =
(constr:(expr.var "x56") +
constr:(expr.var "x134")));
("x139" =
(constr:(expr.var "x138") <
constr:(expr.var "x56")));
("x140" =
(constr:(expr.var "x139") +
constr:(expr.var "x57")));
("x141" =
(constr:(expr.var "x140") +
constr:(expr.var "x137")));
("x142" =
(constr:(expr.var "x76") +
constr:(expr.var "x138")));
("x143" =
(constr:(expr.var "x142") <
constr:(expr.var "x76")));
("x144" =
(constr:(expr.var "x143") +
constr:(expr.var "x141")));
("x145" =
(constr:(expr.var "x142") >>
constr:(expr.literal 51)
| constr:(expr.var "x144") <<
constr:(expr.literal 13)));
("x146" =
(constr:(expr.var "x142") &
constr:(expr.literal 2251799813685247)));
("x147" =
(constr:(expr.var "x145") +
constr:(expr.var "x122")));
("x148" =
(constr:(expr.var "x147") <
constr:(expr.var "x145")));
("x149" =
(constr:(expr.var "x148") +
constr:(expr.var "x125")));
("x150" =
(constr:(expr.var "x147") >>
constr:(expr.literal 51)
| constr:(expr.var "x149") <<
constr:(expr.literal 13)));
("x151" =
(constr:(expr.var "x147") &
constr:(expr.literal 2251799813685247)));
("x152" =
(constr:(expr.var "x150") +
constr:(expr.var "x106")));
("x153" =
(constr:(expr.var "x152") <
constr:(expr.var "x150")));
("x154" =
(constr:(expr.var "x153") +
constr:(expr.var "x109")));
("x155" =
(constr:(expr.var "x152") >>
constr:(expr.literal 51)
| constr:(expr.var "x154") <<
constr:(expr.literal 13)));
("x156" =
(constr:(expr.var "x152") &
constr:(expr.literal 2251799813685247)));
("x157" =
(constr:(expr.var "x155") +
constr:(expr.var "x90")));
("x158" =
(constr:(expr.var "x157") <
constr:(expr.var "x155")));
("x159" =
(constr:(expr.var "x158") +
constr:(expr.var "x93")));
("x160" =
(constr:(expr.var "x157") >>
constr:(expr.literal 51)
| constr:(expr.var "x159") <<
constr:(expr.literal 13)));
("x161" =
(constr:(expr.var "x157") &
constr:(expr.literal 2251799813685247)));
("x162" =
(constr:(expr.var "x160") *
constr:(expr.literal 19)));
("x163" =
(constr:(expr.var "x77") +
constr:(expr.var "x162")));
("x164" =
(constr:(expr.var "x163") >>
constr:(expr.literal 51)));
("x165" =
(constr:(expr.var "x163") &
constr:(expr.literal 2251799813685247)));
("x166" =
(constr:(expr.var "x164") +
constr:(expr.var "x146")));
("x167" =
(constr:(expr.var "x166") >>
constr:(expr.literal 51)));
("x168" =
(constr:(expr.var "x166") &
constr:(expr.literal 2251799813685247)));
("x169" =
(constr:(expr.var "x167") +
constr:(expr.var "x151")));
("x170" = (constr:(expr.var "x165")));
("x171" = (constr:(expr.var "x168")));
("x172" = (constr:(expr.var "x169")));
("x173" = (constr:(expr.var "x156")));
("x174" = (constr:(expr.var "x161")));
/*skip*/);
(store( constr:(expr.var "ret") +
constr:(expr.literal 0),
constr:(expr.var "x170")));
(store( constr:(expr.var "ret") +
constr:(expr.literal 8),
constr:(expr.var "x171")));
(store( constr:(expr.var "ret") +
constr:(expr.literal 16),
constr:(expr.var "x172")));
(store( constr:(expr.var "ret") +
constr:(expr.literal 24),
constr:(expr.var "x173")));
(store( constr:(expr.var "ret") +
constr:(expr.literal 32),
constr:(expr.var "x174")));
/*skip*/)
: cmd
