Planning for Copilot 4.7.2 / 4.8

[ivanperez-keera]

This thread is to collect ideas for the next release of Copilot after 4.7.1 (May 7th), which will be versioned 4.7.2 or 4.8 (depending on whether we need to bump the major or not or not), and will be released on July 7th.

List ideas down if you want them considered for this release.

Shortlist (will be edited based on comments / discussions):

• @carte731 to work on removing LambdaCase.
  • Discussion: Planning for Copilot 4.6.1 #684 (comment)
  • Tentative branch: https://github.com/carte731/copilot
• @rlipkis to work on removing PatternSynonyms.
• @kavehz-nasa to work on adding version bounds to the dependencies of what4-arithmetic-counterexamples.
• @chathhorn-galois to upgrade copilot-theorem to work with a more modern version of kind2.
• @RyanGlScott ?

[ivanperez-keera]

Kaveh, would you like to take a stab at fixing this warning we get when uploading packages to Hackage:

Warnings:                                                                        
- [missing-upper-bounds] On executable 'what4-arithmetic-counterexamples',       
these packages miss upper bounds:                                                
- - containers

That one's related to

copilot/copilot/copilot.cabal

Line 89 in 0c987a7

executable what4-arithmetic-counterexamples

Context: #690

[ivanperez-keera]

@carte731 if you want, once we deal with that one related to lambda case, you could also remove (in separate issues and PRs)

• PatternSynonyms

@RyanGlScott Is NondecreasingIndentation needed in the verifier?

[RyanGlScott]

Is NondecreasingIndentation needed in the verifier?

I honestly don't remember. It it does, however, then I imagine that it could easily be removed with some minor refactoring.

[ivanperez-keera]

Is there a chance that the same code could still compile without that extension but mean something different?

Or is it just a matter of removing the extension and seeing if it compiles? If the latter, this would be a great issue for someone new to the project.

[RyanGlScott]

I am aware of two prior discussions containing some noticeable (but relatively easy-to-fix) bugs. Perhaps we should elevate these to issues?

• copilot-verifier: 25 verifier tests fails with 'instruction code 62 is unknown' #685 (specifically, copilot-verifier does not work with Nix's version of clang out of the box due to it enabling -fwrapv, see 25 verifier tests fails with 'instruction code 62 is unknown' #685 (reply in thread))
• copilot-bluespec: Bit Vector of Unknown Size Error in Generated Bluespec Code #648

[chathhorn-galois]

Another thing worth including (as @RyanGlScott mentioned in the meeting today): updating copilot-theorem to work with the latest version of the Kind2 model checker.

Currently, copilot-theorem generates Kind2 input in its s-expression-based native format, which has evolved over the past few years so that copilot-theorem's output is no longer accepted by current versions (v2.3.0) of Kind2. I think it's probably been broken since Kind2 v1.0 or so.

The biggest difference appears to be in the location and style of "property" definitions -- newer Kind2 expects them to be nested inside a top-level define-node expression, whereas copilot-theorem currently places them in a top-level check-prop expression.

E.g., consider this Copilot spec:

kind2 = check $ kind2Prover def

counter :: Stream Word32
counter = [0] ++ (counter + 1) 
                          
spec = do
    bounds <- prop "bounds" (forAll $ counter < 255)
    theorem "nonneg" (forAll $ counter >= 0) (assume bounds >> kind2)

It currently produces the following Kind2 output:

(define-pred top
  ((prop-bounds.out Bool)
   (prop-nonneg.out Bool)
   (s0.out Int)
   (s0.out.1 Int))
  (init
    (and
      (and
        (= prop-bounds.out
          (< s0.out 255))
        (= prop-nonneg.out
          (>= s0.out 0))
        (= s0.out 0)
        (= s0.out.1
          (+ s0.out 1))) bounds))
  (trans
    (and
      (and
        (= (prime prop-bounds.out)
          (< (prime s0.out) 255))
        (= (prime prop-nonneg.out)
          (>= (prime s0.out) 0))
        (= (prime s0.out) s0.out.1)
        (= (prime s0.out.1)
          (+ (prime s0.out) 1))) (prime bounds))))

(check-prop
  ((nonneg prop-nonneg.out)))

Whereas current versions of Kind2 expect something along these lines:

(define-node top
  ((prop-bounds.out Bool)
   (prop-nonneg.out Bool)
   (s0.out Int)
   (s0.out.1 Int))
  (init
    (and
      (and
        (= prop-bounds.out
          (< s0.out 255))
        (= prop-nonneg.out
          (>= s0.out 0))
        (= s0.out 0)
        (= s0.out.1
          (+ s0.out 1))) prop-bounds.out))
  (trans
    (and
      (and
        (= (prime prop-bounds.out)
          (< (prime s0.out) 255))
        (= (prime prop-nonneg.out)
          (>= (prime s0.out) 0))
        (= (prime s0.out) s0.out.1)
        (= (prime s0.out.1)
          (+ (prime s0.out) 1))) (prime prop-bounds.out)))

  (props
    ((nonneg prop-nonneg.out :user myfile:28-3))))

I think updating the Kind2 native format along these lines should be straightforward, requiring relatively minor changes mostly to Kind2/PrettyPrint.hs, Kind2/AST.hs, and Kind2/Translate.hs.

Longer-term, it would be much better to target Lustre V4, which is a well-documented language independent of just Kind2 and is Kind2's only officially-supported input language. But this would of course require more effort than just updating support for the native format.

[ivanperez-keera]

A few additional notes from discussions in the meeting:

@rlipkis will also be contributing to the next release, starting with a very small issue.