Add composition support to prove_bisim

doc/manual/manual.md

@@ -4042,39 +4042,45 @@ N.B: The following commands must first be enabled using `enable_experimental`.
 
 SAW contains a bisimulation prover to prove that two terms simulate each other.
 This prover allows users to prove that two terms executing in lockstep satisfy
-some relation over the state of each circuit and their outputs.  This type of
+some relations over the state of each circuit and their outputs.  This type of
 proof is useful in demonstrating the eventual equivalence of two circuits, or
 of a circuit and a functional specification.  SAW enables these proofs with the
 experimental `prove_bisim` command:
 
 ~~~~
-prove_bisim : ProofScript () -> Term -> Term -> Term -> TopLevel ProofResult
+prove_bisim : ProofScript () -> [BisimTheorem] -> Term -> Term -> Term -> Term -> TopLevel ProofResult
 ~~~~
 
-When invoking `prove_bisim strat relation lhs rhs`, the arguments represent the
-following:
+When invoking `prove_bisim strat theorems srel orel lhs rhs`, the arguments
+represent the following:
 
 1. `strat`: A proof strategy to use during verification.
-2. `relation`: A relation between `lhs` and `rhs`.  This relation must have the
-   type `(lhsState, output) -> (rhsState, output) -> Bit`. The relation's first
-   argument is a pair consisting of `lhs`'s state and output following
+2. `theorems`: A list of already proven bisimulation theorems.
+3. `srel`: A state relation between `lhs` and `rhs`.  This relation must have
+   the type `lhsState -> rhsState -> Bit`. The relation's first argument is
+   `lhs`'s state prior to execution. The relation's second argument is `rhs`'s
+   state prior to execution. `srel` then returns a `Bit` indicating whether
+   the two arguments satisfy the bisimulation's state relation.
+4. `orel`: An output relation between `lhs` and `rhs`.  This relation must have
+   the type `(lhsState, output) -> (rhsState, output) -> Bit`. The relation's
+   first argument is a pair consisting of `lhs`'s state and output following
    execution. The relation's second argument is a pair consisting of `rhs`'s
-   state and output following execution. `relation` then then returns a `Bit`
-   indicating whether the two arguments satisfy the bisimulation relation. That
-   is, whether the terms simulate each other.
-3. `lhs`: A term that simulates `rhs`. `lhs` must have the type
+   state and output following execution. `orel` then returns a `Bit` indicating
+   whether the two arguments satisfy the bisimulation's output relation.
+5. `lhs`: A term that simulates `rhs`. `lhs` must have the type
    `(lhsState, input) -> (lhsState, output)`.  The first argument to `lhs` is a
    tuple containing the internal state of `lhs`, as well as the input to `lhs`.
    `lhs` returns a tuple containing its internal state after execution, as well
    as its output.
-4. `rhs`: A term that simulates `lhs`. `rhs` must have the type
+6. `rhs`: A term that simulates `lhs`. `rhs` must have the type
    `(rhsState, input) -> (rhsState, output)`.  The first argument to `rhs` is a
    tuple containing the internal state of `rhs`, as well as the input to `rhs`.
    `rhs` returns a tuple containing its internal state after execution, as well
    as its output.
 
-`prove_bisim` returns a `ProofResult` indicating whether `lhs` and `rhs` are
-bisimilar, given the relation `relation`.
+On success, `prove_bisim` returns a `BisimTheorem` that can be used in future
+bisimulation proofs to enable compositional bisimulation proofs.  On failure,
+`prove_bisim` will abort.
 
 ## Bisimulation Example
 
@@ -4142,22 +4148,38 @@ is the result of the function's computation.
 It computes the logical AND directly on the function's inputs using Cryptol's
 `(&&)` operator.
 
+Next, we define a state relation over `andImp` and `andSpec`:
+
+~~~~
+andStateRel : andState -> () -> Bit
+andStateRel _ () = True
+~~~~
+
+`andStateRel` takes two arguments:
+
+1. An `andState` for `andImp`.
+2. An empty state (`()`) for `andSpec`.
+
+`andStateRel` returns a `Bit` indicating whether the relation is satisified.  In
+this case, `andStateRel` always returns `True` because `andSpec` is stateless
+and therefore the state relation permits `andImp` to accept any state.
+
 Lastly, we define a relation over `andImp` and `andSpec`:
 
 ~~~~
