Planning for Copilot 4.7

[ivanperez-keera]

The following is a tentative plan for Copilot 4.7:

• Hopefully we can tackle:
  • copilot-language - Unable to drop as many elements from Stream as prepended #607 (hard to review)
  • Extend range of versions of dependencies #603 (easy/medium, but we are blocked due to some dependencies not upgrading to newer versions of GHC)
  • copilot-bluespec: Tests are failing on Hackage #673 (easy)

Anyone wants to volunteer with those?

We also have a couple of issues pending from the Galois team that we want to add to this release. Can someone remind me of those?

Finally, we want to update the documentation for the Bluespec backend.

Please comment below if you are available to help out with this release, and if there's an issue you'd like to work on or you think we should be adding to this release.

Everything has to be merged by Dec 21, so we have a little over a month for planning, implementation, testing & acceptance.

[ivanperez-keera]

Tagging @RyanGlScott for awareness. Please tag your Galois colleagues to draw attention to this thread.

[ivanperez-keera]

Tagging also @fdedden @estherdconrad @chathhorn @kaBeech @carte731

[RyanGlScott]

Some tasks that we would definitely like to address on the Galois side (and already have prototype implementations for) are:

• copilot-bluespec: Tests are failing on Hackage #673
• Give more graceful error message when compiling `Array 0` to C99? #649
• `copilot-{bluespec,theorem}`: Special floating-point values are translated incorrectly #675

We would need to promote the latter two to full Copilot issues before proceeding.

[ivanperez-keera]

Could you please file the last two using template we are using? Like before, don't apply labels yet, I'll come in, review, adjust (if needed), and apply labels to progress it to the point where they can be accepted.

[RyanGlScott]

I have opened #695 for the issue about empty arrays and structs in C99 (what was previously discussed in #649).

Thinking more about #675, I think the discussion there is really about two separate (but closely related) bugs:

1. copilot-bluespec's constFP function produces syntactically invalid Bluespec code for negative zero, infinity, and NaN values. This affects values of type Float and Double.
2. copilot-bluespec and copilot-theorem use the realToFrac function, which results in Float values that are syntactically valid, but nevertheless the wrong values (e.g., NaN is turned into infinity). This only affects values of type Float, as we only ever call realToFrac on Floats.

If you are agreeable, then I think it would be worth filing two separate issues for each of these bugs, and then we could fix (1) before we fix (2). We would be able to add a copilot-bluespec test case demonstrating that compilation preserves special Double values after just fixing (1), but we wouldn't be able to add a corresponding test case for special Float values unless we fixed both (1) and (2).

[RyanGlScott]

Based on a discussion with @ivanperez-keera, we decided to split these into two issues:

• copilot-bluespec: Special floating-point values are translated to syntactically invalid Bluespec code #696 (for bug 1 above)
• copilot-{bluespec,theorem}: Special Float values are translated incorrectly #697 (for bug 2 above)

[ivanperez-keera]

I also would like to try to address this issue for the upcoming release:

#608

I could use your help reviewing this PR, @RyanGlScott . I want to make sure I don't miss any edge cases. Is that something you could help review (I'm aware that you already went through it and left some comments)?

[RyanGlScott]

Sure, this is something that we could work on.

As I understand it, #608 is mostly complete, other than it lacking tests?

[ivanperez-keera]

I have not reviewed the conversation in detail. Were you able to try it? Does it work? Anything that seems "suspicious"?

[RyanGlScott]

It does work, although there is a question of how far we should go with this idea. For instance, the current implementation of #608 allows drop 2 ([True, True] ++ false) to work, but it does not allow drop 3 ([True, True] ++ false), even though one could imagine making that work (similarly to how drop 3 false currently works). Doing so would require adding additional special cases to drop beyond what is included in #608.

[ivanperez-keera]

From what I understand, it doesn't stop a case that currently works from working, but simply extends the cases that should work and do. Is that a fair assessment of the implementation in the PR?

[RyanGlScott]

Yes, that's correct.

[ivanperez-keera]

Potentially, we could also work on: #641. Specifically, I'd like to port the examples first to use What4 or SMT, and later (possibly in Copilot 4.8) we can remove the unused Z3 module.

[RyanGlScott]

We'd also be up for working on this. Should we file a Copilot issue first about porting the relevant examples from Copilot.Theorem.Prover.Z3 to Copilot.Theorem.Prover.SMT?

[ivanperez-keera]

