rme (empty) → 0.1

raw patch · 6 files changed

+609/−0 lines, 6 filesdep +basedep +containersdep +vector

Dependencies added: base, containers, vector

Files

CHANGELOG.md +5/−0
LICENSE +30/−0
rme.cabal +37/−0
src/Data/RME.hs +18/−0
src/Data/RME/Base.hs +184/−0
src/Data/RME/Vector.hs +335/−0

+ CHANGELOG.md view

@@ -0,0 +1,5 @@+# Revision history for rme++## 0.1 -- TBA++* First version.

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2012-2025 Galois, Inc.+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++  * Redistributions of source code must retain the above copyright+    notice, this list of conditions and the following disclaimer.++  * Redistributions in binary form must reproduce the above copyright+    notice, this list of conditions and the following disclaimer in+    the documentation and/or other materials provided with the+    distribution.++  * Neither the name of Galois, Inc. nor the names of its contributors+    may be used to endorse or promote products derived from this+    software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ rme.cabal view

@@ -0,0 +1,37 @@+Cabal-version:      3.0+Name:               rme+Version:            0.1+Author:             Galois, Inc.+Maintainer:         huffman@galois.com+Build-type:         Simple+License:            BSD-3-Clause+extra-doc-files:    CHANGELOG.md+License-file:       LICENSE+Copyright:          (c) 2016-2025 Galois Inc.+Category:           Formal Methods+Synopsis:           Reed-Muller Expansion normal form for Boolean Formulas+Description:+  A representation of the Algebraic Normal Form of boolean formulas+  using the Reed-Muller Expansion.++source-repository head+  type:     git+  location: https://github.com/GaloisInc/rme+  subdir:   rme++library+  default-language: Haskell2010++  build-depends:+    -- upstream packages from hackage+    base == 4.*,+    containers,+    vector++  hs-source-dirs: src+  exposed-modules:+    Data.RME+    Data.RME.Base+    Data.RME.Vector++  ghc-options: -O2 -Wall -Wcompat -fno-ignore-asserts -fno-spec-constr-count

+ src/Data/RME.hs view

@@ -0,0 +1,18 @@+{- |+Module      : Data.RME+Copyright   : Galois, Inc. 2016+License     : BSD3+Maintainer  : huffman@galois.com+Stability   : experimental+Portability : portable++Reed-Muller Expansion normal form for Boolean Formulas.+-}++module Data.RME+  ( module Data.RME.Base+  , module Data.RME.Vector+  ) where++import Data.RME.Base+import Data.RME.Vector

+ src/Data/RME/Base.hs view

