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