Skip to content

Commit

Permalink
EVE epochs fixed, I believe
Browse files Browse the repository at this point in the history
  • Loading branch information
@josef-widder
josef-widder committed Apr 18, 2024
1 parent 0bacc36 commit 1ff3df2
Show file tree
Hide file tree
Showing 2 changed files with 45 additions and 47 deletions.
76 changes: 33 additions & 43 deletions specs/quint/specs/reset.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,10 @@ type ForkID = int
// val minReg = -3
// val ValAddresses = Set("Huey", "Dewey", "Louie")


const L2EpochSize : Height
const L1EpochSize : Time
const EthStartTime : Time
const maxReg : int
const minReg : int
const ValAddresses : Set[Address]
Expand Down Expand Up @@ -95,24 +97,14 @@ pure def L1Epoch(b: L1Block) : int =
pure def staleRegs (b: L1Block) : Set[Registration] =
b.pendingRegistrations.filter(r => r.eth_epoch + 2 <= L1Epoch(b))


pure def existsStale (b: L1Block) : bool =
staleRegs(b).size() > 0

pure def forkID (regs: Set[Registration]) : int =
// TODO0404: it will set the fork ID equal to the EVE of the most recent stale registration
1

// // TODO0404: gets much simpler
// pure def provenHeight(verifProofs: Set[L2BlockProof]) : Height =
// // smallest unproven block - 1
// // Remark: This models somewhat that L1 is initialized with a proof of the L2 genesis state
// val HeightsWithProofs = Set(0).union(verifProofs.fold(Set(), (s, pp) => s.union(Set(pp.height))))
// // complete contains a proofs i such that we also have all proofs from 0 to i
// // that is if we have {0,1,2,4,5,8}, complete is {0,1,2}; TODO test
// val complete = HeightsWithProofs.filter(i => 0.to(i).subseteq(HeightsWithProofs))
// // take biggest, that is 2 in the example above
// complete.fold(0, (max, i) => if (i > max) i else max)
// set the fork ID equal to the EVE of the most recent stale registration
pure def expectedForkID (b: L1Block) : int =
if (not(existsStale(b))) b.l2forkID
else
staleRegs(b).fold(b.l2forkID, (s, x) => if (x.eth_epoch > s) x.eth_epoch else s)

// confirmed registrations in proofs up to the proven height
pure def confirmedRegistrations (vp: L2Proof) : Set[Registration] =
Expand All @@ -128,10 +120,7 @@ pure def confirmedRegistrations (vp: L2Proof) : Set[Registration] =
pure def proofOK (prev: L1Block, p: L2BlockProof) : bool =
if (prev.provenHeight + 1 != p.from_height) false
else
if (existsStale(prev))
p.forkID == prev.L1Epoch() // TODO: epoch of the latest stale
else
p.forkID <= prev.l2forkID // TODO: not very precise
p.forkID == prev.expectedForkID()

pure def newL1Block (prev: L1Block, regs: Set[Registration], proof: L2Proof) : L1Block =
val accepted = match proof {
Expand All @@ -147,11 +136,6 @@ pure def newL1Block (prev: L1Block, regs: Set[Registration], proof: L2Proof) : L
| Invalid => prev.provenHeight
| Proof(p) => p.to_height
}
val newForkID = match accepted {
| None => prev.l2forkID
| Invalid => prev.provenHeight
| Proof(p) => p.forkID
}
val newBlockHash = match accepted {
| None => prev.latestProvenL2BlockHash
| Invalid => prev.latestProvenL2BlockHash
Expand All @@ -162,7 +146,7 @@ pure def newL1Block (prev: L1Block, regs: Set[Registration], proof: L2Proof) : L
newProof: proof,
provenHeight: newProvenHeight,
latestProvenL2BlockHash: newBlockHash,
l2forkID: newForkID,
l2forkID: prev.expectedForkID(), // off by one perhaps.
pendingRegistrations: prev.pendingRegistrations.union(regs).exclude(confirmed),
cntRegistrations: prev.cntRegistrations + regs.size()
}
Expand Down Expand Up @@ -211,7 +195,7 @@ pure def forkBlock (prev: L2Block, lastL1: L1Block) : L2Block =
// Is L1->L2 messaging guaranteed to be ordered? not in the L1->L2 protocol, but the L2 smart contract
// ensures ordering
{ height: lastL1.provenHeight + 1,
forkID: lastL1.L1Epoch(), // TODO: check Matan's document. Epoch of the heighest stale update?
forkID: lastL1.expectedForkID(), // TODO: check Matan's document. Epoch of the heighest stale update?

Check failure on line 198 in specs/quint/specs/reset.qnt

View workflow job for this annotation

GitHub Actions / Check spelling 

heighest ==> highest
registrations: regs,
valset: newValSet,
stagedUpdates: Set(),
Expand All @@ -220,6 +204,23 @@ pure def forkBlock (prev: L2Block, lastL1: L1Block) : L2Block =
}


