Code

Small IPC lemmas#822

Code

Open

michaelmcinerney wants to merge 14 commits intortseL4/l4v:rtfrom michaelm-small_ipc_lemmasseL4/l4v:michaelm-small_ipc_lemmasCopy head branch name to clipboard

+1,098-604

Commits

Commits on Oct 8, 2024

• rt riscv refine: add cursc_relation

  Show description for b8d82aa
  michaelmcinerney

  committed
  b8d82aa

• rt haskell+design+haskell translator: add readStateAssert

  Show description for 6458c49
  michaelmcinerney

  committed
  6458c49

• rt haskell+design+proof: reduce use of active_sc_at' in CRefine

  Show description for 4d274ae
  michaelmcinerney

  committed
  4d274ae

• rt crefine: move tcbReleaseEnqueue_ccorres

  Show description for 1a6fb39
  michaelmcinerney

  committed
  1a6fb39

• rt riscv refine: speed up proof of commitTime_corres

  Show description for e6c78f5
  michaelmcinerney

  committed
  e6c78f5

• rt crefine: prove postpone_ccorres

  Show description for ee7f1f5
  michaelmcinerney

  committed
  ee7f1f5

• rt crefine: prove schedContext_resume_ccorres

  Show description for 6d71f59
  michaelmcinerney

  committed
  6d71f59

• rt crefine: add obj_at_cslift_ntfn

  Show description for ce90c1c
  michaelmcinerney

  committed
  ce90c1c

• rt crefine: prove maybeDonateSchedContext_ccorres

  Show description for fae09d1
  michaelmcinerney

  committed
  fae09d1

• rt haskell+riscv refine+crefine: prove schedContext_bindTCB_ccorres

  Show description for d54d658
  michaelmcinerney

  committed
  d54d658

• rt haskell+riscv refine+crefine: prove schedContext_bindNtfn_ccorres

  Show description for edc2057
  michaelmcinerney

  committed
  edc2057

• rt haskell+riscv refine+crefine: prove maybeReturnSchedContext_ccorres

  Show description for afa5a87
  michaelmcinerney

  committed
  afa5a87

• rt crefine: remove duplicate of sc_released_ccorres

  Show description for c7875aa
  michaelmcinerney

  committed
  c7875aa

• rt riscv refine: add sym_refs_asrt_def to global [simp] set

  Show description for acf0754
  michaelmcinerney

  committed
  acf0754