Code

Rvdevelop#6

Code

Open

F-WRunTime wants to merge 43 commits intodevelopruntimeverification/_audits_lidofinance_dual-governance_fork:developfrom rvdevelopruntimeverification/_audits_lidofinance_dual-governance_fork:rvdevelopCopy head branch name to clipboard

+1,433-210

Commits

Commits on Jul 5, 2024

• Committing KaaS Compute Setup for RV Testing / Development

  

  F-WRunTime

  authored and

  lucasmt

  committed
  c8b4b4d

• Test using variables to get org name / repo name

  

  F-WRunTime

  authored and

  lucasmt

  committed
  c2db612

• Merge conflict resolution

  

  F-WRunTime

  authored and

  lucasmt

  committed
  bb73582

• Revert changes to lido-ci.yml for merge into parent repo

  lucasmt

  committed
  ef5a282

• Committing KaaS Compute Setup for RV Testing / Development

  

  F-WRunTime

  authored and

  lucasmt

  committed
  740b5c5

• Test using variables to get org name / repo name

  

  F-WRunTime

  authored and

  lucasmt

  committed
  3e2804d

• Merge conflict resolution

  

  F-WRunTime

  authored and

  lucasmt

  committed
  979bd73

• Adding workflow_dispatch event triggers

  

  F-WRunTime

  authored and

  lucasmt

  committed
  bef8491

• Add StETH token model

  lucasmt

  committed
  49c836f

• Add new version of Escrow model using rebasable StETH token

  lucasmt

  committed
  29d4c76

• Rename original Escrow model to EscrowNonRebasable.sol

  lucasmt

  committed
  dd713cf

• Make the Escrow version using StETH the default Escrow contract in the model

  lucasmt

  committed
  e145cbc

• Adapt VetoSignalling tests to StETH

  lucasmt

  committed
  ee7d042

• Split off test set-up and helper functions into separate base contract

  lucasmt

  committed
  51c4470

• Reduce SMT timeout in run-kontrol.sh script

  lucasmt

  committed
  ac347ff

• Add test to run-kontrol.sh script

  lucasmt

  committed
  b074a16

• Update versions.json to the latest kontrol version

  lucasmt

  committed
  1cc7737

• Adjust StETH model to be closer to original StETH contract

  lucasmt

  committed
  4eff4c7

• renaming contracts for easier use with Kontrol

  

  PetarMax

  authored and

  lucasmt

  committed
  748790e

• additional lemma for cleaning up specification of getRageQuitSupport

  

  PetarMax

  authored and

  lucasmt

  committed
  19fb17a

• assumptions

  

  PetarMax

  authored and

  lucasmt

  committed
  e26f832

• Refactor DualGovernanceSetUp into 3 contracts for more fine-grained functionality reuse.

  Show description for 5f84969
  lucasmt

  committed
  5f84969

• Make Escrow storage setup compatible with the new storage layout of the model

  lucasmt

  committed
  a8b7377

• Fix assumptions on StETHModel to avoid division by 0 problem

  lucasmt

  committed
  f26be16

• Rename variable in comment of DualGovernanceSetUp

  lucasmt

  committed
  ac4dde4

• Add --verbose and --max-frontier-parallel options to run-kontrol.sh script

  lucasmt

  committed
  538c657

• further limiting branching

  

  PetarMax

  authored and

  lucasmt

  committed
  28ee0ed

• additional constraints to minimise calls to calculateDynamicTimelock

  

  PetarMax

  authored and

  lucasmt

  committed
  7ab371f

• merge

  

  PetarMax

  authored and

  lucasmt

  committed
  5e3c1e8

• Update unlock function in EscrowModel to unlock all of the user's shares

  lucasmt

  committed
  a825995

• Add EscrowAccountingTest

  lucasmt

  committed
  eb9461c

• Add EscrowAccounting tests to run-kontrol.sh script

  lucasmt

  committed
  7320f8d

• Add EscrowOperationsTest and update Setup

  

  qian-hu

  authored and

  lucasmt

  committed
  5317bd2

• Add EscrowOperations tests to run-kontrol.sh script

  

  qian-hu

  authored and

  lucasmt

  committed
  235f93d

• Add postconditions to testLockStEth and testUnlockStEth, accounting for rounding errors

  lucasmt

  committed
  9e0f326

Commits on Jul 8, 2024

• Fix submissionTime and comment out activateNextState()

  qian-hu

  committed
  aab4073

• Add ProposalOperationsTest

  qian-hu

  committed
  98c8857

• Add ProposalOperations tests to run-kontrol.sh script

  qian-hu

  committed
  1187c06

• Update testCanceledOrExecutedActionsCannotBeRescheduled

  qian-hu

  committed
  8a8905a

Commits on Jul 9, 2024

• Fix cancelAllNonExecutedProposals in the timelock model

  qian-hu

  committed
  60a2a5f

• Add testOnlyAdminProposersCanCancelProposals to ProposalOperations tests

  qian-hu

  committed
  e7a8fb6

Commits on Jul 31, 2024

• Moving kaas changes to primary default branch, updating this workflow to now call compute from primary branch workflows

  F-WRunTime

  committed
  68c00e9

• Resolve Conflict, take develop branch changes

  F-WRunTime

  committed
  b2ea538