Commits

Branch selector

 master

User selector

All users

All time

Commit History

Commits on Apr 13, 2026

• spec+proof: move call to setThreadState within suspend

  Show description for 1583255
  

  michaelmcinerney

  authored and

  lsf37

  committed
  1583255

  Copy full SHA for 1583255

Commits on Apr 9, 2026

• haskell+refine+crefine: align scheduleTCB with ASpec and C

  Show description for 59b2d2f
  

  michaelmcinerney

  authored and

  lsf37

  committed
  59b2d2f

  Copy full SHA for 59b2d2f

Commits on Apr 1, 2026

• refine: arch-split InterruptAcc_R

  Show description for 88b6421
  Xaphiosis

  committed
  88b6421

  Copy full SHA for 88b6421

• refine: arch-split Init_R

  Show description for 19ab0af
  Xaphiosis

  committed
  19ab0af

  Copy full SHA for 19ab0af

• cspec/c: extract maxIRQ for RISCV64

  Show description for 5a81e25
  lsf37

  committed
  5a81e25

  Copy full SHA for 5a81e25

Commits on Mar 30, 2026

• refine: arch-split IpcCancel_R and update

  Show description for c097c61
  Xaphiosis

  committed
  c097c61

  Copy full SHA for c097c61

• refine: IpcCancel_R given arch prefix

  Show description for ed6405f
  Xaphiosis

  committed
  ed6405f

  Copy full SHA for ed6405f

• refine: expose threadSet_invs_trivialT as generic interface

  Show description for 6efdfc6
  Xaphiosis

  committed
  6efdfc6

  Copy full SHA for 6efdfc6

• infoflow refine: update for Detype_R arch-split

  Show description for c7cb651
  Xaphiosis

  committed
  c7cb651

  Copy full SHA for c7cb651

• crefine: update for Detype_R arch-split

  Show description for 66a24ba
  Xaphiosis

  committed
  66a24ba

  Copy full SHA for 66a24ba

• refine+orphanage: update for Detype_R arch-split

  Show description for 4061600
  Xaphiosis

  committed
  4061600

  Copy full SHA for 4061600

• refine: arch-split Detype_R

  Show description for bd07a11
  Xaphiosis

  committed
  bd07a11

  Copy full SHA for bd07a11

• refine: Detype_R given arch prefix

  Show description for f14d860
  Xaphiosis

  committed
  f14d860

  Copy full SHA for f14d860

Commits on Mar 25, 2026

• arm+arm-hyp crefine: fix nextDomain for NUM_DOMAINS=1

  Show description for 0a1ed59
  lsf37

  committed
  0a1ed59

  Copy full SHA for 0a1ed59

Commits on Mar 24, 2026

• spec+proof: fix domain schedule wrap

  Show description for e8ba986
  lsf37

  committed
  e8ba986

  Copy full SHA for e8ba986

• infoflow: dynamic domain scheduler

  Show description for 7d6bbe5
  lsf37

  committed
  7d6bbe5

  Copy full SHA for 7d6bbe5

• sys-init: dynamic domain scheduler

  Show description for 4270930
  lsf37

  committed
  4270930

  Copy full SHA for 4270930

• drefine: dynamic domain scheduler

  Show description for d9b521b
  lsf37

  committed
  d9b521b

  Copy full SHA for d9b521b

• capdl: dynamic domain scheduler

  Show description for 66055f3
  lsf37

  committed
  66055f3

  Copy full SHA for 66055f3

• access: add no_domain_caps

  Show description for 6eb8e61
  lsf37

  committed
  6eb8e61

  Copy full SHA for 6eb8e61

• access: dynamic domain scheduler

  Show description for 0cec0a1
  lsf37

  committed
  0cec0a1

  Copy full SHA for 0cec0a1

• crefine: dynamic domain scheduler

  Show description for 530a156
  lsf37

  committed
  530a156

  Copy full SHA for 530a156

• refine: dynamic domain scheduler

  Show description for 91eef8f
  lsf37

  committed
  91eef8f

  Copy full SHA for 91eef8f

• ainvs: dynamic domain scheduler

  Show description for 1abd6e8
  lsf37

  committed
  1abd6e8

  Copy full SHA for 1abd6e8

• cspec: remove static domain schedule from build

  Show description for a07dd71
  lsf37

  committed
  a07dd71

  Copy full SHA for a07dd71

• aspec: dynamic domain scheduler

  Show description for 0365e80
  lsf37

  committed
  0365e80

  Copy full SHA for 0365e80

• design+translator: dynamic domain scheduler

  Show description for 1e87d6b
  lsf37

  committed
  1e87d6b

  Copy full SHA for 1e87d6b

• haskell: dynamic domain scheduler

  Show description for e0db262
  lsf37

  committed
  e0db262

  Copy full SHA for e0db262

• machine: define domainBits bound for domain values

  Show description for c8d1710
  lsf37

  committed
  c8d1710

  Copy full SHA for c8d1710

• clib: ccorres lemmas

  Show description for ef3a9e5
  lsf37

  committed
  ef3a9e5

  Copy full SHA for ef3a9e5

• lib: lemmas for none_top/bot, pairs, listUpdate, corres

  Show description for 831f5d6
  lsf37

  committed
  831f5d6

  Copy full SHA for 831f5d6

• word_lib: rewrites for ucast on 0

  Show description for 9e9bccd
  lsf37

  committed
  9e9bccd

  Copy full SHA for 9e9bccd

Commits on Mar 23, 2026

• tests.xml+Makefiles: handle ASpec file dependencies

  Show description for 8c14fa9
  lsf37

  committed
  8c14fa9

  Copy full SHA for 8c14fa9

Commits on Mar 19, 2026

• sys-init+capDL-api: add SMC caps to initialiser

  Show description for 8c1ba82
  lsf37

  committed
  8c1ba82

  Copy full SHA for 8c1ba82

• proofs: update capDL-related proofs for SMC caps

  Show description for 2089f16
  lsf37

  committed
  2089f16

  Copy full SHA for 2089f16