gistfile1.txt

import stp

width = 64
s = stp.Solver()
MAX = 2 ** width - 1
UINT256MAX = s.bitvecval(width, MAX)

t1 = s.bitvec('t1', width)
t2 = s.bitvec('t2', width)

d1 = s.bitvec('d1', width)
d2 = s.bitvec('d2', width)
dc = s.bitvec('dc', width)
da = s.bitvec('da', width)

w1 = s.bitvec('w1', width)
w2 = s.bitvec('w2', width)

l1 = s.bitvec('l1', width)
l2 = s.bitvec('l2', width)

a1 = s.bitvec('a1', width)
a2 = s.bitvec('a2', width)

invalid_t1 = s.bitvec('invalid_t1', width)
invalid_l1 = s.bitvec('invalid_l1', width)

s.add(dc == d1 + d2 - w1 - w2)
s.add(d1 >= t1 + l1 - t2)
s.add(d1 + d2 >= w1 + w2)
s.add(d1 + d2 <= UINT256MAX)

# constraints for a honest node1
# dont send an invalid BP
s.add(t1 + l1 >= t1)      # overflow check
s.add(t2 - t1 + l1 >= 0)  # out-of-balance
s.add(t2 - t1 + l1 <= d1) # out-of-balance
# dont accept invalid BPs
s.add(t2 - t1 - l2 >= 0)  # out-of-balance
s.add(t2 - t1 - l2 <= d2) # out-of-balance

# on-chain computation with a dishonest node2
s.add(invalid_t1 <= t1)
s.add(invalid_l1 <= l1)

s.add(da == dc - invalid_l1 - l2)
s.add(a1 == d1 + t2 - invalid_t1 - w1)
s.add(a2 == da - a1)

# if this happens the system is broken
s.add(a1 + a2 + l1 + l2 != dc)
if s.check():
    m = s.model()

    print('MAX = {}'.format(MAX))
    print('d1, d2 ({}, {})'.format(m['d1'], m['d2']))
    print('w1, w2 ({}, {})'.format(m['w1'], m['w2']))
    print('dc ({})'.format(m['dc']))
    print('t1, l1 ({}, {})'.format(m['t1'], m['l1']))
    print('t2, l2 ({}, {})'.format(m['t2'], m['l2']))
    print('a1, a2, l1, l2 ({}, {}, {}, {})'.format(m['a1'], m['a2'], m['l1'], m['l2']))