Bump copilot submodule to 3.18.1

`copilot-language-3.18` deprecates the `forall` function in favor of `forAll`, so also update any uses of the former to the latter.
Copilot-Language · Jan 8, 2024 · b399ebc · b399ebc
1 parent 75a7c06
commit b399ebc
Show file tree

Hide file tree

Showing 17 changed files with 31 additions and 31 deletions.
diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal
@@ -28,13 +28,13 @@ common bldflags
     bv-sized >= 1.0.0 && < 1.1,
     bytestring,
     containers >= 0.5.9.0,
-    copilot >= 3.17,
-    copilot-c99 >= 3.17,
-    copilot-core >= 3.17,
-    copilot-libraries >= 3.17,
-    copilot-language >= 3.17,
-    copilot-prettyprinter >= 3.17,
-    copilot-theorem >= 3.17,
+    copilot >= 3.18,
+    copilot-c99 >= 3.18,
+    copilot-core >= 3.18,
+    copilot-libraries >= 3.18,
+    copilot-language >= 3.18,
+    copilot-prettyprinter >= 3.18,
+    copilot-theorem >= 3.18,
     crucible,
     crucible-llvm,
     crux,

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs
@@ -15,7 +15,7 @@ spec = do
   let stream :: Stream Int32
       stream = extern "stream" Nothing
 