//
// Functions for Provers
//

pure def makeProof (l2: List[L2Block], to_height: Height, l1: List[L1Block]) : L2Proof =
val from_height = l1[l1.length()-1].provenHeight + 1
if (from_height <= to_height and to_height < l2.length())
val listToProve = l2.slice(from_height, to_height + 1)
val regs = listToProve.foldl (Set(), (s, x) => s.union(x.registrations))
val newforkID = listToProve[listToProve.length()-1].forkID
Proof({ from_height: from_height,
to_height: to_height,
confirmedRegs: regs,
forkID: newforkID,
resultingBlock: l2[to_height]})
else
Invalid


// STATE MACHINE
Expand Down Expand Up @@ -264,24 +265,25 @@ action init =
receivedRegistrations: Set(),
}
all {
L1' = List({time : 0,
L1' = List({time : EthStartTime,
newRegistrations: Set(),
newProof: None,
pendingRegistrations: Set(),
provenHeight: -1,
provenHeight: 0, // initial state proven?
l2forkID: 0,
latestProvenL2BlockHash: initialL2Block,
cntRegistrations: 0,
}),
L2' = List(initialL2Block),
envRegs' = Set(),
}
}


action addRegistration = all {
nondet newVal = ValAddresses.oneOf()
nondet power = minReg.to(maxReg).oneOf()
val newReg = {
eth_epoch: L1.length() / L1EpochSize, //TODO: check and fix
eth_epoch: L1[L1.length()-1].L1Epoch(), //TODO: check and fix
seq_num: L1[L1.length() - 1].cntRegistrations + envRegs.size() + 1, // encodes unique registration index
starknet_addr: newVal,
amount: power
Expand All @@ -291,19 +293,7 @@ action addRegistration = all {
L2' = L2,
}

pure def makeProof (l2: List[L2Block], to_height: Height, l1: List[L1Block]) : L2Proof =
val from_height = l1[l1.length()-1].provenHeight // + 1
val listToProve = l2.slice(from_height, to_height)
val regs = listToProve.foldl (Set(), (s, x) => s.union(x.registrations))
val forkID = listToProve[listToProve.length()-1].forkID
if (from_height < to_height and to_height <= l2.length())
Proof({ from_height: from_height,
to_height: to_height,
confirmedRegs: regs,
forkID: forkID,
resultingBlock: l2[to_height]})
else
Invalid




Expand Down
16 changes: 12 additions & 4 deletions specs/quint/specs/resetTest.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@ module resetTest {

import reset (
L2EpochSize = 5,
L1EpochSize = 5,
L1EpochSize = 4,
EthStartTime = 42,
maxReg = 3,
minReg = -3,
ValAddresses = Set("Huey", "Dewey", "Louie")
Expand All @@ -15,16 +16,23 @@ run FailedResetTest =
init
.then(addRegistration)
.then(addL1BlockNoProof)
.then((2 * L1EpochSize).reps(_ => addL1BlockNoProof))
.then((3 * L1EpochSize).reps(_ => addL1BlockNoProof))
.then(reset)
.expect(L2[L2.length()-1].chainID == 2 and L2.length() == 2) // first reset happened
.expect(L2[L2.length()-1].forkID == L1[L1.length()-1].l2forkID and L2.length() == 2) // first reset happened
.then((L1EpochSize).reps(_ => addL1BlockNoProof))
.then(reset)
.expect(L2[L2.length()-1].chainID == 3 and L2.length() == 2) // second reset happened
.expect(L2[L2.length()-1].forkID == L1[L1.length()-1].l2forkID and L2.length() == 2) // second reset happened
.then(addL1BlockProofWithHeight(1)) // now proof gets into L1
.expect(not(existsStale(L1[L1.length()-1]))) // no more stale registrations


run ResetwithProofonL1Test =
init
.then(addRegistration)
.then((3*L1EpochSize).reps(_=>addL1BlockNoProof))
.then(reset)
.then(addL1BlockProofWithHeight(1))
.expect(L2[L2.length()-1] == L1[L1.length()-1].latestProvenL2BlockHash)

run simpleTest =
init
Expand Down

0 comments on commit 1ff3df2

Please sign in to comment.