Implementing sequential composition of program specs

Stream: metaprogramming / tactics

[Vlad]

Reposting this from "new members" topic.

I'd like to implement a new operator for sequential composition of program specifications.
It's written as S ; R where S and R are boolean expressions representing specifications.

Both S and R can use variables with pre-state σ and post-state σ' values.
The sequential composition is defined as follows:

S ; R = ∃ σ'', (fun σ' ↦ S) σ'' ∧ (fun σ ↦ R) σ''

Essentially, it checks if there exist intermediate state σ'' such that both S and R hold after substituting these intermediate states for their respective variables in S and R.

For example, if x and y are variables of S and R, then S ; R should be rewritten as

  ∃ x'' y'', (fun x' y' ↦ S) x'' y'' ∧ (fun x y ↦ R) x'' y''
= ∃ x'' y'', (substitute x'', y'' for x', y' in S) ∧ (substitute x'', y'' for x, y in R)

I've been exploring using macros to achieve this, but I'm stuck on how to rename variable names inside the terms S and R.
Any suggestions or guidance would be greatly appreciated!

[Vlad]

Here what I've got so far:

syntax:20 (name := compose_seq) term:20 " ;; " term:21 : term

partial def elab_compose_seq : TermElab := fun stx type? =>
  match stx with
  | `($R:term ;; $S:term) => do
    let R <- elabTermAndSynthesize R none
    let S <- elabTermAndSynthesize S none
    -- TODO:
    -- get all primed variables in R and replace them with double-primed variables
    -- get all unprimed variables in S and replace them with double-primed variables
    return -- Exists expression with double-primed bound variables
  | _ => return unreachable!

[Notification Bot]

Vlad has marked this topic as resolved.

[Notification Bot]

Vlad has marked this topic as unresolved.