Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Sync audit formal verification (#294)
* Certora's formal verification effort for Manifest (#259) * Certora's formal verification effort for Manifest - Verification rules are in `programs/manifest/src/certora/spec` - Mock for red-black tree in `cvt_db_mock.rs` - Mock for QuoteAtomsPerBaseAtoms in `quantities_certora.rs` - Uses conditional compilation with feature `certora` to plug in the mocks - See the accompanying audit report for additional details * specs: add rules for matching mechanism --------- Co-authored-by: caballa <[email protected]> * Fix build * More making certora compile * More fixes * add updated script * Fix verify * Update rbtree * Fix list of rules for violated rules * Remove expected to be violated rules * Cleanup * Update logs * comment on batch update * Processor * quantities * utils * Update github action * Fix lint * Fix unused * Unused * action remove with * remove container * remove container * Fix yml --------- Co-authored-by: nisarg-certora <[email protected]> Co-authored-by: caballa <[email protected]>
- Loading branch information