Gerwin Klein
865facfde9
aarch64 refine: first pass through Ipc_R
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Rafal Kolanski
4dfb6f8ad3
aarch64 refine: first pass through Finalise_R
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Gerwin Klein
be22c7bfcc
aarch64 refine: set up Untyped_R from RISCV64, add hyp/vcpu
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Gerwin Klein
0a7eaece00
aarch64 refine: copy over Invocations_R from RISCV64
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:44 +10:00
Gerwin Klein
f4c12a6d85
aarch64 refine: remove kernel_mappings in Retype/Detype
...
These do not exist on AARCH64
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Gerwin Klein
5601abc530
aarch64 refine: fill in VSpaceObject cases in Retype_R
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Rafal Kolanski
a4536a17ce
aarch64 refine: first pass through Detype_R
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Rafal Kolanski
e508693534
aarch64 refine: first pass through Retype_R
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Rafal Kolanski
3a77d097c4
aarch64 refine: first pass through IpcCancel_R
...
needed some changes to Schedule_R and VSpace_R
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:43 +10:00
Rafal Kolanski
044a97ed1a
aarch64 refine: first run through Schedule_R
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:42 +10:00
Rafal Kolanski
904056868d
aarch64 refine: add state_hyp_refs_of' to valid_state'
...
Somehow we missed this on the first pass. Adjusted existing proofs.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:42 +10:00
Rafal Kolanski
a79e06f419
aarch64 refine: first run through VSpace_R
...
This required a lot of adaptation from ARM_HYP, rearranging, and fixing.
The VCPU lemmas are mostly now constrained to one area, making it
theoretically possible to make a VCPU theory in the future.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:42 +10:00
Gerwin Klein
0f11a7a52a
aarch64 refine: progress in ArchAcc
...
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:42 +10:00
Rafal Kolanski
97ebd07298
aarch64 refine: start on VSpace_R
...
Up to and including handleVMFault_corres which needed a major overhaul.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:42 +10:00
Rafal Kolanski
059afc8743
aarch64 refine: add InterruptAcc_R
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Rafal Kolanski
cb03631312
aarch64 refine: add TcbAcc_R and ArchMove_R
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Rafal Kolanski
2b543da5f3
aarch64 refine: add CSpace_R
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Rafal Kolanski
18d76ef54b
aarch64 refine: add vcpuBits_def to objBits_defs
...
The way we handle vcpuBits on AARCH64 is different to ARM_HYP.
This seems the most logical place to put vcpuBits_def to aid automation.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Rafal Kolanski
a93a62641d
aarch64 refine: copy RAB_FN from RISCV64
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Rafal Kolanski
e0114eef06
aarch64 refine: add CSpace_I and CSpace1_R
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-26 18:04:41 +10:00
Gerwin Klein
3b5a983362
aarch64 refine: first pass through ArchAcc_R
...
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-26 18:04:40 +10:00
Gerwin Klein
b42665460d
aarch64 refine: use ptTranslationBits for indices
...
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:18 +10:00
Gerwin Klein
38a65fd453
aarch64 refine: adjust KHeap_R from RISCV64
...
Add VCPU/hyp lemmas from ARM_HYP, fix and update failing lemmas. Leave
1 sorry on pspace_canonical, which might not be needed for AARCH64.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:17 +10:00
Gerwin Klein
b882216086
aarch64 refine: copy Machine_R from RISCV64
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:17 +10:00
Gerwin Klein
555bff6f6c
aarch64 refine: copy SubMonad_R from RISCV64
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:17 +10:00
Gerwin Klein
7cdb85fad1
aarch64 refine: copy EmptyFail from RISCV64
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:17 +10:00
Gerwin Klein
bf3929b9d5
aarch64 refine: adjust Bits_R from RISCV64
...
Add VCPU/hyp material from ARM_HYP, fix up broken lemmas.
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:17 +10:00
Gerwin Klein
61bce83518
aarch64 refine: copy Corres.thy from RISCV64
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:17 +10:00
Gerwin Klein
55a01f1829
aarch64 refine: complete StateRelation
...
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:16 +10:00
Gerwin Klein
9f25a4e8f6
aarch64 haskell: use ppn concept for PageTablePTEs
...
Don't store the bottom 12 bits of the base address for page table PTEs,
because we know they are zero. This gives us implicit alignment to
pageBits in the page table walker.
The C code stores only 36 significant bits, whereas this commit still
uses a full 64-bit machine word for the ppn in Haskell. To be adjusted
in a future change.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:16 +10:00
Gerwin Klein
394f74b615
aarch64 aspec: sync vmid bit width with Haskell+C
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:16 +10:00
Gerwin Klein
0b0b3b32d5
aarch64 refine: iteration on Invariants_H
...
Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.system>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:16 +10:00
Gerwin Klein
44fc3ec8d5
aarch64 refine: copy LevityCatch from RISCV64
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:16 +10:00
Gerwin Klein
96851e8b34
aarch64 ainvs: fix typo
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-25 19:34:16 +10:00
Rafal Kolanski
1404b9c0d0
aarch64 refine: add StateRelation
...
Only text replacement of RISCV64->AARCH64 for now.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-25 19:34:15 +10:00
Rafal Kolanski
01575f20d5
aarch64 refine: copy InvariantUpdates_H from RISCV64
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-25 19:34:15 +10:00
Rafal Kolanski
148355479f
aarch64 refine: first attempt at Invariants_H
...
Quite a few issues remain, notably validity of ASID maps and
relationship to ASID table is missing from valid_arch_state'
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-25 19:34:15 +10:00
Rafal Kolanski
0794e0a427
run_tests: enable BaseRefine for AARCH64
...
Switch exclusion to Refine.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-25 19:34:15 +10:00
Rafal Kolanski
59bf9d92c8
docs: style: right- vs left-wrapping of operators
...
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
2023-05-04 11:36:50 +10:00
Gerwin Klein
2545aa0e51
github: add manual triggers for testing
...
The worklow_dispatch trigger adds a button in the GitHub UI that lets
one trigger the workflow manually. Useful for testing the workflows.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-05-03 14:23:06 +10:00
Michael McInerney
ca589b635c
c-parser: add dom_lift_t_heap_update and lemmas for proj_d
...
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
2023-05-01 15:16:22 +09:30
Michael McInerney
ac5fe5bd59
refine: add obj_range'_disjoint
...
This also moves several lemmas required for obj_range'_disjoint
to Invariants_H
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
2023-05-01 10:52:50 +09:30
Michael McInerney
1273ba314a
clib: generalise monadic_rewrite_ccorres_assemble
...
This makes the flags schematic
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
2023-04-27 08:12:31 +10:00
Corey Lewis
b8714328cb
word_lib+crefine: add and_one_neq_simps and adjust proofs
...
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
2023-04-18 13:23:42 +10:00
Corey Lewis
68e33858e2
crefine: simp rules for true and false
...
These rules allow the simplifier to solve almost all existing goals that
involve the C constants true and false, without unfolding their
definitions.
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
2023-04-18 13:23:42 +10:00
Corey Lewis
ba241aac64
riscv+x64 crefine: remove unused lemma
...
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
2023-04-18 13:23:42 +10:00
Gerwin Klein
1d2e75fd81
word_lib: lemma to turn < into bitwise reasoning
...
word_less_bit_eq turns `<` into a bitwise expression on abstract word
length to make it easier to reason about the relationship of < and bit
operations (boolean, but also shift etc).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-04-11 13:17:54 +10:00
Gerwin Klein
d4a63b2784
word_lib: more docs on word_bitwise and word_eqI
...
The Eisbach method command doesn't seem to allow providing a doc
string. Instead at least place a comment right next to the definition
so that people can find that when they discover the method name with
print_methods.
Update doc string of word_bitwise to clarify where it is useful.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-04-11 13:17:53 +10:00
Gerwin Klein
b72e177677
word_lib: laws about min, max, and NOT
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-04-11 13:17:53 +10:00
Gerwin Klein
d163d41b63
word_lib: some cleanup in More_Word
...
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2023-04-11 13:17:53 +10:00