-andRel : (andState, (Bit, Bit)) -> ((), (Bit, Bit)) -> Bit
-andRel (s, (impReady, impO)) ((), (_, specO)) =
+andOutputRel : (andState, (Bit, Bit)) -> ((), (Bit, Bit)) -> Bit
+andOutputRel (s, (impReady, impO)) ((), (_, specO)) =
   if impReady then impO == specO else True
 ~~~~
 
-`andRel` takes two arguments:
+`andOutputRel` takes two arguments:
 
 1. A return value from `andImp`. Specifically, a pair consisting of an
    `andState` and a pair containing a ready bit and result of the logical AND.
 2. A return value from `andSpec`. Specifically, a pair consisting of an empty
    state `()` and a pair containing a ready bit and result of the logical AND.
 
-`andRel` returns a `Bit` indicating whether the relation is satisfied.  It
+`andOutputRel` returns a `Bit` indicating whether the relation is satisfied.  It
 considers the relation satisfied in two ways:
 
 1. If `andImp`'s ready bit is set, the relation is satisfied if the output
@@ -4175,13 +4197,9 @@ terms are bisimilar--by using `prove_bisim`:
 import "And.cry";
 enable_experimental;
 
-res <- prove_bisim z3 {{ andRel }} {{ andImp }} {{ andSpec }};
-print res;
+and_bisim <- prove_bisim z3 [] {{ andStateRel }} {{ andOutputRel }} {{ andImp }} {{ andSpec }};
 ~~~~
 
-Upon running this script, SAW prints `Valid` indicating that `andImp` and
-`andSpec` are bisimilar, given the relation `andRel`.
-
 ### Building a NAND gate
 
 We can make the example more interesting by reusing components to build a NAND
@@ -4200,7 +4218,7 @@ result:
 nandImp : (nandState, (Bit, Bit)) -> (nandState, (Bit, Bit))
 nandImp x = (s, (andReady, ~andRes))
   where
-    (s ,(andReady, andRes)) = andImp x
+    (s, (andReady, andRes)) = andImp x
 ~~~~
 
 Note that `nandImp` is careful to preserve the ready status of `andImp`.
@@ -4217,41 +4235,93 @@ nandSpec (_, (x, y)) = ((), (True, ~ (andSpec ((), (x, y))).1.1))
 As with `andSpec`, `nandSpec` is pure and computes its result in a single
 cycle.
 
-Lastly, we define a relation indicating that `nandImp` and `nandSpec` produce
-equivalent results once `nandImp`'s ready bit is `1`:
+Next, we define a state relation over `nandImp` and `nandSpec`:
+
+~~~~
+nandStateRel : andState -> () -> Bit
+nandStateRel _ () = True
+~~~~
+
+As with `andStateRel`, this state relation is always `True` because `nandSpec`
+is stateless.
+
+Lastly, we define an output relation indicating that `nandImp` and `nandSpec`
+produce equivalent results once `nandImp`'s ready bit is `1`:
 
 ~~~~
-nandRel : (nandState, (Bit, Bit)) -> ((), (Bit, Bit)) -> Bit
-nandRel (s, (impReady, impO)) ((), (_, specO)) =
+nandOutputRel : (nandState, (Bit, Bit)) -> ((), (Bit, Bit)) -> Bit
+nandOutputRel (s, (impReady, impO)) ((), (_, specO)) =
   if impReady then impO == specO else True
 ~~~~
 
 To prove that `nandImp` and `nandSpec` are bisimilar, we again use
-`prove_bisim`:
+`prove_bisim`. This time however, we can reuse the bisimulation proof for the
+AND gate by including it in the `theorems` paramter for `prove_bisim`:
 
 ~~~~
