who2: Fix rol/ror bug, reinstate property tests

Author: langston-barrett

who2/src/Who2/Builder/Ops/BV.hs

@@ -1049,7 +1049,7 @@ bvRol alloc x y
   -- test: bvrol-const
   | Just (wx, bvx) <- asBVLit x
   , Just (_, bvy) <- asBVLit y =
-      bvLit alloc wx (BV.rotateL wx bvx (fromInteger (BV.asUnsigned bvy)))
+      bvLit alloc wx (BV.rotateL wx bvx (fromInteger (BV.asUnsigned bvy `mod` NR.intValue wx)))
   | otherwise = do
       let w = EBV.width x
       -- Cryptol> :prove \(x : [8]) -> x <<< 8 == x
@@ -1075,7 +1075,7 @@ bvRor alloc x y
   -- test: bvror-const
   | Just (wx, bvx) <- asBVLit x
   , Just (_, bvy) <- asBVLit y =
-      bvLit alloc wx (BV.rotateR wx bvx (fromInteger (BV.asUnsigned bvy)))
+      bvLit alloc wx (BV.rotateR wx bvx (fromInteger (BV.asUnsigned bvy `mod` NR.intValue wx)))
   | otherwise = do
       let w = EBV.width x
       -- Cryptol> :prove \(x : [8]) -> x >>> 8 == x

who2/test/Main.hs

@@ -116,16 +116,15 @@ hashConsedTests =
 simplificationCorrectnessTests :: TestTree
 simplificationCorrectnessTests =
   testGroup "Simplification Correctness"
