Merge master into rt #828

corlewis · 2024-11-20T01:50:00Z

As usual, it probably only makes sense to review the final post-merge commits. The main impacts from master are making use of the new arch_requalify and arch_global_naming commands, and the changes to init_arch_objects.

bump-ver-manifest now takes an optional parameter `--mcs` to operate on `mcs-devel.xml` instead of `devel.xml`. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Python 3.12 complains about `\<` not being a legal escape sequence. Use raw string instead. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Add deployment of the mcs-devel.xml manifest to mcs.xml. The pattern is to use the branch name in `github.ref` as a guard in the initial code freeze action, and then make any subsequent actions depend on either `code` or `mcs-code`, respectively. All of this lives on the master branch (but does trigger on pushes to `rt`), so that it can in the future also trigger on manifest updates from `repository_dispatch` events. Currently the latter does not happen yet, because `github.ref` will be `refs/head/master` for `repository_dispatch` events, so only the main deployment job runs for those. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

i.e. 's/AI_asms/AI_assms/g' and same for Pre_asms ("asms" is rarely expected outside of ML code) Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

* add warnings when exporting a name that already exists in theory context, suppressable by `(aliasing)` option * add `arch` variants of requalify commands that implicitly add the value of L4V_ARCH before whatever you give them, with optional suffixes for abstract (A) and Haskell (H) spec global naming. * write hopefully-understandable documentation with commented examples Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Also document that requalify commands will issue warnings. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Stops namespace pollution, allows us to use Arch locale as example. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

* prefer arch_global_naming * prefer arch_requalify commands over interpretation * indicate consts might need to be requalified in Arch theories * explain (in Arch) + requalify pattern for generic consequences of arch-specific properties Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Unifying the tag between Github labels, docs, and so on will make it less confusing to grep for and deal with. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

- change MCS proof badge to the new deployment workflow - adjust badges to only point to the branch they refer to Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Factor out the platform branch rebase job into its own workflow which is triggered explicitly by a repository-dispatch event. We can then re-trigger the rebase job after the proofs have succeeded on the rebased branch to confirm that everything is now up to date and get a successful rebase test run after everything has completed. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

It was a mix of ARM_A and ARM_HYP_A previously. AInvs+Refine+CRefine needed updates. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

(already in Arch locale) Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Implicitly use L4V_ARCH for global_naming prefix. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

* try get rid of `interpretation Arch .` (slow) in lieu of `(in Arch)` (faster) or proper requalifying (nearly instant) * get rid of requalifications that were already requalified, or were global (thanks to new warnings) * put arch_global_naming on same line as `context Arch begin` Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

* get rid of `global_naming Arch`, this is no longer needed since we can requalify directly from `arch_global_naming` with `arch_requalify` commands * add missing `arch_global_naming` for `context Arch`, for consistency * update X64 Refine `Arch.` references (other arches did not need this) Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

* prevent duplication between arches by moving requalifications from Arch theories to generic ones * this strategy is not available for new constants that are introduced in the Arch locale that need to be referenced in generic definitions or locale instantiations * fix up the inconsistent qualification of set_cap_valid_arch_caps_simple Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Rename the wellformed_acap version to wf_acap_rights_update_id, and the valid_arch_cap version to valid_acap_rights_update_id. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Avoid unnecessary Arch context interpretation (slow). Remove attempts at requalifying entities that are already generic (misleading). Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Makes global_naming implicit (based on L4V_ARCH). Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

This was generic on these two architectures, not consistent with others. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

MiscMachine_A already contains asid_high_bits, asid_low_bits and asid_bits. Other architectures don't duplicate them in Arch_Structs_A, so ARM and ARM_HYP shouldn't either. For ARM, this also means fixing up DRefine+DPolicy+CamkesCdlRefine to refer to the MiscMachine_A definitions when needed (CapDL duplicates them again in Types_D, but as they don't import machine theories, those can't be removed). Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

These proofs have been arch-split for some time now so the FIXMEs appear resolved. They are also non-specific, so it is impossible to tell at this point whether they referred to anything. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

The isabelle.systems site appears to be down for a while, use archive to stop the constant PR links failures while we think of a longer-term solution. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

These were requalified in the middle of the design spec and seemed out of place. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

* makes global_naming implicit (based on L4V_ARCH) * avoid unnecessary Arch context interpretation (slow) Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

* make global_naming implicit (based on L4V_ARCH) * avoid unnecessary Arch context interpretation (slow) * change inclusion point of MachineExports to Types_H and eliminate duplicated requalifications * migrate some Arch-theory requalifications to generic (more consistent interface) * document some name clash disambiguations * annotate vcpu type which can't be moved there, and leave vmrights which is needed for enum instantiations (can't be done in a locale) * unify interface for initIRQController and maxIRQ by providing abbreviations in _H global_naming * do not import generic constants sanitiseRegister and getSanitiseRegisterInfo; their definitions were never imported in lieu of using translated Arch versions that have the same type, causing aliasing warning during const requalification. * update comments where requalify clobbers arch version from abstract spec. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

This uses a complex workaround to unify the parse location of the original name encoded in YXML with the name the user is actually aiming for. While intuitively one could think to use the position of the name we parsed, there appears to be no way to pass that location to read_const/read_type_name, as those expect to be fed the result of Parse.const and Parse.typ respectively. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Previous attempts to update the code to allow ctrl+clicking on names resulted in markup overlap errors for arch_requalify commands. This was due to a misconception that YXML strings already containing correct position information (e.g. obtained via Parse.const) would be used directly by Proof_context.read_const/read_type_name. This is not the case. Instead, position information is adjusted for the content length, and since we add a prefix for L4V_ARCH, we got annotation that did not match the document text. After hours of digging to uncover the above issue, we get this: * the "check_parsed_nm" in gen_requalify was not an extra check, but a hook to do document annotation; updated comments * use Proof_Context.check_const/check_type_name with user-supplied name and parsed position of Parse.name, and manually report resulting markup (do not use previously resolved name as it could point to a hidden const/type) * since the above works for arch_requalify_const, the normal requalify_const becomes a simpler instance of it * the whole Parse.const/Parse.typ was a red herring and ultimately did not add anything to the code except for read_const/read_type_name interaction; removed The resulting code is simpler; large cautionary comments remain for future generations. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Document/test surprising interactions of hide_const, locales and requalify for the purposes of temporarily making arch-specific constants visible in theory scope. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>