-res2 <- prove_bisim z3 {{ nandRel }} {{ nandImp }} {{ nandSpec }};
-print res2;
+prove_bisim z3 [and_bisim] {{ nandStateRel }} {{ nandOutputRel }} {{ nandImp }} {{ nandSpec }};
 ~~~~
 
-Upon running this portion of the script, SAW prints `Valid` confirming that the
-two terms are bisimilar, given the relation `nandRel`.
-
-## Understanding the proof goal
+## Understanding the proof goals
 
 While not necessary for simple proofs, more advanced proofs may require
-inspecting the proof goal.  `prove_bisim` generates and attempts to solve the
-proof goal:
+inspecting proof goals.  `prove_bisim` generates and attempts to solve the
+following proof goals:
 
 ~~~~
-forall s1 s2 in out1 out2.
-    relation (s1, out1) (s2, out2) -> relation (lhs (s1, in)) (rhs (s2, in))
+OUTPUT RELATION THEOREM:
+  forall s1 s2 in.
+    srel s1 s2 -> orel (lhs (s1, in)) (rhs (s2, in))
+
+STATE RELATION THEOREM:
+  forall s1 s2 out1 out2.
+    orel (s1, out1) (s2, out2) -> srel s1 s2
 ~~~~
 
-where the variables in the `forall` are:
+where the variables in the `forall`s are:
 
 * `s1`: Initial state for `lhs`
 * `s2`: Initial state for `rhs`
 * `in`: Input value to `lhs` and `rhs`
 * `out1`: Initial output value for `lhs`
 * `out2`: Initial output value for `rhs`
+
+The `STATE RELATION THEOREM` verifies that the output relation properly captures
+the guarantees of the state relation.  The `OUTPUT RELATION THEOREM` verifies
+that if `lhs` and `rhs` are executed with related states, then the result of
+that execution is also related.  These two theorems together guarantee that the
+terms simulate eachother.
+
+When using composition, the `prove_bisim` also generates and attempts to solve
+the proof goal below for any successfully applied `BisimTheorem` in the
+`theorems` list:
+
+~~~~
+COMPOSITION SIDE CONDITION:
+  forall g_lhs_s g_rhs_s.
+    g_srel g_lhs_s g_rhs_s -> f_srel f_lhs_s f_rhs_s
+~~~~
+
+where `g_lhs` contains a call to `f_lhs` and `g_rhs` contains a call to `f_rhs`, and the variables in `COMPOSITION SIDE CONDITION` are:
+
+* `g_lhs_s`: The state for `g_lhs`
+* `g_rhs_s`: The state for `g_rhs`
+* `g_srel`: The state relation for `g_lhs` and `g_rhs`
+* `f_srel`: The state relation for `f_lhs` and `f_rhs`
+* `f_lhs_s`: The state for `f_lhs`, as represented in `g_lhs_s`
+* `f_rhs_s`: The state for `f_rhs`, as represented in `g_rhs_s`
+
+The `COMPOSITION SIDE CONDITION` exists to verify that the terms in the
+bisimulation relation properly set up valid states for subterms they contain.
+
+## Limitiations
+
+For now, the `prove_bisim` command has a couple limitations:
+
+* `lhs` and `rhs` must be named functions.  This is because `prove_bisim` uses
+  these names to perform substitution when making use of compositionality.
+* Each subterm present in the list of bisimulation theorems already
+  proven may be invoked at most once in `lhs` or `rhs`.  That is, if some
+  function `g_lhs` calls `f_lhs`, and `prove_bisim` is invoked with a
+  `BisimTheorem` proving that `f_lhs` is bisimilar to `f_rhs`, then `g_lhs` may
+  call `f_lhs` at most once.

intTests/test_bisimulation/Comp.cry

@@ -24,25 +24,35 @@ andImp (s, (x, y)) =
   then (s, (True, s.origX && s.origY))
   else ({ loaded = True, origX = x, origY = y }, (False, 0))
 
-// Relation between `andImp` and `andSpec`.  Checks that outputs are
+// Output relation between `andImp` and `andSpec`.  Checks that outputs are
 // equivalent, given that `andImp` is ready to be read.