@@ -0,0 +1,184 @@+{- |+Module      : Data.RME.Base+Copyright   : Galois, Inc. 2016+License     : BSD3+Maintainer  : huffman@galois.com+Stability   : experimental+Portability : portable++Reed-Muller Expansion normal form for Boolean Formulas.+-}++module Data.RME.Base+  ( RME+  , true, false, lit+  , constant, isBool+  , compl, xor, conj, disj, iff, mux+  , eval+  , sat, allsat+  , degree+  , depth, size+  , explode+  ) where++-- | Boolean formulas in Algebraic Normal Form, using a representation+-- based on the Reed-Muller expansion.++-- Invariants: The last argument to a `Node` constructor should never+-- be `R0`. Also the `Int` arguments should strictly increase as you+-- go deeper in the tree.++data RME = Node !Int !RME !RME | R0 | R1+  deriving (Eq, Show)++-- | Evaluate formula with given variable assignment.+eval :: RME -> (Int -> Bool) -> Bool+eval anf v =+  case anf of+    R0 -> False+    R1 -> True+    Node n a b -> (eval a v) /= (v n && eval b v)++-- | Normalizing constructor.+node :: Int -> RME -> RME -> RME+node _ a R0 = a+node n a b = Node n a b++-- | Constant true formula.+true :: RME+true = R1++-- | Constant false formula.+false :: RME+false = R0++-- | Boolean constant formulas.+constant :: Bool -> RME+constant False = false+constant True = true++-- | Test whether an RME formula is a constant boolean.+isBool :: RME -> Maybe Bool+isBool R0 = Just False+isBool R1 = Just True+isBool _ = Nothing++-- | Boolean literals.+lit :: Int -> RME+lit n = Node n R0 R1++-- | Logical complement.+compl :: RME -> RME+compl R0 = R1+compl R1 = R0+compl (Node n a b) = Node n (compl a) b++-- | Logical exclusive-or.+xor :: RME -> RME -> RME+xor R0 y = y+xor R1 y = compl y+xor x R0 = x+xor x R1 = compl x+xor x@(Node i a b) y@(Node j c d)+  | i < j = Node i (xor a y) b+  | j < i = Node j (xor x c) d+  | otherwise = node i (xor a c) (xor b d)++-- | Logical conjunction.+conj :: RME -> RME -> RME+conj R0 _ = R0+conj R1 y = y+conj _ R0 = R0+conj x R1 = x+conj x@(Node i a b) y@(Node j c d)+  | i < j = node i (conj a y) (conj b y)+  | j < i = node j (conj x c) (conj x d)+  | otherwise = node i ac (xor ac (conj (xor a b) (xor c d)))+  where ac = conj a c++-- | Logical disjunction.+disj :: RME -> RME -> RME+disj R0 y = y+disj R1 _ = R1+disj x R0 = x+disj _ R1 = R1+disj x@(Node i a b) y@(Node j c d)+  | i < j = node i (disj a y) (conj b (compl y))+  | j < i = node j (disj x c) (conj (compl x) d)+  | otherwise = node i ac (xor ac (disj (xor a b) (xor c d)))+  where ac = disj a c++-- | Logical equivalence.+iff :: RME -> RME -> RME+iff x y = xor (compl x) y+{-+iff R0 y = compl y+iff R1 y = y+iff x R0 = compl x+iff x R1 = x+iff x@(Node i a b) y@(Node j c d)+  | i < j = Node i (iff a y) b+  | j < i = Node j (iff x c) d+  | otherwise = node i (iff a c) (xor b d)+-}++-- | Logical if-then-else.+mux :: RME -> RME -> RME -> RME+--mux w x y = xor (conj w x) (conj (compl w) y)+mux R0 _ y = y+mux R1 x _ = x+mux b x y = xor (conj b (xor x y)) y++{-+mux R0 x y = y+mux R1 x y = x+mux w R0 y = conj (compl w) y+mux w R1 y = disj w y+mux w x R0 = conj w x+mux w x R1 = disj (compl w) x+mux w@(Node i a b) x@(Node j c d) y@(Node k e f)+  | i < j && i < k = node i (mux a x y) (conj b (xor x y))+  | j < i && j < k = node i (mux w c y) (conj w d)+  | k < i && k < j = node i (mux w x e) (conj (compl w) f)+  | i == j && i < k = node i (mux a c y) _+-}++-- | Satisfiability checker.+sat :: RME -> Maybe [(Int, Bool)]+sat R0 = Nothing+sat R1 = Just []+sat (Node n a b) =+  case sat a of+    Just xs -> Just ((n, False) : xs)+    Nothing -> fmap ((n, True) :) (sat b)++-- | List of all satisfying assignments.+allsat :: RME -> [[(Int, Bool)]]+allsat R0 = []+allsat R1 = [[]]+allsat (Node n a b) =+  map ((n, False) :) (allsat a) ++ map ((n, True) :) (allsat (xor a b))++-- | Maximum polynomial degree.+degree :: RME -> Int+degree R0 = 0+degree R1 = 0+degree (Node _ a b) = max (degree a) (1 + degree b)++-- | Tree depth.+depth :: RME -> Int+depth R0 = 0+depth R1 = 0+depth (Node _ a b) = 1 + max (depth a) (depth b)++-- | Tree size.+size :: RME -> Int+size R0 = 1+size R1 = 1+size (Node _ a b) = 1 + size a + size b++-- | Convert to an explicit polynomial representation.+explode :: RME -> [[Int]]+explode R0 = []+explode R1 = [[]]+explode (Node i a b) = explode a ++ map (i:) (explode b)

+ src/Data/RME/Vector.hs view

