Merge pull request #206 from lefterislazar/rocq-lemmas

Rocq Postcondition and Invariants

Author: lefterislazar

Makefile

@@ -60,7 +60,7 @@ hevm_multi_fast=$(filter-out $(hevm_multi_slow), $(hevm_multi_pass))
 failing_typing=tests/frontend/pass/dss/vat.act tests/frontend/pass/creation/createMultiple.act tests/frontend/pass/staticstore/staticstore.act
 
 
-coq-examples = tests/coq/transitions tests/coq/safemath tests/coq/exponent tests/coq/token tests/coq/ERC20-simple tests/coq/ERC20 tests/coq/multi
+coq-examples = tests/coq/transitions tests/coq/safemath tests/coq/exponent tests/coq/token tests/coq/ERC20-simple tests/coq/ERC20 tests/coq/multi tests/coq/amm
 
 .PHONY: test-coq $(coq-examples)
 test-coq: compiler $(coq-examples)

src/Act/Bounds.hs

@@ -35,7 +35,7 @@ addBoundsConstructor ctor@(Constructor _ (Interface _ decls) _ pre post invs sta
        , _cpostconditions = post'
        , _invariants = invs' }
     where
-      pre' = pre
+      pre' = nub $ pre
              <> mkCallDataBounds decls
              <> mkEthEnvBounds (ethEnvFromConstructor ctor)
               -- The following is sound as values of locations outside local storage
@@ -55,7 +55,7 @@ addBoundsBehaviour :: Behaviour -> Behaviour
 addBoundsBehaviour behv@(Behaviour _ _ (Interface _ decls) _ pre cases post stateUpdates ret) =
   behv { _preconditions = pre', _postconditions = post' }
     where
-      pre' = pre
+      pre' = nub $ pre
              <> mkCallDataBounds decls
              <> mkStorageBounds stateUpdates Pre
              <> mkLocationBounds locs
@@ -72,14 +72,14 @@ addBoundsInvariant :: Constructor -> Invariant -> Invariant
 addBoundsInvariant (Constructor _ (Interface _ decls) _ _ _ _ _) inv@(Invariant _ preconds storagebounds (PredTimed predicate _)) =
   inv { _ipreconditions = preconds', _istoragebounds = storagebounds' }
     where
-      preconds' = preconds
+      preconds' = nub $ preconds
                   <> mkCallDataBounds decls
                   <> mkEthEnvBounds (ethEnvFromExp predicate)
                   <> mkLocationBounds nonlocalLocs
       storagebounds' = storagebounds
                        <> mkLocationBounds localLocs
 
-      locs = concatMap locsFromExp (preconds <> storagebounds)
+      locs = nub $ concatMap locsFromExp (preconds <> storagebounds)
              <> locsFromExp predicate
       (nonlocalLocs, localLocs) = partition (not . isLocalLoc) locs
 

src/Act/CLI.hs

@@ -47,7 +47,7 @@ import Act.Syntax.TypedExplicit hiding (_Array)
 import Act.Bounds
 import Act.SMT as SMT
 import Act.Type
-import Act.Coq hiding (indent)
+import Act.Coq hiding (indent, (<+>))
 import Act.HEVM
 import Act.HEVM_utils
 import Act.Consistency