-  _ <- prop "notIntMin" (forall (stream > constI32 minBound))
+  _ <- prop "notIntMin" (forAll (stream > constI32 minBound))
   trigger "streamAbs" (abs stream == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs
@@ -14,7 +14,7 @@ spec = do
   let stream :: Stream Int32
       stream = extern "stream" Nothing
 
-  _ <- prop "notIntMax" (forall (stream < constI32 maxBound))
+  _ <- prop "notIntMax" (forAll (stream < constI32 maxBound))
   trigger "streamAddSigned" ((stream + 1) == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs
@@ -14,7 +14,7 @@ spec = do
   let stream :: Stream Int16
       stream = extern "stream" Nothing
 
-  _ <- prop "nonzero" (forall (stream /= 0))
+  _ <- prop "nonzero" (forAll (stream /= 0))
   trigger "streamDiv" ((stream `div` stream) == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs
@@ -18,7 +18,7 @@ spec = do
       stream2 :: Stream Word32
       stream2 = extern "stream2" Nothing
 
-  _ <- prop "withinBounds" (forall (stream2 < constW32 2))
+  _ <- prop "withinBounds" (forAll (stream2 < constW32 2))
   trigger "streamIndex" ((stream1 .!! stream2) == 1) [arg stream1, arg stream2]
 
 verifySpec :: Verbosity -> IO ()

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs
@@ -14,7 +14,7 @@ spec = do
   let stream :: Stream Int16
       stream = extern "stream" Nothing
 
-  _ <- prop "nonzero" (forall (stream /= 0))
+  _ <- prop "nonzero" (forAll (stream /= 0))
   trigger "streamMod" ((stream `mod` stream) == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs
@@ -16,7 +16,7 @@ spec = do
   let stream :: Stream Int32
       stream = extern "stream" Nothing
 
-  _ <- prop "withinRange" (forall
+  _ <- prop "withinRange" (forAll
            (constI32 ((minBound P.+ 1) P.* 2) < stream
          && stream < constI32 ((maxBound P.- 1) `P.div` 2)))
   trigger "streamMulSigned" ((stream * 2) == 2) [arg stream]

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs
@@ -18,7 +18,7 @@ spec = do
       stream2 :: Stream Int64
       stream2 = extern "stream2" Nothing
 
-  _ <- prop "lessThanBitWidth" (forall
+  _ <- prop "lessThanBitWidth" (forAll
          (constI64 0 <= stream2 && stream2 < constI64 32))
   trigger "streamShiftL" ((stream1 .<<. stream2) == 1) [arg stream1, arg stream2]
 

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs
@@ -18,7 +18,7 @@ spec = do
       stream2 :: Stream Int64
       stream2 = extern "stream2" Nothing
 
-  _ <- prop "lessThanBitWidth" (forall
+  _ <- prop "lessThanBitWidth" (forAll
          (constI64 0 <= stream2 && stream2 < constI64 32))
   trigger "streamShiftR" ((stream1 .<<. stream2) == 1) [arg stream1, arg stream2]
 

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs
@@ -14,7 +14,7 @@ spec = do
   let stream :: Stream Int32
       stream = extern "stream" Nothing
 
-  _ <- prop "notIntMin" (forall (stream > constI32 minBound))
+  _ <- prop "notIntMin" (forAll (stream > constI32 minBound))
   trigger "streamSubSigned" ((stream - 1) == 1) [arg stream]
 
 verifySpec :: Verbosity -> IO ()

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs
@@ -19,9 +19,9 @@ lastPrime = 31
 
 multRingSpec :: Spec
 multRingSpec = do
-  _ <- prop "clamp nonzero" (forall ((clamp > 0) && (clamp < lastPrime)))
-  _ <- prop "reduced" (forall (acc < lastPrime))
-  _ <- prop "nonzero" (forall (acc > 0 && (acc < lastPrime)))
+  _ <- prop "clamp nonzero" (forAll ((clamp > 0) && (clamp < lastPrime)))
+  _ <- prop "reduced" (forAll (acc < lastPrime))
+  _ <- prop "nonzero" (forAll (acc > 0 && (acc < lastPrime)))
 
   trigger "outofrange" (not (acc > 0 && acc < lastPrime)) [arg acc]
 

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs
@@ -31,8 +31,8 @@ spec :: Spec
 spec = do
   observer "clk"  clkStream
   observer "clk'" clkStream'
-  _ <- prop "clksPhase" (forall (clkStream == drop 2 clkStream'))
-  _ <- prop "clksDistinct" (forall (not (clkStream && clkStream')))
+  _ <- prop "clksPhase" (forAll (clkStream == drop 2 clkStream'))
+  _ <- prop "clksDistinct" (forAll (not (clkStream && clkStream')))
   trigger "clksHigh" (clkStream && clkStream') []
 
 

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs
@@ -38,9 +38,9 @@ bytecounter2 = counter true ([False] ++ bytecounter2 == 255)
 
 spec :: Spec
 spec =
-  do _ <- prop "range" (forall (bytecounter == unsafeCast (resetcounter `mod` 256)))
-     _ <- prop "range2" (forall (0 <= bytecounter2 && bytecounter2 <= 255))
-     _ <- prop "same"  (forall ((0 <= bytecounter2 && bytecounter2 <= 255) &&
+  do _ <- prop "range" (forAll (bytecounter == unsafeCast (resetcounter `mod` 256)))
+     _ <- prop "range2" (forAll (0 <= bytecounter2 && bytecounter2 <= 255))
+     _ <- prop "same"  (forAll ((0 <= bytecounter2 && bytecounter2 <= 255) &&
                                 (bytecounter == unsafeCast (resetcounter `mod` 256)) &&
                                 (bytecounter == bytecounter2)))
      trigger "counter" true [arg $ bytecounter, arg $ bytecounter2]

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs
@@ -15,8 +15,8 @@ spec = do
       shiftBy :: Stream Int16
       shiftBy = extern "shiftBy" Nothing
 
-  _ <- prop "nonzero" (forall (stream /= 0))
-  _ <- prop "shiftByBits" (forall (0 <= shiftBy && shiftBy < 16))
+  _ <- prop "nonzero" (forAll (stream /= 0))
+  _ <- prop "shiftByBits" (forAll (0 <= shiftBy && shiftBy < 16))
 
   triggerOp1 "abs" abs stream
   triggerOp1 "signum" signum stream

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs
@@ -60,12 +60,12 @@ spec = do
 
   -- Check equality, indexing into nested structs and arrays. Note that this is
   -- trivial by equality.
-  void $ prop "Example 1" $ forall $
+  void $ prop "Example 1" $ forAll $
     (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts)
 
   -- Same as previous example, but get a different array index (so should be
   -- false).
-  void $ prop "Example 2" $ forall $
+  void $ prop "Example 2" $ forAll $
     (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)
 
   -- Same as previous example, but in trigger form

diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs
@@ -170,8 +170,8 @@ horizontalWCV tvar s v =
   (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr))
 
 spec = do
-  Monad.void $ prop "1a" (forall $ (tau s v) ~= (tau (neg s) (neg v)))
-  -- Monad.void $ prop "3d" (forall $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
+  Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))
+  -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))
   trigger "well_clear_violation" (wcv tep s sz v vz) []
 
 verifySpec :: Verbosity -> IO ()

diff --git a/deps/copilot b/deps/copilot
+22 −2		.travis.yml
+10 −0		copilot-c99/CHANGELOG
+4 −4		copilot-c99/copilot-c99.cabal
+40 −33		copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
+15 −4		copilot-c99/src/Copilot/Compile/C99/Compile.hs
+33 −9		copilot-c99/tests/Test/Copilot/Compile/C99.hs
+6 −0		copilot-core/CHANGELOG
+1 −1		copilot-core/copilot-core.cabal
+6 −0		copilot-interpreter/CHANGELOG
+2 −2		copilot-interpreter/copilot-interpreter.cabal
+8 −0		copilot-language/CHANGELOG
+4 −4		copilot-language/copilot-language.cabal
+1 −0		copilot-language/src/Copilot/Language.hs
+7 −1		copilot-language/src/Copilot/Language/Spec.hs
+6 −2		copilot-language/tests/Test/Copilot/Language/Reify.hs
+8 −0		copilot-libraries/CHANGELOG
+33 −2		copilot-libraries/copilot-libraries.cabal
+18 −0		copilot-libraries/tests/Main.hs
+72 −0		copilot-libraries/tests/Test/Copilot/Library/PTLTL.hs
+556 −0		copilot-libraries/tests/Test/Extra.hs
+6 −0		copilot-prettyprinter/CHANGELOG
+2 −2		copilot-prettyprinter/copilot-prettyprinter.cabal
+9 −0		copilot-theorem/CHANGELOG
+31 −3		copilot-theorem/copilot-theorem.cabal
+3 −3		copilot-theorem/examples/BoyerMoore.hs
+2 −2		copilot-theorem/examples/Grey.hs
+3 −3		copilot-theorem/examples/Incr.hs
+2 −2		copilot-theorem/examples/SerialBoyerMoore.hs
+18 −18		copilot-theorem/examples/SphericalWCV.hs
+15 −15		copilot-theorem/examples/Trig.hs
+18 −18		copilot-theorem/examples/WCV.hs
+1 −0		copilot-theorem/src/Copilot/Theorem/IL/Translate.hs
+1 −1		copilot-theorem/src/Copilot/Theorem/Misc/Utils.hs
+1 −0		copilot-theorem/src/Copilot/Theorem/Prove.hs
+1 −0		copilot-theorem/src/Copilot/Theorem/TransSys/Translate.hs
+1 −0		copilot-theorem/src/Copilot/Theorem/What4.hs
+18 −0		copilot-theorem/tests/Main.hs
+108 −0		copilot-theorem/tests/Test/Copilot/Theorem/What4.hs
+12 −0		copilot/CHANGELOG
+2 −2		copilot/README.md
+8 −8		copilot/copilot.cabal
+2 −2		copilot/examples/WCV.hs
+6 −6		copilot/examples/what4/Arithmetic.hs
+7 −7		copilot/examples/what4/Propositional.hs
+2 −2		copilot/examples/what4/Structs.hs