The princeton suite is roughtly 10kTd (kiloTwelf declarations) in size. I run my code on it, it chokes at declaration 2447. So I have 2kTd to think about. I finally get my stupid code working that is supposed to filter out just those declarations that a given one depends on, and reduce this to 100Td that are sufficient to evince the same bug. By manually inlining some definitions and performing some habitual reductions, I get this down to around 80Td before I find a single definition which, if inlined, makes the bug not tripped. An educated guess leads me to a file only 5Td long:
%use word32.
zero : word32 = 0.
a : word32 -> type.
c : {x:word32} a x.
test : a zero = c 0.Now to figure out why this breaks. A typical line from the 80Td thing that I was afraid I'd have to painfully whittle down by hand is this beast:
pow2_32_eq_65536*65536 = cut_1313 (eq_1244 k (arr (*_1762 (const_83 0) (const_83 bignum_base_169)) (const_83 1)) (const_83 1)) (eq_1244 k (dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (arr (const_83 65536) (c_2394 65536))) (congr_1315 k (*_1762 (const_83 0) (const_83 bignum_base_169)) (const_83 0) ([z1:o] eq_1244 k (arr z1 (const_83 1)) (const_83 1)) (zero_times_1808 (const_83 bignum_base_169)) (zero_plus_1770 (const_83 1))) ([p1:pf_5 (eq_1244 k (dig_171 bignum_170 1) (const_83 1))] cut_1313 (==_1246 k (dig_171 (dig_171 bignum_170 1) 0) (c_2394 bignum_base_169)) (eq_1244 k (dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (arr (const_83 65536) (c_2394 65536))) (trans_1321 k (dig_171 (dig_171 bignum_170 1) 0) (*_1762 (const_83 1) (c_2394 bignum_base_169)) (c_2394 bignum_base_169) (dig0lem1_2446 (dig_171 bignum_170 1) (const_83 1) p1) (one_times_1778 (c_2394 bignum_base_169))) ([p2:pf_5 (eq_1244 k (dig_171 (dig_171 bignum_170 1) 0) (const_83 bignum_base_169))] cut_1313 (==_1246 k (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) (c_2394 65536)) (eq_1244 k (dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (arr (const_83 65536) (c_2394 65536))) (trans_1321 k (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) (*_1762 (const_83 bignum_base_169) (c_2394 bignum_base_169)) (c_2394 65536) (dig0lem1_2446 (dig_171 (dig_171 bignum_170 1) 0) (const_83 bignum_base_169) p2) (eval_times_2438 256 256 65536 256*256_2427)) ([p3:pf_5 (eq_1244 k (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) (const_83 65536))] cut_1313 (==_1246 k (dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (*_1762 (const_83 65536) (*_1762 (c_2394 bignum_base_169) (c_2394 bignum_base_169)))) (eq_1244 k (dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (arr (const_83 65536) (c_2394 65536))) (trans_1321 k (dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (*_1762 (*_1762 (const_83 65536) (c_2394 bignum_base_169)) (c_2394 bignum_base_169)) (*_1762 (const_83 65536) (*_1762 (c_2394 bignum_base_169) (c_2394 bignum_base_169))) (dig0lem1_2446 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) (*_1762 (const_83 65536) (c_2394 bignum_base_169)) (dig0lem1_2446 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) (const_83 65536) p3)) (times_assoc_1775 (const_83 65536) (c_2394 bignum_base_169) (c_2394 bignum_base_169))) ([p4:pf_5 (eq_1244 k (dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (arr (const_83 65536) (arr (const_83 bignum_base_169) (const_83 bignum_base_169))))] congr_1315 k (c_2394 65536) (*_1762 (c_2394 256) (c_2394 256)) ([z2:o] eq_1244 k (dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (arr (const_83 65536) z2)) (symm_1320 k (*_1762 (c_2394 256) (c_2394 256)) (c_2394 65536) (eval_times_2438 256 256 65536 256*256_2427)) p4)))).