-    [ -- TODO: These all fail :-(
-    -- [ testProperty "General simplifications (depth 5)" $
-    --     Hedgehog.withTests 32 Props.propSimplificationCorrect  -- TODO: increase
-    -- , testProperty "Deep expressions (depth 10)" $
-    --     Hedgehog.withTests 32 Props.propDeepSimplifications  -- TODO: increase
-    --   testProperty "Boolean-only expressions (100 tests)" $
-    --     Hedgehog.withTests 128 Props.propBoolSimplifications
-    -- , testProperty "BV arithmetic expressions (100 tests)" $
-    --     Hedgehog.withTests 128 Props.propBvArithSimplifications
-      testProperty "No variables reduces to literal" $
+    [ testProperty "General simplifications (depth 5)" $
+        Hedgehog.withTests 32 Props.propSimplificationCorrect  -- TODO: increase
+    , testProperty "Deep expressions (depth 10)" $
+        Hedgehog.withTests 32 Props.propDeepSimplifications  -- TODO: increase
+    , testProperty "Boolean-only expressions (100 tests)" $
+        Hedgehog.withTests 128 Props.propBoolSimplifications
+    , testProperty "BV arithmetic expressions (100 tests)" $
+        Hedgehog.withTests 128 Props.propBvArithSimplifications
+    , testProperty "No variables reduces to literal" $
         Hedgehog.withTests 1000 Props.propNoVariablesReducesToLiteral
     ]
 

who2/test/Who2/Builder/Simplification.hs

@@ -20,6 +20,7 @@ module Who2.Builder.Simplification
 
 import Control.Exception (catch, SomeException, evaluate)
 import Control.Monad.IO.Class (liftIO)
+import Data.List (isInfixOf)
 import qualified Data.Text as Text
 import qualified Data.Text.Lazy as Text.Lazy
 import qualified Data.Text.Lazy.Builder as Builder
@@ -29,6 +30,7 @@ import System.Process (readProcessWithExitCode)
 import System.Timeout (timeout)
 
 import Data.Parameterized.Nonce (withIONonceGenerator)
+import qualified Hedgehog as H
 import Hedgehog (Property, PropertyT, property, forAll, annotate, failure, assert)
 import qualified Hedgehog.Gen as Gen
 
@@ -106,25 +108,31 @@ checkSimplificationPreserved expr = do
   case result of
     (Right simpleRes, Right naiveRes) | simpleRes == naiveRes ->
       pure ()  -- Equisatisfiable
-    (Left "term rendering timeout", Left _) -> do
-      annotate "Skipped - naive term too large to render"
-      pure ()  -- Pass the test, don't fail on huge terms
     (Right simpleRes, Right naiveRes) -> do
       annotate $ "Expression: " ++ show expr
       annotate $ "Simplified result: " ++ Text.unpack simpleRes
       annotate $ "Naive result: " ++ Text.unpack naiveRes
       annotate "Results differ - not equisatisfiable"
       failure
-    (Left err, _) | "term rendering timeout" `elem` words err -> do
+    (Left "term rendering timeout", Left _) -> do
+      annotate "Skipped - naive term too large to render"
+      H.discard
+    (Left err, _) | "term rendering timeout" `isInfixOf` err -> do
+      annotate "Skipped - term too large to render"
+      H.discard
+    (Left err, _) | "z3 timeout" `isInfixOf` err -> do
+      annotate "Skipped - Z3 timeout (query too complex)"
+      H.discard
+    (_, Left err) | "term rendering timeout" `isInfixOf` err -> do
       annotate "Skipped - term too large to render"
-      pure ()  -- Pass the test
+      H.discard
+    (_, Left err) | "z3 timeout" `isInfixOf` err -> do
+      annotate "Skipped - Z3 timeout (query too complex)"
+      H.discard
     (Left err, _) -> do
       annotate $ "Expression: " ++ show expr
       annotate $ "Z3 error (simplified): " ++ err
       failure
-    (_, Left err) | "term rendering timeout" `elem` words err -> do
-      annotate "Skipped - term too large to render"
-      pure ()  -- Pass the test
     (_, Left err) -> do
       annotate $ "Expression: " ++ show expr
       annotate $ "Z3 error (naive): " ++ err

who2/test/Who2/Builder/TestBuilder.hs

@@ -14,6 +14,7 @@ module Who2.Builder.TestBuilder
 
 import Data.Parameterized.Nonce (NonceGenerator, Nonce)
 import qualified Data.Parameterized.Nonce as Nonce
+import Data.Parameterized.NatRepr (natValue)
 import qualified Data.BitVector.Sized as BVS
 
 import What4.BaseTypes (BaseBoolType)
@@ -33,6 +34,7 @@ import Who2.Expr.SymExpr (SymExpr(..))
 import qualified Who2.Builder.Ops.BV as BV
 import qualified Who2.Expr.BV as EBV
 import qualified Who2.Expr.Logic as EL
+import qualified Who2.Expr.Views as EV
 import qualified Who2.Expr.Bloom.Polarized as PBS
 import qualified Who2.Expr.Bloom.SemiRing.Product as SRP
 import qualified Who2.Expr.Bloom.SemiRing.Sum as SRS
@@ -282,13 +284,31 @@ instance IsExprBuilder (TestBuilder t) where
   bvRol tb x y = do
     let SymExpr ex = x
         SymExpr ey = y
-    result <- naiveAlloc tb (BVApp (EBV.BVRol (EBV.width ex) ex ey))
+        w = EBV.width ex
+    -- Normalize rotation amount modulo width (same as Builder)
+    -- But only if it's not already a literal < width
+    y' <- case EV.asBVLit ey of
+      Just (_, bv) | BVS.asUnsigned bv < toInteger (natValue w) -> pure y  -- Already normalized
+      _ -> do
+        widthLit <- bvLit tb w (BVS.mkBV w (toInteger (natValue w)))
+        bvUrem tb y widthLit
+    let SymExpr ey' = y'
+    result <- naiveAlloc tb (BVApp (EBV.BVRol w ex ey'))
     pure (SymExpr result)
 
   bvRor tb x y = do
     let SymExpr ex = x
         SymExpr ey = y
-    result <- naiveAlloc tb (BVApp (EBV.BVRor (EBV.width ex) ex ey))
+        w = EBV.width ex
+    -- Normalize rotation amount modulo width (same as Builder)
+    -- But only if it's not already a literal < width
+    y' <- case EV.asBVLit ey of
+      Just (_, bv) | BVS.asUnsigned bv < toInteger (natValue w) -> pure y  -- Already normalized
+      _ -> do
+        widthLit <- bvLit tb w (BVS.mkBV w (toInteger (natValue w)))
+        bvUrem tb y widthLit
+    let SymExpr ey' = y'
+    result <- naiveAlloc tb (BVApp (EBV.BVRor w ex ey'))
     pure (SymExpr result)
 
   bvConcat tb x y = do