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

[WIP] Opinionated deployment of enhanced Requalify capabilities on AInvs #791

Closed
wants to merge 9 commits into from
Closed

[WIP] Opinionated deployment of enhanced Requalify capabilities on AInvs #791

wants to merge 9 commits into from

Commits on Jul 23, 2024

  1. ainvs: use "assms" in name for arch locales 

    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 <[email protected]>
    @Xaphiosis
    Xaphiosis committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    647fa12 View commit details
    Browse the repository at this point in the history

  2. lib: overhaul Requalify, add arch variants 

    * 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 <[email protected]>
    @Xaphiosis
    Xaphiosis committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    d4f5564 View commit details
    Browse the repository at this point in the history

  3. docs: arch-split: requalifying into Arch locale 

    Also document that requalify commands will issue warnings.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    e1ff464 View commit details
    Browse the repository at this point in the history

  4. lib: migrate Requalify tests into test/ 

    Stops namespace pollution, allows us to use Arch locale as example.

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    705a73b View commit details
    Browse the repository at this point in the history

  5. [wip] gen+aarch64 ainvs: deploy requalify infrastructure 

    Temporarily only dealing with AARCH64; want feedback before applying to
other arches.

* global_naming AARCH64 -> arch_global_naming
* 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)
  TODO: some of these will turn out to be broken because they're not
  actually global/exported on other arches
* put arch_global_naming on same line as `context Arch begin`
* annotate requalifications in Arch theories that can be moved to
  generic
* put FIXMEs on unusual global_naming practices

Signed-off-by: Rafal Kolanski <[email protected]>
    @Xaphiosis
    Xaphiosis committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    c248d31 View commit details
    Browse the repository at this point in the history

  6. [wip] gen+aarch64 ainvs: add missing arch_global_naming 

    * 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
    @Xaphiosis
    Xaphiosis committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    54473b2 View commit details
    Browse the repository at this point in the history

  7. ainvs: disambiguate acap_rights_update_id 

    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 <[email protected]>
    @Xaphiosis
    Xaphiosis committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    22cccb3 View commit details
    Browse the repository at this point in the history

  8. [wip] gen+aarch64 ainvs: move requalifies to generic theories 

    * 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
    @Xaphiosis
    Xaphiosis committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    9a10755 View commit details
    Browse the repository at this point in the history

  9. [wip] docs: arch-split.md: more overhaul 

    * 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
    @Xaphiosis
    Xaphiosis committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    f1270aa View commit details
    Browse the repository at this point in the history