(in a0 a1 a2 a3 a4 a5 a6 a7 b0 b1 b2 b3 b4 b5 b6 b7)
(out res ca0 ca1 ca2 ca3 ca4 ca5 ca6 ca7 cb0 cb1 cb2 cb3 cb4 cb5 cb6 cb7)
(verify res b0 b1 b2 b3 b4 b5 b6 b7)

(program
    (= ca0 (* a0 (+ a0 250)))
    (= ca1 (* a1 (+ a1 250)))
    (= ca2 (* a2 (+ a2 250)))
    (= ca3 (* a3 (+ a3 250)))
    (= ca4 (* a4 (+ a4 250)))
    (= ca5 (* a5 (+ a5 250)))
    (= ca6 (* a6 (+ a6 250)))
    (= ca7 (* a7 (+ a7 250)))
    (= cb0 (* b0 (+ b0 250)))
    (= cb1 (* b1 (+ b1 250)))
    (= cb2 (* b2 (+ b2 250)))
    (= cb3 (* b3 (+ b3 250)))
    (= cb4 (* b4 (+ b4 250)))
    (= cb5 (* b5 (+ b5 250)))
    (= cb6 (* b6 (+ b6 250)))
    (= cb7 (* b7 (+ b7 250)))
    
    (= diff0 (* (+ a0 (* 250 b0)) (+ a0 (* 250 b0))))
    (= diff1 (* (+ a1 (* 250 b1)) (+ a1 (* 250 b1))))
    (= diff2 (* (+ a2 (* 250 b2)) (+ a2 (* 250 b2))))
    (= diff3 (* (+ a3 (* 250 b3)) (+ a3 (* 250 b3))))
    (= diff4 (* (+ a4 (* 250 b4)) (+ a4 (* 250 b4))))
    (= diff5 (* (+ a5 (* 250 b5)) (+ a5 (* 250 b5))))
    (= diff6 (* (+ a6 (* 250 b6)) (+ a6 (* 250 b6))))
    (= diff7 (* (+ a7 (* 250 b7)) (+ a7 (* 250 b7))))
    
    (= acc7 (* 1 diff7))
    (= acc_i6 (* acc7 diff6))
    (= acc6 (* 1 (+ acc7 diff6 (* 250 acc_i6))))
    (= acc_i5 (* acc6 diff5))
    (= acc5 (* 1 (+ acc6 diff5 (* 250 acc_i5))))
    (= acc_i4 (* acc5 diff4))
    (= acc4 (* 1 (+ acc5 diff4 (* 250 acc_i4))))
    (= acc_i3 (* acc4 diff3))
    (= acc3 (* 1 (+ acc4 diff3 (* 250 acc_i3))))
    (= acc_i2 (* acc3 diff2))
    (= acc2 (* 1 (+ acc3 diff2 (* 250 acc_i2))))
    (= acc_i1 (* acc2 diff1))
    (= acc1 (* 1 (+ acc2 diff1 (* 250 acc_i1))))
    (= acc_i0 (* acc1 diff0))
    (= acc0 (* 1 (+ acc1 diff0 (* 250 acc_i0))))

    (= fdiff7 (* 1 acc7))
    (= fdiff6 (* (+ acc7 (* 250 acc6)) (+ acc7 (* 250 acc6))))
    (= fdiff5 (* (+ acc6 (* 250 acc5)) (+ acc6 (* 250 acc5))))
    (= fdiff4 (* (+ acc5 (* 250 acc4)) (+ acc5 (* 250 acc4))))
    (= fdiff3 (* (+ acc4 (* 250 acc3)) (+ acc4 (* 250 acc3))))
    (= fdiff2 (* (+ acc3 (* 250 acc2)) (+ acc3 (* 250 acc2))))
    (= fdiff1 (* (+ acc2 (* 250 acc1)) (+ acc2 (* 250 acc1))))
    (= fdiff0 (* (+ acc1 (* 250 acc0)) (+ acc1 (* 250 acc0))))

    (= chka0 (* a0 fdiff0))
    (= chka1 (* a1 fdiff1))
    (= chka2 (* a2 fdiff2))
    (= chka3 (* a3 fdiff3))
    (= chka4 (* a4 fdiff4))
    (= chka5 (* a5 fdiff5))
    (= chka6 (* a6 fdiff6))
    (= chka7 (* a7 fdiff7))

    (= res7 (* 1 chka7))
    (= res_i6 (* res7 chka6))
    (= res6 (* 1 (+ res7 chka6 (* 250 res_i6))))
    (= res_i5 (* res6 chka5))
    (= res5 (* 1 (+ res6 chka5 (* 250 res_i5))))
    (= res_i4 (* res5 chka4))
    (= res4 (* 1 (+ res5 chka4 (* 250 res_i4))))
    (= res_i3 (* res4 chka3))
    (= res3 (* 1 (+ res4 chka3 (* 250 res_i3))))
    (= res_i2 (* res3 chka2))
    (= res2 (* 1 (+ res3 chka2 (* 250 res_i2))))
    (= res_i1 (* res2 chka1))
    (= res1 (* 1 (+ res2 chka1 (* 250 res_i1))))
    (= res_i (* res1 chka0))
    (= res (* 1 (+ res1 chka0 (* 250 res_i)))))