Code

AArch64 fastpath proofs#739

Code

Merged

lsf37 merged 8 commits intoseL4:masterseL4/l4v:masterfrom Xaphiosis:aarch64_fastpathXaphiosis/l4v:aarch64_fastpathCopy head branch name to clipboardMar 25, 2024

+2,474-1,982

Commits

Commits on Mar 25, 2024

• lib: generic monadic_rewrite_state_assert/stateAssert

  Show description for 0033f2d
  Xaphiosis

  committed
  0033f2d

  Copy full SHA for 0033f2d

• crefine: update for monadic_rewrite_stateAssert

  Show description for f2f38b7
  Xaphiosis

  committed
  f2f38b7

  Copy full SHA for f2f38b7

• haskell+design: add fastpathKernelAssertions

  Show description for c407d26
  Xaphiosis

  committed
  c407d26

  Copy full SHA for c407d26

• refine+crefine: define and handle fastpathKernelAssertions

  Show description for 56e125d
  Xaphiosis

  committed
  56e125d

  Copy full SHA for 56e125d

• aarch64 crefine: fastpath specs for call and replyrecv

  Show description for dba6177
  Xaphiosis

  committed
  dba6177

  Copy full SHA for dba6177

• aarch64 crefine: prove fastpath equivalent to slow path

  Show description for 467ef27
  Xaphiosis

  committed
  467ef27

  Copy full SHA for 467ef27

• aarch64 crefine: prove fastpath equivalent to C fastpath

  Show description for 754acc3
  Xaphiosis

  committed
  754acc3

  Copy full SHA for 754acc3

• proof: remove AArch64 quick_and_dirty CRefine

  Show description for 4efd093
  Xaphiosis

  committed
  4efd093

  Copy full SHA for 4efd093