-andRel : (andState, (Bit, Bit)) -> ((), (Bit, Bit)) -> Bit
-andRel (s, (impReady, impO)) ((), (_, specO)) =
+andOutputRel : (andState, (Bit, Bit)) -> ((), (Bit, Bit)) -> Bit
+andOutputRel (s, (impReady, impO)) ((), (_, specO)) =
   if impReady then impO == specO else True
 
-// Stateful NAND gate holds `andState`. It has no additional state.
-type nandState = andState
+// State relation between `andImp` and `andSpec`.  Trivial in this case because
+// `andSpec` is stateless.
+andStateRel : andState -> () -> Bit
+andStateRel _ () = True
+
+// Stateful NAND gate holds `andState` as well as an unused bit.
+type nandState = { as : andState, unused : Bit }
 
 // A stateful NAND gate.  First output bit is the ready bit, second bit is the
 // result.  This gate takes 2 cycles to compute.  It restarts when the input
 // changes.
 nandImp : (nandState, (Bit, Bit)) -> (nandState, (Bit, Bit))
-nandImp x = (s, (andReady, ~andRes))
+nandImp (s, in) = ({ as = as' , unused = False }, (andReady, ~andRes))
   where
-    (s ,(andReady, andRes)) = andImp x
+    (as', (andReady, andRes)) = andImp (s.as, in)
 
 // Relation between `nandImp` and `nandSpec`.  Checks that outputs are
 // equivalent, given that `nandImp` is ready to be read.
-nandRel : (nandState, (Bit, Bit)) -> ((), (Bit, Bit)) -> Bit
-nandRel (s, (impReady, impO)) ((), (_, specO)) =
+nandOutputRel : (nandState, (Bit, Bit)) -> ((), (Bit, Bit)) -> Bit
+nandOutputRel (s, (impReady, impO)) ((), (_, specO)) =
   if impReady then impO == specO else True
+
+// State relation between `nandImp` and `nandSpec`.  Trivial in this case
+// because `nandSpec` is stateless.
+nandStateRel : nandState -> () -> Bit
+nandStateRel _ () = True

intTests/test_bisimulation/Test.cry

@@ -20,6 +20,10 @@ f2_bad_input_type (ctr, inp) = (ctr+1, (drop inp)+(drop ctr))
 f2_bad_output_type : (S2, [8]) -> (S2, [9])
 f2_bad_output_type (ctr, inp) = (ctr+1, zext (inp+(drop ctr)))
 
-// Bisimulation relation for f1 and f2
-rel : (S1, [8]) -> (S2, [8]) -> Bit
-rel (s1, o1) (s2, o2) = s1 == drop s2 /\ o1 == o2
+// Output bisimulation relation for f1 and f2
+orel : (S1, [8]) -> (S2, [8]) -> Bit
+orel (s1, o1) (s2, o2) = s1 == drop s2 /\ o1 == o2
+
+// State bisimulation relation for f1 and f2
+srel : S1 -> S2 -> Bit
+srel s1 s2 = s1 == drop s2

intTests/test_bisimulation/comp.saw

@@ -1,13 +1,29 @@
-/* Test the prove_bisim command with a compositional circuit. At the moment,
- * prove_bisim does not have any notion of compositionality, but this example
- * is simple enough to work as-is */
+/* Test the prove_bisim command with a compositional circuit */
 
 import "Comp.cry";
 
 enable_experimental;
 
-res <- prove_bisim z3 {{ andRel }} {{ andImp }} {{ andSpec }};
-print res;
+// Prove 'andImp' and 'andSpec' simulate eachother
+and_res <- prove_bisim z3
+                       []
+                       {{ andStateRel }}
+                       {{ andOutputRel }}
+                       {{ andImp }}
+                       {{ andSpec }};
 
-res2 <- prove_bisim z3 {{ nandRel }} {{ nandImp }} {{ nandSpec }};
-print res2;
+// Prove 'nandImp' and 'nandSpec' simulate eachother, using 'and_res' in the
+// process.
+nand_res <- prove_bisim (do {
+    unfolding ["nandImp", "nandSpec"];
+    w4_unint_z3 ["andImp", "andSpec" ];
+  })
+  [and_res] {{ \x -> nandStateRel x }} {{ \x -> nandOutputRel x }} {{ nandImp }} {{ nandSpec }};
+
+// Test using theorem that doesn't apply
+prove_bisim z3
+            [nand_res]
+            {{ andStateRel }}
+            {{ andOutputRel }}
+            {{ andImp }}
+            {{ andSpec }};

intTests/test_bisimulation/test.saw

@@ -4,17 +4,22 @@ import "Test.cry";
 
 enable_experimental;
 
-res <- prove_bisim z3 {{ rel }} {{ f1 }} {{ f2 }};
-print res;
+res <- prove_bisim z3 [] {{ srel }} {{ orel }} {{ f1 }} {{ f2 }};
+
+// Test non-named constant in bisimulation term
+fails (prove_bisim z3 [] {{ srel }} {{ orel }} {{ f1 }} {{ \x -> f2 x }});
 
 // Test incompatable input types
-fails (prove_bisim z3 {{ rel }} {{ f1 }} {{ f2_bad_input_type }});
+fails (prove_bisim z3 [] {{ srel }} {{ orel }} {{ f1 }} {{ f2_bad_input_type }});
 
 // Test incompatable output types
-fails (prove_bisim z3 {{ rel }} {{ f1 }} {{ f2_bad_output_type }});
+fails (prove_bisim z3 [] {{ srel }} {{ orel }} {{ f1 }} {{ f2_bad_output_type }});
+
+// Test bad output relation type
+fails (prove_bisim z3 [] {{ srel }} {{ True }} {{ f1 }} {{ f2 }});
 
-// Test bad relation type
-fails (prove_bisim z3 {{ True }} {{ f1 }} {{ f2 }});
+// Test bad state relation type
+fails (prove_bisim z3 [] {{ True }} {{ orel }} {{ f1 }} {{ f2 }});
 
 // Test wrong state type
-fails (prove_bisim z3 {{ rel }} {{ f2 }} {{ f2 }});
+fails (prove_bisim z3 [] {{ srel }} {{ orel }} {{ f2 }} {{ f2 }});

saw-core/src/Verifier/SAW/SharedTerm.hs

@@ -253,6 +253,7 @@ module Verifier.SAW.SharedTerm
 --  , scFalse
    , scOpenTerm
    , scCloseTerm
+   , scLambdaBody
     -- ** Variable substitution
   , instantiateVar
   , instantiateVarList
@@ -2589,7 +2590,6 @@ scGeneralizeExts sc exts x = loop (zip (inits exts) exts)
     -- base case, convert all the exts in the body of x into deBruijn variables
     loop [] = scExtsToLocals sc exts x
 
-
 scUnfoldConstants :: SharedContext -> [VarIndex] -> Term -> IO Term
 scUnfoldConstants sc names t0 = scUnfoldConstantSet sc True (Set.fromList names) t0
 
@@ -2708,3 +2708,14 @@ scCloseTerm close sc ec body = do
     lv <- scLocalVar sc 0
     body' <- scInstantiateExt sc (Map.insert (ecVarIndex ec) lv Map.empty) =<< incVars sc 0 1 body
     close sc (toShortName (ecName ec)) (ecType ec) body'
+
+-- | Compute the body of 0 or more nested lambda-abstractions by applying the
+-- lambdas to fresh 'ExtCns's. Note that we do this lambda-by-lambda, rather
+-- than generating all of the 'ExtCns's at the same time, because later
+-- variables could have types that depend on earlier variables, and so the
+-- substitution of earlier 'ExtCns's has to happen before we generate later
+-- ones.
+scLambdaBody :: SharedContext -> Term -> IO Term
+scLambdaBody sc (asLambda -> Just (nm, tp, body)) =
+  scOpenTerm sc nm tp 0 body >>= scLambdaBody sc . snd
+scLambdaBody _sc t = return t