From 5a8f2fd24167b0609cb0d8986e578bb43c71072c Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Thu, 26 Jan 2023 18:10:28 -0800
Subject: [PATCH 1/4] added axioms about one-step unfoldings of foldl and
 foldr; fixed the rewriter to be able to rewrite with these axioms by allowing
 patterns of the form Succ x to match nat literals

---
 .../CryptolToCoq/SAWCoreVectorsAsCoqVectors.v | 31 +++++++++++++++++++
 .../SAW/Translation/Coq/SpecialTreatment.hs   |  6 ++++
 saw-core/prelude/Prelude.sawcore              | 16 ++++++++++
 saw-core/src/Verifier/SAW/Rewriter.hs         | 15 ++++++---
 4 files changed, 63 insertions(+), 5 deletions(-)

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
index 7a03a6fb7b..340cc95a42 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
@@ -68,6 +68,9 @@ Fixpoint gen (n : nat) (a : Type) (f : nat -> a) {struct n} : Vec n a.
     ).
 Defined.
 
+Definition head (n : nat) (a : Type) (v : Vec (S n) a) : a := hd v.
+Definition tail (n : nat) (a : Type) (v : Vec (S n) a) : Vec n a := tl v.
+
 Instance Inhabited_Vec (n:nat) (a:Type) {Ha:Inhabited a} : Inhabited (Vec n a) :=
   MkInhabited (Vec n a) (gen n a (fun _ => inhabitant)).
 
@@ -156,12 +159,40 @@ Fixpoint foldr (a b : Type) (n : nat) (f : a -> b -> b) (base : b) (v : Vec n a)
   | Vector.cons hd _ tl => f hd (foldr _ _ _ f base tl)
   end.
 
+Lemma foldr_nil (a b : Type) (f : a -> b -> b) (base : b) (v : Vec 0 a) :
+  foldr a b 0 f base v = base.
+Proof.
+  rewrite (Vec_0_nil _ v). reflexivity.
+Qed.
+
+Lemma foldr_cons (a b : Type) (n : nat) (f : a -> b -> b) (base : b)
+  (v : Vec (S n) a) : foldr a b (S n) f base v = f (hd v) (foldr a b n f base (tl v)).
+Proof.
+  destruct (Vec_S_cons _ _ v) as [ x [ xs pf ]].
+  rewrite pf. reflexivity.
+Qed.
+
+
 Fixpoint foldl (a b : Type) (n : nat) (f : b -> a -> b) (acc : b) (v : Vec n a) : b :=
   match v with
   | Vector.nil => acc
   | Vector.cons hd _ tl => foldl _ _ _ f (f acc hd) tl
   end.
 
+Lemma foldl_nil (a b : Type) (f : b -> a -> b) (base : b) (v : Vec 0 a) :
+  foldl a b 0 f base v = base.
+Proof.
+  rewrite (Vec_0_nil _ v). reflexivity.
+Qed.
+
+Lemma foldl_cons (a b : Type) (n : nat) (f : b -> a -> b) (base : b)
+  (v : Vec (S n) a) :
+  foldl a b (S n) f base v = foldl a b n f (f base (hd v)) (tl v).
+Proof.
+  destruct (Vec_S_cons _ _ v) as [ x [ xs pf ]].
+  rewrite pf. reflexivity.
+Qed.
+
 Fixpoint scanl (a b : Type) (n : nat) (f : b -> a -> b) (acc : b) (v : Vec n a) : Vec (S n) b :=
   match v in VectorDef.t _ n return Vec (S n) b with
   | Vector.nil => [ acc ]
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
index e884a27635..45bd34ab6b 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -393,7 +393,11 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("coerceVec",     mapsTo vectorsModule "coerceVec")
   , ("eq_Vec",        skip)
   , ("foldr",         mapsTo vectorsModule "foldr")
+  , ("foldr_nil",     mapsTo vectorsModule "foldr_nil")
+  , ("foldr_cons",    mapsTo vectorsModule "foldr_cons")
   , ("foldl",         mapsTo vectorsModule "foldl")
+  , ("foldl_nil",     mapsTo vectorsModule "foldl_nil")
+  , ("foldl_cons",    mapsTo vectorsModule "foldl_cons")
   , ("gen_at_BVVec",  mapsTo preludeExtraModule "gen_at_BVVec")
   , ("genWithProof",  mapsTo vectorsModule "genWithProof")
   , ("scanl",         mapsTo vectorsModule "scanl")
