|
|
|---|
|
|
|
|---|
The longer and shorter blockchains calculate the same bonded committees, when they both do.
This proves most of what we need for our overall proof. The interesting case of the overall proof is when the two blockchains are not equal, but one is longer and the other is shorter. We express this relation using nthcdr here, as in lists-noforkp. We make use of (two instances of) the theorem to expand the committee calculation to include a call of trim-blocks-for-round, and the two theorems that simplify them (for longer and shorter blockchain). We also need, as a local lemma, the fact that the round of the oldest block of the extension is greater than the round of the newest block of the shorter blockchain, but expressed in terms of nth of the longer blockchain. We also need the fact that the rounds are not only ordered, but even: this ensures that there is a gap of at least 2 between two block rounds where one is greater.
This proof, and its hints, is a bit more complex than ideal. Perhaps it can be simplified and streamlined a bit.
Theorem:
(defthm same-bonded-committees-longer-shorter (implies (and (blocks-orderedp blocks2) (< (len blocks1) (len blocks2)) (equal blocks1 (nthcdr (- (len blocks2) (len blocks1)) blocks2)) (bonded-committee-at-round round blocks1) (bonded-committee-at-round round blocks2)) (equal (bonded-committee-at-round round blocks1) (bonded-committee-at-round round blocks2))))