@@ -0,0 +1,335 @@+{-# LANGUAGE BangPatterns, BlockArguments #-}+{- |+Module      : Data.RME.Vector+Copyright   : Galois, Inc. 2016+License     : BSD3+Maintainer  : huffman@galois.com+Stability   : experimental+Portability : portable++Operations on big-endian vectors of RME formulas.+-}++module Data.RME.Vector+  ( RMEV+  , eq, ule, ult, sle, slt+  , neg, add, sub, mul+  , udiv, urem, sdiv, srem+  , pmul, pmod, pdiv+  , shl, ashr, lshr, ror, rol+  , integer+  , popcount+  , countLeadingZeros+  , countTrailingZeros+  ) where++import Data.RME.Base (RME)+import qualified Data.RME.Base as RME++import qualified Data.Bits as Bits+import Data.Vector (Vector)+import qualified Data.Vector as V++type RMEV = Vector RME++-- | Constant integer literals.+integer :: Int -> Integer -> RMEV+integer width x = V.reverse (V.generate width (RME.constant . Bits.testBit x))++-- | Bitvector equality.+eq :: RMEV -> RMEV -> RME+eq x y = V.foldr RME.conj RME.true (V.zipWith RME.iff x y)++-- | Unsigned less-than-or-equal.+ule :: RMEV -> RMEV -> RME+ule xv yv = go (V.toList xv) (V.toList yv)+  where+    go (x : xs) (y : ys) =+      let z = go xs ys+      in RME.xor (RME.conj y z) (RME.conj (RME.compl x) (RME.xor y z))+    go _ _ = RME.true++-- | Unsigned less-than.+ult :: RMEV -> RMEV -> RME+ult x y = RME.compl (ule y x)++swap_sign :: RMEV -> RMEV+swap_sign x+  | V.null x = x+  | otherwise = V.singleton (RME.compl (V.head x)) V.++ V.tail x++-- | Signed less-than-or-equal.+sle :: RMEV -> RMEV -> RME+sle x y = ule (swap_sign x) (swap_sign y)++-- | Signed less-than.+slt :: RMEV -> RMEV -> RME+slt x y = ult (swap_sign x) (swap_sign y)++-- | Big-endian bitvector increment with carry.+increment :: [RME] -> (RME, [RME])+increment [] = (RME.true, [])+increment (x : xs) = (RME.conj x c, RME.xor x c : ys)+  where (c, ys) = increment xs++-- | Two's complement bitvector negation.+neg :: RMEV -> RMEV+neg x = V.fromList (snd (increment (map RME.compl (V.toList x))))++-- | 1-bit full adder.+full_adder :: RME -> RME -> RME -> (RME, RME)+full_adder a b c = (carry, RME.xor (RME.xor a b) c)+  where carry = RME.xor (RME.conj a b) (RME.conj (RME.xor a b) c)++-- | Big-endian ripple-carry adder.+ripple_carry_adder :: [RME] -> [RME] -> RME -> (RME, [RME])+ripple_carry_adder [] _ c = (c, [])+ripple_carry_adder _ [] c = (c, [])+ripple_carry_adder (x : xs) (y : ys) c = (c'', z : zs)+  where (c', zs) = ripple_carry_adder xs ys c+        (c'', z) = full_adder x y c'++-- | Two's complement bitvector addition.+add :: RMEV -> RMEV -> RMEV+add x y =+  V.fromList (snd (ripple_carry_adder (V.toList x) (V.toList y) RME.false))++-- | Two's complement bitvector subtraction.+sub :: RMEV -> RMEV -> RMEV+sub x y =+  V.fromList (snd (ripple_carry_adder (V.toList x) (map RME.compl (V.toList y)) RME.true))++-- | Two's complement bitvector multiplication.+mul :: RMEV -> RMEV -> RMEV+mul x y = V.foldl f zero y+  where+    zero = V.replicate (V.length x) RME.false+    f acc c = V.zipWith (RME.mux c) (add acc2 x) acc2+      where acc2 = V.drop 1 (acc V.++ V.singleton RME.false)++-- | Unsigned bitvector division.+udiv :: RMEV -> RMEV -> RMEV+udiv x y = fst (udivrem x y)++-- | Unsigned bitvector remainder.+urem :: RMEV -> RMEV -> RMEV+urem x y = snd (udivrem x y)++-- | Signed bitvector division.+sdiv :: RMEV -> RMEV -> RMEV+sdiv x y = fst (sdivrem x y)++-- | Signed bitvector remainder.+srem :: RMEV -> RMEV -> RMEV+srem x y = snd (sdivrem x y)++udivrem :: RMEV -> RMEV -> (RMEV, RMEV)+udivrem dividend divisor = divStep 0 RME.false initial+  where+    n :: Int+    n = V.length dividend++    -- Given an n-bit dividend and divisor, 'initial' is the starting value of+    -- the 2n-bit "remainder register" that carries both the quotient and remainder;+    initial :: RMEV+    initial = integer n 0 V.++ dividend++    divStep :: Int -> RME -> RMEV -> (RMEV, RMEV)+    divStep i p rr | i == n = (q `shiftL1` p, r)+      where (r, q) = V.splitAt n rr+    divStep i p rr = divStep (i+1) b (V.zipWith (RME.mux b) (V.fromList s V.++ q) rs)+      where rs = rr `shiftL1` p+            (r, q) = V.splitAt n rs+            -- Subtract the divisor from the left half of the "remainder register"+            (b, s) = ripple_carry_adder (V.toList r) (map RME.compl (V.toList divisor)) RME.true++    shiftL1 :: RMEV -> RME -> RMEV+    shiftL1 v e = V.tail v `V.snoc` e++-- Perform udivrem on the absolute value of the operands.  Then, negate the+-- quotient if the signs of the operands differ and make the sign of a nonzero+-- remainder to match that of the dividend.+sdivrem :: RMEV -> RMEV -> (RMEV, RMEV)+sdivrem dividend divisor = (q',r')+  where+    sign1 = V.head dividend+    sign2 = V.head divisor+    signXor = RME.xor sign1 sign2+    negWhen x c = V.zipWith (RME.mux c) (neg x) x+    dividend' = negWhen dividend sign1+    divisor' = negWhen divisor sign2+    (q, r) = udivrem dividend' divisor'+    q' = negWhen q signXor+    r' = negWhen r sign1++popcount :: RMEV -> RMEV+popcount bits = if l == 0 then V.empty else (V.replicate (l-w-1) RME.false) <> pcnt+  where+    l = V.length bits+    w = Bits.countTrailingZeros l -- log_2 rounded down, w+1 is enough bits to hold popcount+    zs = V.replicate w RME.false++    pcnt = foldr1 add xs -- length is w+1+    xs = [ zs <> V.singleton b | b <- V.toList bits ]++countTrailingZeros :: RMEV -> RMEV+countTrailingZeros bits = countLeadingZeros (V.reverse bits)++-- Big endian convention means its easier to count leading zeros+countLeadingZeros :: RMEV -> RMEV+countLeadingZeros bits = if l == 0 then V.empty else (V.replicate (l-w-1) RME.false) <> (go 0 (V.toList bits))+  where+    l = V.length bits+    w = Bits.countTrailingZeros l -- log_2 rounded down, w+1 is enough bits to hold count++    go :: Integer -> [RME] -> Vector RME+    go !i []      = integer (w+1) i+    go !i (b:bs)  = V.zipWith (RME.mux b) (integer (w+1) i) (go (i+1) bs)++-- | Polynomial multiplication. Note that the algorithm works the same+-- no matter which endianness convention is used. Result length is+-- @max 0 (m+n-1)@, where @m@ and @n@ are the lengths of the inputs.+pmul :: RMEV -> RMEV -> RMEV+pmul x y = V.generate (max 0 (m + n - 1)) coeff+  where+    m = V.length x+    n = V.length y+    coeff k = foldr RME.xor RME.false+      [ RME.conj (x V.! i) (y V.! j) | i <- [0 .. k], let j = k - i, i < m, j < n ]++-- | Polynomial mod with symbolic modulus. Return value has length one+-- less than the length of the modulus.+-- This implementation is optimized for the (common) case where the modulus+-- is concrete.+pmod :: RMEV -> RMEV -> RMEV+pmod x y = findmsb (V.toList y)+  where+    findmsb :: [RME] -> RMEV+    findmsb [] = V.replicate (V.length y - 1) RME.false -- division by zero+    findmsb (c : cs)+      | c == RME.true = usemask cs+      | c == RME.false = findmsb cs+      | otherwise = V.zipWith (RME.mux c) (usemask cs) (findmsb cs)++    usemask :: [RME] -> RMEV+    usemask m = zext (V.fromList (go (V.length x - 1) p0 z0)) (V.length y - 1)+      where+        zext v r = V.replicate (r - V.length v) RME.false V.++ v+        msize = length m+        p0 = replicate (msize - 1) RME.false ++ [RME.true]+        z0 = replicate msize RME.false++        next :: [RME] -> [RME]+        next [] = []+        next (b : bs) =+          let m' = map (RME.conj b) m+              bs' = bs ++ [RME.false]+          in zipWith RME.xor m' bs'++        go :: Int -> [RME] -> [RME] -> [RME]+        go i p acc+          | i < 0 = acc+          | otherwise =+              let px = map (RME.conj (x V.! i)) p+                  acc' = zipWith RME.xor px acc+                  p' = next p+              in go (i-1) p' acc'++-- | Polynomial division. Return value has length+--   equal to the first argument.+pdiv :: RMEV -> RMEV -> RMEV+pdiv x y = fst (pdivmod x y)++-- Polynomial div/mod: resulting lengths are as in Cryptol.++-- TODO: probably this function should be disentangled to only compute+-- division, given that we have a separate polynomial modulus algorithm.+pdivmod :: RMEV -> RMEV -> (RMEV, RMEV)+pdivmod x y = findmsb (V.toList y)+  where+    findmsb :: [RME] -> (RMEV, RMEV)+    findmsb (c : cs) = muxPair c (usemask cs) (findmsb cs)+    findmsb [] = (x, V.replicate (V.length y - 1) RME.false) -- division by zero++    usemask :: [RME] -> (RMEV, RMEV)+    usemask mask = (q, r)+      where+        (qs, rs) = pdivmod_helper (V.toList x) mask+        z = RME.false+        qs' = map (const z) rs ++ qs+        rs' = replicate (V.length y - 1 - length rs) z ++ rs+        q = V.fromList qs'+        r = V.fromList rs'++    muxPair :: RME -> (RMEV, RMEV) -> (RMEV, RMEV) -> (RMEV, RMEV)+    muxPair c a b+      | c == RME.true = a+      | c == RME.false = b+      | otherwise = (V.zipWith (RME.mux c) (fst a) (fst b), V.zipWith (RME.mux c) (snd a) (snd b))++-- Divide ds by (1 : mask), giving quotient and remainder. All+-- arguments and results are big-endian. Remainder has the same length+-- as mask (but limited by length ds); total length of quotient +++-- remainder = length ds.+pdivmod_helper :: [RME] -> [RME] -> ([RME], [RME])+pdivmod_helper ds mask = go (length ds - length mask) ds+  where+    go :: Int -> [RME] -> ([RME], [RME])+    go n cs | n <= 0 = ([], cs)+    go _ []          = error "Data.AIG.Operations.pdiv: impossible"+    go n (c : cs)    = (c : qs, rs)+      where cs' = mux_add c cs mask+            (qs, rs) = go (n - 1) cs'++    mux_add :: RME -> [RME] -> [RME] -> [RME]+    mux_add c (x : xs) (y : ys) = RME.mux c (RME.xor x y) x : mux_add c xs ys+    mux_add _ []       (_ : _ ) = error "pdiv: impossible"+    mux_add _ xs       []       = xs++-- | Helper for building shift and rotate operations.+-- The callback function is called with: the first argument,+-- the index being filled in the result, and the arithmetic+-- value of the second argument.+bitOp :: (RMEV -> Integer -> Integer -> RME) -> RMEV -> RMEV -> RMEV+bitOp f x y = V.generate w \i -> pick (toInteger i) 0 y'+  where+    y' = V.toList y+    w = length x+    pick i j [] = f x i j+    pick i j (b:bs) = RME.mux b (pick i (1+2*j) bs) (pick i (2*j) bs)++-- | Bitwise logical left shift. Shifts the bits in the first bit-vector+-- by the unsigned, arithmetic value in the second bit-vector filling+-- in with false bits.+shl :: RMEV -> RMEV -> RMEV+shl = bitOp \x i j ->+  let w = length x in +  if i + j >= toInteger w then RME.false else x V.! fromInteger (i+j)++-- | Arithmetic logical right shift. Shifts the bits in the first bit-vector+-- by the unsigned, arithmetic value in the second bit-vector filling+-- in with bits matching the first bit (which is treated as a sign bit).+ashr :: RMEV -> RMEV -> RMEV+ashr = bitOp \x i j ->+  if i < j then V.head x else x V.! fromInteger (i-j)++-- | Bitwise logical right shift. Shifts the bits in the first bit-vector+-- by the unsigned, arithmetic value in the second bit-vector filling+-- in with false bits.+lshr :: RMEV -> RMEV -> RMEV+lshr = bitOp \x i j ->+  if i < j then RME.false else x V.! fromInteger (i-j)++-- | Bitwise left rotation. Rotates the bits in the first bit-vector+-- by the unsigned, arithmetic value in the second bit-vector.+rol :: RMEV -> RMEV -> RMEV+rol = bitOp \x i j ->+  let w = length x in+  x V.! fromInteger ((i + j) `mod` toInteger w)++-- | Bitwise right rotation. Rotates the bits in the first bit-vector+-- by the unsigned, arithmetic value in the second bit-vector.+ror :: RMEV -> RMEV -> RMEV+ror = bitOp \x i j ->+  let w = length x in+  x V.! fromInteger ((i - j) `mod` toInteger w)