Skip to content

Port HeapLang tactics #480

Description

@suhr

Port remaining HeapLang tactics from Rocq Iris.

Tactics to take one or more pure program steps:

  • wp_pure
  • wp_pures
  • wp_rec
  • wp_lam
  • wp_let
  • wp_seq
  • wp_proj
  • wp_if_true
  • wp_if_false
  • wp_if
  • wp_unop
  • wp_binop
  • wp_op
  • wp_case
  • wp_match
  • wp_inj
  • wp_pair
  • wp_closure

Tactics for the heap:

  • wp_alloc
  • wp_load
  • wp_store
  • wp_cmpxchg_suc
  • wp_cmpxchg_fail
  • wp_cmpxchg
  • wp_faa

Further tactics:

  • wp_bind
  • wp_apply
  • wp_smart_apply

Metadata

Metadata

Assignees

No one assigned

    Labels

    claimedSomebody is working on thisportingPorting Rocq developmentproof-modeProofMode porting tasks

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions