Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Proofs for SGI API #733

Draft
wants to merge 20 commits into
base: master
Choose a base branch
from
Draft

Proofs for SGI API #733

wants to merge 20 commits into from

Commits on Mar 26, 2024

  1. cspec: explain why config keys are renamed 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    c5d88c7 View commit details
    Browse the repository at this point in the history

  2. cspec: make config_ARM_GIC_V3 config visible to proofs 

    In preparation for adding an API for software-generated interrupts,
make config_ARM_GIC_V3 visible to the proofs, so values of constants
can be defined conditionally on GICv2/v3 use.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    32a8990 View commit details
    Browse the repository at this point in the history

  3. aarch64 machine: add ipiSendTarget machine op 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    b6943d5 View commit details
    Browse the repository at this point in the history

  4. haskell: add SGISignalCap API 

    This affects all architectures, because generic interfaces are changing,
but the SGISignalCap API is only added to ARM, ARM_HYP, and AARCH64.
For X64 and RISCV64, we trivially implement the new interfaces, and in
generic code we call those interfaces.

These new interfaces are isArchMDBParentOf and
isIRQControlCapDescendant, for checking in generic code if there are
architecture specific cases in isMDBParentOf and isCapRevocable
respectively.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    5e0b269 View commit details
    Browse the repository at this point in the history

  5. arm+arm-hyp+aarch64 machine: IPI + SGI machine interface 

    Define the new constants numSGIs and gicSGITargetMaskBits, plus a new
machine operation ipiSendTarget.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    f54f8aa View commit details
    Browse the repository at this point in the history

  6. design+haskell-translator: add new arch interfaces and caseconvs 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    c75b9f8 View commit details
    Browse the repository at this point in the history

  7. aspec: add SGISignalCap API + cdt interfaces 

    - add SGISignalCap API for ARM, ARM_HYP, AARCH64
- add generic interface for should_be_arch_parent_of and
  is_irq_control_descendant in the cdt implementation
- add default interface implementations new interfaces for RISCV64, X64

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    5d1ef38 View commit details
    Browse the repository at this point in the history

  8. x64+riscv ainvs: adjust for new CDT interface 

    This contains a slight tweak to generic CSpace_AI and proof adjustments
for the architectures that do not implement the SGISignalCap API.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    7a1a026 View commit details
    Browse the repository at this point in the history

  9. arm+arm-hyp+aarch64 ainvs: SGISignalCap proofs 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    b4bd110 View commit details
    Browse the repository at this point in the history

  10. x64+riscv refine: CDT interface update 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    bd4e95b View commit details
    Browse the repository at this point in the history

  11. arm+arm-hyp+aarch64: SGISignalCap proofs 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    1670481 View commit details
    Browse the repository at this point in the history

  12. x64+riscv crefine: CTD interface updates 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    6b9a2ab View commit details
    Browse the repository at this point in the history

  13. arm+arm-hyp+aarch64: SGISignalCap proofs 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    05d4e36 View commit details
    Browse the repository at this point in the history

  14. arm access+infoflow: SGISignalCap security thms 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    961e607 View commit details
    Browse the repository at this point in the history

  15. capDL: add SGISignalCap API to capDL 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    bb2d6e6 View commit details
    Browse the repository at this point in the history

  16. drefine+dpolicy: SGISignalCap proofs 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    0144f61 View commit details
    Browse the repository at this point in the history

  17. capDL: SGISignalCap API for SepDSpec and DSpecProofs 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    9116b66 View commit details
    Browse the repository at this point in the history

  18. sys-init: exclude SGISignalCap 

    For now exclude SGISignalCap from wellformed specs. To be relaxed
later.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    3f971a8 View commit details
    Browse the repository at this point in the history

  19. capDL-api: restyle IRQ_DP 

    Fix + modernise style and proofs.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    6d1df8d View commit details
    Browse the repository at this point in the history

  20. capDL-api: seplogic lemmas for ARMIssueSGISignal 

    Add separation logic specification lemmas for the new SGISignalCap API
for later use in sys-init.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37
    lsf37 committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    dc2fd26 View commit details
    Browse the repository at this point in the history