Skip to content

Latest commit

 

History

History
6 lines (6 loc) · 530 Bytes

TODO.md

File metadata and controls

6 lines (6 loc) · 530 Bytes
Raw
  • Prove formally that [Alice received (openChannel, Alice, Bob, init, tid) from E && Alice sent (news, {..}.has(tid), _, _) to E && for all i in |out|, [Alice received (pay, Bob, out_i, _, _) to E && Alice sent (news, _, _, {..}.has(receipt of out_i)) to E] && for all i in |in|, [Alice received (TODO) from TODO && Alice sent (news, _, _, {..}.has(receipt of in_i)) to E]] -> [blockchain will eventually have a tx from which Alice will be able to unilaterally spend at least init - sum(out_i) + sum(in_i)]