@@ -409,6 +413,8 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("zip",           realize zipSnippet)
   -- cannot map directly to Vector.t because arguments are in a different order
   , ("Vec",           mapsTo vectorsModule "Vec")
+  , ("head",          mapsTo vectorsModule "head")
+  , ("tail",          mapsTo vectorsModule "tail")
   ]
 
   -- Streams
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index fa504674ad..7e88f23e16 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -1153,6 +1153,22 @@ primitive foldr : (a b : sort 0) -> (n : Nat) -> (a -> b -> b) -> b -> Vec n a -
 primitive foldl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> b;
 primitive scanl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> Vec (addNat 1 n) b;
 
+-- Axioms defining foldr
+axiom foldr_nil : (a b : sort 0) -> (f : a -> b -> b) -> (x : b) ->
+                  (v : Vec 0 a) -> Eq b (foldr a b 0 f x v) x;
+axiom foldr_cons : (a b : sort 0) -> (n : Nat) -> (f : a -> b -> b) -> (x : b) ->
+                   (v : Vec (Succ n) a) ->
+                   Eq b (foldr a b (Succ n) f x v)
+                        (f (head n a v) (foldr a b n f x (tail n a v)));
+
+-- Axioms defining foldl
+axiom foldl_nil : (a b : sort 0) -> (f : b -> a -> b) -> (x : b) ->
+                  (v : Vec 0 a) -> Eq b (foldl a b 0 f x v) x;
+axiom foldl_cons : (a b : sort 0) -> (n : Nat) -> (f : b -> a -> b) -> (x : b) ->
+                   (v : Vec (Succ n) a) ->
+                   Eq b (foldl a b (Succ n) f x v)
+                        (foldl a b n f (f x (head n a v)) (tail n a v));
+
 reverse : (n : Nat) -> (a : isort 0) -> Vec n a -> Vec n a;
 reverse n a xs = gen n a (\ (i : Nat) -> at n a xs (subNat (subNat n 1) i));
 
diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index b9596827df..0e464cdbad 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -202,7 +202,7 @@ scMatch ::
   IO (Maybe (Map DeBruijnIndex Term))
 scMatch sc pat term =
   runMaybeT $
-  do --lift $ putStrLn $ "********** scMatch **********"
+  do -- lift $ putStrLn $ "********** scMatch **********"
      MatchState inst cs <- match 0 [] pat term emptyMatchState
      mapM_ (check inst) cs
      return inst
@@ -231,13 +231,13 @@ scMatch sc pat term =
               | j < depth -> go (j : js) t
             _ -> Nothing
 
-    match :: Int -> [(LocalName, Term)] -> Term -> Term -> MatchState -> MaybeT IO MatchState
+    match :: Int -> [(LocalName, Term)] -> Term -> Term -> MatchState ->
+             MaybeT IO MatchState
     match _ _ (STApp i fv _) (STApp j _ _) s
       | fv == emptyBitSet && i == j = return s
     match depth env x y s@(MatchState m cs) =
-      --do
-      --lift $ putStrLn $ "matching (lhs): " ++ scPrettyTerm defaultPPOpts x
-      --lift $ putStrLn $ "matching (rhs): " ++ scPrettyTerm defaultPPOpts y
+      -- (lift $ putStrLn $ "matching (lhs): " ++ scPrettyTerm defaultPPOpts x) >>
+      -- (lift $ putStrLn $ "matching (rhs): " ++ scPrettyTerm defaultPPOpts y) >>
       case asVarPat depth x of
         Just (i, js) ->
           do -- ensure parameter variables are distinct
