Merge pull request #1503 from GaloisInc/coq-primitives

More updates to Coq extraction

doc/manual/galois-whitepaper.cls

@@ -82,7 +82,7 @@
 \rhead{\sffamily \textit{\@title{}}}
 \makeatother
 
-\lfoot{\sffamily\color{lightgray}\small\copyright{} 2019 Galois, Inc.}
+\lfoot{\sffamily\color{lightgray}\small\copyright{} 2021 Galois, Inc.}
 
 \rfoot{
   % \sffamily \color{galoislightgray}\small

saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v

@@ -420,7 +420,7 @@ Definition minNat : SAWCoreScaffolding.Nat -> SAWCoreScaffolding.Nat -> SAWCoreS
   fun (x : SAWCoreScaffolding.Nat) (y : SAWCoreScaffolding.Nat) => Nat_cases2 SAWCoreScaffolding.Nat (fun (y' : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Zero) (fun (x' : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Zero) (fun (x' : SAWCoreScaffolding.Nat) (y' : SAWCoreScaffolding.Nat) (min_xy : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Succ min_xy) x y.
 
 Definition maxNat : SAWCoreScaffolding.Nat -> SAWCoreScaffolding.Nat -> SAWCoreScaffolding.Nat :=
-  fun (x : SAWCoreScaffolding.Nat) (y : SAWCoreScaffolding.Nat) => Nat_cases2 SAWCoreScaffolding.Nat (fun (x' : SAWCoreScaffolding.Nat) => x') (fun (y' : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Succ y') (fun (y' : SAWCoreScaffolding.Nat) (x' : SAWCoreScaffolding.Nat) (sub_xy : SAWCoreScaffolding.Nat) => sub_xy) y x.
+  fun (x : SAWCoreScaffolding.Nat) (y : SAWCoreScaffolding.Nat) => Nat_cases2 SAWCoreScaffolding.Nat (fun (y' : SAWCoreScaffolding.Nat) => y') (fun (x' : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Succ x') (fun (x' : SAWCoreScaffolding.Nat) (y' : SAWCoreScaffolding.Nat) (max_xy : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Succ max_xy) x y.
 
 (* Prelude.widthNat was skipped *)
 

saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v

@@ -1,6 +1,7 @@
 (* This module contains additional definitions that can only be defined after *)
 (* the Cryptol prelude has been defined. *)
 
+From Coq          Require Import Lia.
 From Coq          Require Import Lists.List.
 From Coq          Require Import String.
 From Coq          Require Import Vectors.Vector.
@@ -28,69 +29,33 @@ Proof.
   reflexivity.
 Qed.
 
-Theorem min_S n : min n (S n) = n.
+Theorem min_nSn n : min n (S n) = n.
 Proof.
-  rewrite PeanoNat.Nat.min_comm.
-  induction n.
-  { reflexivity. }
-  { simpl in *. intuition. }
+  induction n; simpl; auto.
+Qed.
+
+Theorem min_Snn n : min (S n) n = n.
+Proof.
+  induction n; simpl; auto.
 Qed.
 
 Ltac solveUnsafeAssertStep :=
   match goal with
   | [ |- context [ Succ ] ] => unfold Succ
+  | [ |- context [ addNat _ _ ] ] => rewrite addNat_add
+  | [ |- context [ mulNat _ _ ] ] => rewrite mulNat_mul
+  | [ |- context [ subNat _ _ ] ] => rewrite subNat_sub
+  | [ |- context [ maxNat _ _ ] ] => rewrite maxNat_max
+  | [ |- context [ minNat _ _ ] ] => rewrite minNat_min
   | [ n : Num |- _ ] => destruct n
   | [ |- Eq Num (TCNum _) (TCNum _) ] => apply Eq_TCNum
   | [ |- Eq Num _ _ ] => reflexivity
-  | [ |- context [ minNat _ _ ] ] => rewrite minNat_min
-  | [ |- min ?n (S ?n) = ?n ] => apply min_S
+  | [ |- min ?n (S ?n) = _ ] => rewrite (min_nSn n)
+  | [ |- min (S ?n) ?n = _ ] => rewrite (min_Snn n)
   end.
 
-Ltac solveUnsafeAssert := repeat (solveUnsafeAssertStep; simpl); trivial.
-
-Definition cbc_enc_helper n : Eq Num (tcMin n (tcAdd (TCNum 1) n)) n :=
-  ltac:(solveUnsafeAssert).
-
-(*
-Goal forall n p b, Eq Num (tcAdd n (tcAdd (TCNum 32) p)) (tcMul (tcAdd (TCNum 2) b) (TCNum 16)).
-  intros.
-  simpl.
-  solve_unsafeAssert_step. simpl.
+Ltac solveUnsafeAssert := repeat (solveUnsafeAssertStep; simpl; try lia); trivial.
 
-Goal forall n0, Eq Num TCInf
-   (TCNum
-      (S
-         (S
-            (S
-               (S
-                  (S
-                     (S
-                        (S
-                           (S
-                              (S
-                                 (S
-                                    (S
-                                       (S
-                                          (S
-                                             (S
-                                                (S
-                                                   (S
-                                                      (S
-                                                         (S
-                                                            (S
-                                                               (S
-                                                                  (S
-                                                                     (S
-                                                                        (S
-                                                                           (S
-                                                                              (S
-                                                                                 (S
-                                                                                    (S
-                                                                                       (S
-                                                                                          (S (S (S (S (mulNat n0 16)))))))))))))))))))))))))))))))))).
-  intros.
-  solve_unsafeAssert.
-*)
 
 Fixpoint iterNat {a : Type} (n : nat) (f : a -> a) : a -> a :=
   match n with
@@ -99,7 +64,7 @@ Fixpoint iterNat {a : Type} (n : nat) (f : a -> a) : a -> a :=
   end
 .
 
-Fixpoint iter {a : Type} (n : Num) (f : a -> a) : a -> a :=
+Definition iter {a : Type} (n : Num) (f : a -> a) : a -> a :=
     match n with
     | TCNum n => fun xs => iterNat n f xs
     | TCInf   => fun xs => xs

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v

@@ -14,51 +14,37 @@ Fixpoint Nat_cases2_match a f1 f2 f3 (x y : nat) : a :=
   | (S x, S y) => f3 x y (Nat_cases2_match a f1 f2 f3 x y)
   end.
 
-Theorem Nat_cases2_match_spec a f1 f2 f3 x y :
+Theorem Nat_cases2_match_spec a f1 f2 f3 : forall x y,
   Nat_cases2 a f1 f2 f3 x y = Nat_cases2_match a f1 f2 f3 x y.
 Proof.
-  revert y.
-  induction x; intros y.
-  {
-    reflexivity.
-  }
-  {
-    destruct y.
-    {
-      reflexivity.
-    }
-    {
-      simpl.
-      now rewrite IHx.
-    }
-  }
+  induction x; induction y; simpl; congruence.
 Qed.
 
-Theorem minNat_min a b : minNat a b = min a b.
+Theorem minNat_min : forall x y, minNat x y = min x y.
 Proof.
-  revert b.
-  induction a; intros b.
-  {
-    reflexivity.
-  }
-  {
-    destruct b; simpl; intuition.
-  }
+  induction x; induction y; simpl; auto.
 Qed.
 
-Theorem minNat_Succ n : minNat n (Succ n) = n.
+Theorem maxNat_max : forall x y, maxNat x y = max x y.
 Proof.
-  unfold minNat.
-  rewrite Nat_cases2_match_spec.
-  induction n.
-  {
-    reflexivity.
-  }
-  {
-    unfold Succ in *.
-    simpl.
-    intuition.
-  }
+  induction x; induction y; simpl; auto.
+Qed.
+
+Theorem addNat_add : forall x y, addNat x y = x + y.
+Proof.
+  induction x; simpl; auto.
+Qed.
+
+Theorem subNat_sub : forall x y, subNat x y = x - y.
+Proof.
+  induction x; induction y; simpl; auto.
+Qed.
+
+Theorem mulNat_mul : forall x y, mulNat x y = x * y.
+Proof.
+  induction x; simpl; intros; auto.
+  rewrite IHx.
+  apply addNat_add.
 Qed.
 
 Theorem fold_unfold_IRT As Ds D : forall x, foldIRT As Ds D (unfoldIRT As Ds D x) = x.

saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

@@ -572,71 +572,11 @@ translateTermUnshared t = withLocalTranslationState $ do
               [] -> return ite
               _  -> Coq.App ite <$> mapM translateTerm rest
           _ -> badTerm
-        -- NOTE: the following works for something like CBC, because computing
-        -- the n-th block only requires n steps of recursion
-        -- FIXME: (pun not intended) better conditions for when this is safe to do
-        "Prelude.fix" ->
-          case args of
-          []  -> errorTermM "call to Prelude.fix with no argument"
-          [_] -> errorTermM "call to Prelude.fix with 1 argument"
-          resultType : lambda : rest ->
-            case resultType of
-            -- TODO: check that 'n' is finite
-            (asSeq -> Just (n, _)) ->
-              case lambda of
-
-              (asLambda -> Just (x, seqType, body)) | seqType == resultType ->
-                  do
-                    len <- translateTerm n
-                    (x', expr) <-
-                      withLocalTranslationState $
-                      do x' <- freshenAndBindName x
-                         expr <- translateTerm body
-                         pure (x', expr)
-                    seqTypeT <- translateTerm seqType
-                    defaultValueT <- defaultTermForType resultType
-                    let iter =
-                          Coq.App (Coq.Var "iter")
-                          [ len
-                          , Coq.Lambda [Coq.Binder x' (Just seqTypeT)] expr
-                          , defaultValueT
-                          ]
-                    case rest of
-                      [] -> return iter
-                      _  -> Coq.App iter <$> mapM translateTerm rest
-              _ -> badTerm
-            -- NOTE: there is currently one instance of `fix` that will trigger
-            -- `errorTermM`.  It is used in `Cryptol.cry` when translating
-            -- `iterate`, which generates an infinite stream of nested
-            -- applications of a given function.
-
-            (asPiList -> (pis, afterPis)) ->
-              -- NOTE: this will output some code, but it is likely that Coq
-              -- will reject it for not being structurally recursive.
-              case lambda of
-              (asLambdaList -> ((recFn, _) : binders, body)) -> do
-                let (_binderPis, otherPis) = splitAt (length binders) pis
-                (recFn', bindersT, typeT, bodyT) <- withLocalTranslationState $ do
-                  -- this is very ugly...
-                  recFn' <- freshenAndBindName recFn
-                  bindersT <- mapM
-                    (\ (b, bType) -> do
-                      bTypeT <- translateTerm bType
-                      b' <- freshenAndBindName b
-                      return $ Coq.Binder b' (Just bTypeT)
-                    )
-                    binders
-                  typeT <- translatePi otherPis afterPis
-                  bodyT <- translateTerm body
-                  return (recFn', bindersT, typeT, bodyT)
-                let fix = Coq.Fix recFn' bindersT typeT bodyT
-                case rest of
-                  [] -> return fix
-                  _  -> errorTermM "THAT" -- Coq.App fix <$> mapM (go env) rest
-              _ -> errorTermM "call to Prelude.fix without lambda"
-
-        _ ->
-          translateIdentWithArgs i args
+
+        -- Refuse to translate any recursive value defined using Prelude.fix
+        "Prelude.fix" -> badTerm
+
+        _ -> translateIdentWithArgs i args
       _ -> Coq.App <$> translateTerm f <*> traverse translateTerm args
 
     LocalVar n

saw-core/prelude/Prelude.sawcore

@@ -859,9 +859,9 @@ minNat x y =
 -- | Maximum
 maxNat : Nat -> Nat -> Nat;
 maxNat x y =
-  Nat_cases2 Nat (\ (x':Nat) -> x')
-             (\ (y':Nat) -> Succ y')
-             (\ (y':Nat) -> \ (x':Nat) -> \ (sub_xy:Nat) -> sub_xy) y x;
+  Nat_cases2 Nat (\ (y':Nat) -> y')
+             (\ (x':Nat) -> Succ x')
+             (\ (x':Nat) -> \ (y':Nat) -> \ (max_xy:Nat) -> Succ max_xy) x y;
 
 -- | Width(n) = 1 + floor(log_2(n))
 primitive widthNat : Nat -> Nat;