Code

Initial formal verification results#69

Code

Merged

wojciechozga merged 18 commits intoIBM:mainIBM/ACE-RISCV:mainfrom lgaeher:ci/lennard/verificationlgaeher/ACE-RISCV:ci/lennard/verificationCopy head branch name to clipboardJul 19, 2024

Commits

Commits on Jul 10, 2024

• Work on Page verification

  Show description for e36bd02
  lgaeher

  committed
  e36bd02

  Copy full SHA for e36bd02

• work on spec for page allocator

  Show description for 028125f
  lgaeher

  committed
  028125f

  Copy full SHA for 028125f

• simplifying page table memory representation

  Show description for 014bcd2
  

  wojciechozga

  authored and

  lgaeher

  committed
  014bcd2

  Copy full SHA for 014bcd2

• more work on page

  Show description for f3a117c
  lgaeher

  committed
  f3a117c

  Copy full SHA for f3a117c

• work on new page allocator spec

  Show description for 3498f9d
  lgaeher

  committed
  3498f9d

  Copy full SHA for 3498f9d

• add readme document outlining the verification

  Show description for 31a38a2
  lgaeher

  committed
  31a38a2

  Copy full SHA for 31a38a2

• build fixes

  Show description for 159276c
  lgaeher

  committed
  159276c

  Copy full SHA for 159276c

Commits on Jul 11, 2024

• fix build

  Show description for 93b2363
  lgaeher

  committed
  93b2363

  Copy full SHA for 93b2363

Commits on Jul 12, 2024

• bump opensbi

  Show description for c8af232
  lgaeher

  committed
  c8af232

  Copy full SHA for c8af232

• fix build script

  Show description for 23e671e
  lgaeher

  committed
  23e671e

  Copy full SHA for 23e671e

• ci fixes

  Show description for fb3c99e
  lgaeher

  committed
  fb3c99e

  Copy full SHA for fb3c99e

Commits on Jul 16, 2024

• Include suggestions in readme

  Show description for 67352a2
  

  lgaeher

  and

  wojciechozga

  committed
  67352a2

  Copy full SHA for 67352a2

• change makefile message

  Show description for b5692de
  lgaeher

  committed
  b5692de

  Copy full SHA for b5692de

• work on cleanups

  Show description for 4735e62
  lgaeher

  committed
  4735e62

  Copy full SHA for 4735e62

Commits on Jul 17, 2024

• some coq refactoring

  Show description for 3c68342
  lgaeher

  committed
  3c68342

  Copy full SHA for 3c68342

• clean up page table

  Show description for 8ce19f4
  lgaeher

  committed
  8ce19f4

  Copy full SHA for 8ce19f4

Commits on Jul 19, 2024

• address comments

  Show description for 2c4cd98
  lgaeher

  committed
  2c4cd98

  Copy full SHA for 2c4cd98

• make read accessible only on Allocated pages

  Show description for 9198b40
  lgaeher

  committed
  9198b40

  Copy full SHA for 9198b40