Yes, we'd have to do that. Feel free to go ahead, filing it as close as possible to the template we are using. Don't apply labels yet, I'll come in, review, adjust (if needed), and apply labels to progress it to the point where it can be accepted.

[RyanGlScott]

I've opened #692 for this.

[ivanperez-keera]

I also would like to eliminate the use of LambdaCase (\case) from the repo, to remove extensions that are not needed.

@carte731 is that something you could help with?

The essence is that there's an extension to the Haskell language that allows one to write switch/select statements like this:

myFunction $ \case ->
  C1 -> result1
  C2 -> result2

instead of writing:

myFunction $ \arg-> case arg of
  C1 -> result1
  C2 -> result2

That extension doesn't really save us much code, but bit by bit the Haskell language we need to support (and our devs need to learn) becomes bigger. It would take going through the code, finding all cases where that happens, and expanding those \case into \someVarName -> case someVarName of. The most difficult bit in that change will be to pick good variable names, but @RyanGlScott and I can help with that.

I took a quick look and there are only uses of LambdaCase in copilot-theorem:

copilot-theorem/src/Copilot/Theorem/TransSys/Operators.hs:308:    numComp ta op = casting ta $ \case
copilot-theorem/src/Copilot/Theorem/What4.hs:416:            CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \case
copilot-theorem/src/Copilot/Theorem/What4.hs:420:            DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \case
copilot-theorem/src/Copilot/Theorem/What4.hs:426:            Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \case
copilot-theorem/src/Copilot/Theorem/What4.hs:430:            Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \case
copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs:332:    getVars' = \case
copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs:373:      entailment Base (modelInit ++ base) baseInv >>= \case
copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs:378:          else entailment Step step stepInv >>= \case
copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs:394:        else entailment Base (modelInit ++ base) (map (Op1 Bool Not) baseInv) >>= \case
copilot-theorem/src/Copilot/Theorem/Prover/SMT.hs:410:        else entailment Base (modelInit ++ base) baseInv >>= \case
copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs:49:expr = \case
copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs:70:showOp1 = \case
copilot-theorem/src/Copilot/Theorem/Prover/TPTP.hs:91:showOp2 = \case
copilot-theorem/src/Copilot/Theorem/IL/Transform.hs:18:    bsimpl' = \case
copilot-theorem/src/Copilot/Theorem/IL/Translate.hs:215:trOp1 = \case
copilot-theorem/src/Copilot/Theorem/IL/Translate.hs:240:trOp2 = \case
copilot-theorem/src/Copilot/Theorem/IL/Translate.hs:273:trType = \case
copilot-theorem/src/Copilot/Theorem/IL/Spec.hs:54:  show = \case

There's a few more in the Copilot.Theorem.Prover.Z3 module, which I'm not showing because that's considered dead code and will be removed in a future release.

Most of those are very easy or repetitive, so I'm hoping that this will not take too much of your time.

After those changes, in each module that used \case, we'd also want to remove LambdaCase from the list of language extensions supported, which is listed at the top of the file.

[ivanperez-keera]

And for future versions of Copilot (nothing that you need to think about at this stage), the extensions ViewPatterns and NamedFieldPuns are also suspect. I find very few uses, and nothing that is essential. In most cases, they almost do not save us any code.

There's a mention of PatternSynonyms that is not needed in copilot-theorem, and there's a use of TemplateHaskell (to get the git hash) that we can also remove. The use of the pattern NearEven from libBF also makes me cringe. It's used as an argument, so we could define nearEven :: RoundMode; nearEven = RoundMode 0 in our code as an internal, auxiliary definition, and be done (why libBF doesn't do that, I don't know; those should not be hard-coded constants in their code).

Also, not sure how I feel about ImplicitParams. It's only used in the verifier.

[ivanperez-keera]

Another one that we can remove:

copilot/copilot-verifier/copilot-verifier.cabal

Lines 40 to 41 in 9dc8f30

	default-extensions:
	NondecreasingIndentation

[ivanperez-keera]

Relevant discussion: #684

[ivanperez-keera]

@carte731 can you confirm if you can work on this for this release? Everything needs to be completed by Dec 21st.

[carte731]

Sorry about the delay, been trying to get caught up on work. Sounds good, always happy to contribute. I will start this weekend!

[ivanperez-keera]

Some more low-hanging fruit: #690

[ivanperez-keera]

@chathhorn-galois The discussion on planning is taking place here. We generally don't discuss planning or who will work on what in the issues themselves.