@@ -268,6 +268,11 @@ scMatch sc pat term =
                Just y3 -> if y2 == y3 then return (MatchState m' cs) else mzero
         Nothing ->
           case (unwrapTermF x, unwrapTermF y) of
+            (_, FTermF (NatLit n))
+              | Just (c, [x']) <- R.asCtor x
+              , primName c == preludeSuccIdent && n > 0 ->
+                do y' <- lift $ scNat sc (n-1)
+                   match depth env x' y' s
             -- check that neither x nor y contains bound variables less than `depth`
             (FTermF xf, FTermF yf) ->
               case zipWithFlatTermF (match depth env) xf yf of

From d617dafec14533a7baa301f1fe3f96b33e9b455e Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 3 Feb 2023 12:12:46 -0800
Subject: [PATCH 2/4] added axioms head_gen and tail_gen to define head and
 tail of a gen

---
 .../CryptolToCoq/SAWCoreVectorsAsCoqVectors.v        | 12 ++++++++++++
 .../Verifier/SAW/Translation/Coq/SpecialTreatment.hs |  2 ++
 saw-core/prelude/Prelude.sawcore                     |  8 ++++++++
 3 files changed, 22 insertions(+)

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
index 340cc95a42..dce38ce7b2 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
@@ -71,6 +71,18 @@ Defined.
 Definition head (n : nat) (a : Type) (v : Vec (S n) a) : a := hd v.
 Definition tail (n : nat) (a : Type) (v : Vec (S n) a) : Vec n a := tl v.
 
+Lemma head_gen (n : nat) (a : Type) (f : nat -> a) :
+  head n a (gen (Succ n) a f) = f 0.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma tail_gen (n : nat) (a : Type) (f : nat -> a) :
+  tail n a (gen (Succ n) a f) = gen n a (fun (i:Nat) => f (Succ i)).
+Proof.
+  reflexivity.
+Qed.
+
 Instance Inhabited_Vec (n:nat) (a:Type) {Ha:Inhabited a} : Inhabited (Vec n a) :=
   MkInhabited (Vec n a) (gen n a (fun _ => inhabitant)).
 
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
index 45bd34ab6b..435beea5fa 100644
--- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
+++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -415,6 +415,8 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("Vec",           mapsTo vectorsModule "Vec")
   , ("head",          mapsTo vectorsModule "head")
   , ("tail",          mapsTo vectorsModule "tail")
+  , ("head_gen",      mapsTo vectorsModule "head_gen")
+  , ("tail_gen",      mapsTo vectorsModule "tail_gen")
   ]
 
   -- Streams
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 7e88f23e16..07b146bbdb 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -1096,6 +1096,14 @@ primitive gen : (n : Nat) -> (a : sort 0) -> (Nat -> a) -> Vec n a;
 primitive head : (n : Nat) -> (a : sort 0) -> Vec (Succ n) a -> a;
 primitive tail : (n : Nat) -> (a : sort 0) -> Vec (Succ n) a -> Vec n a;
 
+-- Axioms describing head and tail in terms of gen
+axiom head_gen : (n : Nat) -> (a : sort 0) -> (f : Nat -> a) ->
+                 Eq a (head n a (gen (Succ n) a f)) (f 0);
+
+axiom tail_gen : (n : Nat) -> (a : sort 0) -> (f : Nat -> a) ->
+                 Eq (Vec n a) (tail n a (gen (Succ n) a f))
+                              (gen n a (\ (i:Nat) -> f (Succ i)));
+
 -- An implementation for atWithDefault
 --
 -- FIXME: can we replace atWithDefault with this implementation? Or does some

From edc0dd59d698aefdd27063580f188c87c6f5be3f Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 3 Feb 2023 12:40:02 -0800
Subject: [PATCH 3/4] added integration test to test the new foldl rewrite
 rules

---
 intTests/test_fold_rewrite_proof/test.sh      |  1 +
 .../test_fold_rewrite_proof/tupletest.cry     | 28 +++++++++++++++++++
 .../test_fold_rewrite_proof/tupletest.saw     | 26 +++++++++++++++++
 3 files changed, 55 insertions(+)
 create mode 100644 intTests/test_fold_rewrite_proof/test.sh
 create mode 100644 intTests/test_fold_rewrite_proof/tupletest.cry
 create mode 100644 intTests/test_fold_rewrite_proof/tupletest.saw

diff --git a/intTests/test_fold_rewrite_proof/test.sh b/intTests/test_fold_rewrite_proof/test.sh
new file mode 100644
index 0000000000..81f1ccf21f
--- /dev/null
+++ b/intTests/test_fold_rewrite_proof/test.sh
@@ -0,0 +1 @@
+$SAW tupletest.saw
diff --git a/intTests/test_fold_rewrite_proof/tupletest.cry b/intTests/test_fold_rewrite_proof/tupletest.cry
new file mode 100644
index 0000000000..ca11073487
--- /dev/null
+++ b/intTests/test_fold_rewrite_proof/tupletest.cry
@@ -0,0 +1,28 @@
+module tupletest where
+
+foldFunction : [8] -> [16] -> [16] -> [8]
+foldFunction x y z = output.0
+  where
+    output = foldl fnc (x, y, z) [0 .. 15]
+
+fnc : ([8], [16], [16]) -> [4] -> ([8], [16], [16])
+fnc (x, y, z) i = returnTup
+  where
+    returnTup = (x ^ take y' ^ take z', y', z')
+    y' = y <<< i
+    z' = z >>> i
+
+foldFunction' : [8] -> [16] -> [16] -> [8]
+foldFunction' x y z = output.0
+  where
+    output = foldl fnc' (x, y, z) [15, 14 .. 0]
+
+fnc' : ([8], [16], [16]) -> [4] -> ([8], [16], [16])
+fnc' (x, y, z) i = returnTup
+  where
+    returnTup = (x ^ take y ^ take z, y', z')
+    y' = y >>> i
+    z' = z <<< i
+
+property foldFunctionInverse x y z =
+    foldFunction' (foldFunction x y z) y z == x
diff --git a/intTests/test_fold_rewrite_proof/tupletest.saw b/intTests/test_fold_rewrite_proof/tupletest.saw
new file mode 100644
index 0000000000..d0521461df
--- /dev/null
+++ b/intTests/test_fold_rewrite_proof/tupletest.saw
@@ -0,0 +1,26 @@
+enable_experimental;
+
+let use_lemmas lemmas =
+    simplify (addsimps lemmas
+              (add_prelude_eqs ["foldl_cons","foldl_nil","head_gen","tail_gen"] (cryptol_ss())));
+
+let proveit p script =
+  do {
+    print (str_concat "Proving " (show_term p));
+    time (prove_print script p);
+  };
+
+import "tupletest.cry";
+
+fnc_lemma <- proveit {{ \x y z i -> (fnc' (fnc (x, y, z) i) i).0 == x }} z3;
+
+proveit {{ foldFunctionInverse }} do {
+    unfolding [ "foldFunctionInverse"
+              , "foldFunction"
+              , "foldFunction'"
+              ];
+    goal_normalize ["fnc", "fnc'"];
+    simplify (add_prelude_eqs ["foldl_cons","foldl_nil",
+                               "head_gen","tail_gen"] (cryptol_ss()));
+    z3;
+};

From 0e10161026557064492dda8e8a5af21f1c28bb95 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Fri, 3 Feb 2023 12:55:42 -0800
Subject: [PATCH 4/4] added comments to explain some of how the rewriter works

---
 saw-core/src/Verifier/SAW/Rewriter.hs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index 0e464cdbad..c21d5f12e9 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -158,6 +158,7 @@ first_order_match pat term = match pat term Map.empty
 -- occur as the 2nd argument of an @App@ constructor. This ensures
 -- that instantiations are well-typed.
 
+-- | Test if a term is a constant natural number
 asConstantNat :: Term -> Maybe Natural
 asConstantNat t =
   case R.asCtor t of
@@ -207,6 +208,8 @@ scMatch sc pat term =
      mapM_ (check inst) cs
      return inst
   where
+    -- Check that a constraint of the form pat = n for natural number literal n
+    -- is satisfied by the supplied substitution (aka instantiation) inst
     check :: Map DeBruijnIndex Term -> (Term, Natural) -> MaybeT IO ()
     check inst (t, n) = do
       --lift $ putStrLn $ "checking: " ++ show (t, n)
@@ -219,6 +222,11 @@ scMatch sc pat term =
         Just i | i == n -> return ()
         _ -> mzero
 
+    -- Check if a term is a higher-order variable pattern, i.e., a free variable
+    -- (meaning one that can match anything) applied to 0 or more bound variable
+    -- arguments. Depth is the number of variables bound by lambdas or pis since
+    -- the top of the current pattern, so "free" means >= the current depth and
+    -- "bound" means less than the current depth
     asVarPat :: Int -> Term -> Maybe (DeBruijnIndex, [DeBruijnIndex])
     asVarPat depth = go []
       where
@@ -231,6 +239,10 @@ scMatch sc pat term =
               | j < depth -> go (j : js) t
             _ -> Nothing
 
+    -- Test if term y matches pattern x, meaning whether there is a substitution
+    -- to the free variables of x to make it equal to y. Depth is the number of
+    -- bound variables, so a "free" variable is a deBruijn index >= depth. Env
+    -- saves the names associated with those bound variables.
     match :: Int -> [(LocalName, Term)] -> Term -> Term -> MatchState ->
              MaybeT IO MatchState
     match _ _ (STApp i fv _) (STApp j _ _) s