# `is_supporting_vote` proofs

*Writing down some proofs to prove that `is_supporting_vote` with message's vote is reflected correctly on the block node.*

to prove this, we take two consecutive blocks
- `blk{slot: 100, block_root: 0xa}`
- `blk{slot: 101, block_root: 0xb, parent_root: 0xa}`

then we look at the following attestations and apply them to the blocks
- `msg{slot: 100, block_root: 0xa}`
- `msg{slot: 100, block_root: 0xb}` (This is an invalid attestation that can be ignored)
- `msg{slot: 101, block_root: 0xa}`
- `msg{slot: 101, block_root: 0xb}`
- `msg{slot: 102, block_root: 0xa}`
- `msg{slot: 102, block_root: 0xb}`


1. Apply `msg{slot: 102, block_root: 0xb}` to `blk{slot: 101, block_root: 0xb, parent_root: 0xa}`
* Return `true` because `msg.root==blk.root && msg.slot >= blk.slot`

2. Apply `msg{slot: 102, block_root: 0xb}` to `blk{slot: 100, block_root: 0xa}`
* Return `true` because
* `msg.root!=blk.root`
* `msg_blk.slot>blk.slot`
* `ancestor_match`

3. Apply `msg{slot: 102, block_root: 0xa}` to `blk{slot: 101, block_root: 0xb, parent_root: 0xa}`
* Return `false` because
* `msg.root!=blk.root`
* `blk.slot>msg_blk.slot`

4. Apply `msg{slot: 102, block_root: 0xa}` to `blk{slot: 100, block_root: 0xa}`
* Return `true` because `msg.root==blk.root && msg.slot >= blk.slot`

5. Apply `msg{slot: 101, block_root: 0xb}` to `blk{slot: 101, block_root: 0xb, parent_root: 0xa}`
- Return `true` `msg.root==blk.root && msg.slot >= blk.slot`

6. Apply `msg{slot: 101, block_root: 0xb}` to `blk{slot: 100, block_root: 0xa}`
* Return `true` because
* `msg.root!=blk.root`
* `msg_blk.slot>blk.slot`
* `ancestor_match`

7. Apply `msg{slot: 101, block_root: 0xa}` to `blk{slot: 101, block_root: 0xb, parent_root: 0xa}`
* Return `false` because
* `msg.root!=blk.root`
* `blk.slot>msg_blk.slot`

8. Apply `msg{slot: 101, block_root: 0xa}` to `blk{slot: 100, block_root: 0xa}`
* Return `true` because `msg.root==blk.root && msg.slot >= blk.slot`

9. Apply `msg{slot: 100, block_root: 0xa}` to `blk{slot: 101, block_root: 0xb, parent_root: 0xa}`
* Return `false` because
* `msg.root!=blk.root`
* `blk.slot>msg_blk.slot`

10. Apply `msg{slot: 100, block_root: 0xa}` to `blk{slot: 100, block_root: 0xa}`
* Return `true` because `msg.root==blk.root && msg.slot >= blk.slot`