From 3e3b1ff460a54afa90836a0021f840b765f13dde Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Tue, 7 Nov 2023 11:30:26 -0800 Subject: [PATCH] Apply suggestions from code review Co-authored-by: Ryan Scott --- doc/manual/manual.md | 6 +++--- intTests/test_bisimulation/comp.saw | 4 ++-- src/SAWScript/Bisimulation/BisimTheorem.hs | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/doc/manual/manual.md b/doc/manual/manual.md index d7d65dddd6..a64dd00510 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -4048,7 +4048,7 @@ of a circuit and a functional specification. SAW enables these proofs with the experimental `prove_bisim` command: ~~~~ -prove_bisim : ProofScript () -> [BisimTheorem] -> Term -> Term -> Term -> Term -> TopLevel ProofResult +prove_bisim : ProofScript () -> [BisimTheorem] -> Term -> Term -> Term -> Term -> TopLevel BisimTheorem ~~~~ When invoking `prove_bisim strat theorems srel orel lhs rhs`, the arguments @@ -4290,9 +4290,9 @@ 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. +terms simulate each other. -When using composition, the `prove_bisim` also generates and attempts to solve +When using composition, `prove_bisim` also generates and attempts to solve the proof goal below for any successfully applied `BisimTheorem` in the `theorems` list: diff --git a/intTests/test_bisimulation/comp.saw b/intTests/test_bisimulation/comp.saw index 286da416cb..b9a96720e9 100644 --- a/intTests/test_bisimulation/comp.saw +++ b/intTests/test_bisimulation/comp.saw @@ -4,7 +4,7 @@ import "Comp.cry"; enable_experimental; -// Prove 'andImp' and 'andSpec' simulate eachother +// Prove 'andImp' and 'andSpec' simulate each other and_res <- prove_bisim z3 [] {{ andStateRel }} @@ -12,7 +12,7 @@ and_res <- prove_bisim z3 {{ andImp }} {{ andSpec }}; -// Prove 'nandImp' and 'nandSpec' simulate eachother, using 'and_res' in the +// Prove 'nandImp' and 'nandSpec' simulate each other, using 'and_res' in the // process. nand_res <- prove_bisim (do { unfolding ["nandImp", "nandSpec"]; diff --git a/src/SAWScript/Bisimulation/BisimTheorem.hs b/src/SAWScript/Bisimulation/BisimTheorem.hs index 5d7f17cfe2..fd95b5dedd 100644 --- a/src/SAWScript/Bisimulation/BisimTheorem.hs +++ b/src/SAWScript/Bisimulation/BisimTheorem.hs @@ -12,8 +12,8 @@ module SAWScript.Bisimulation.BisimTheorem import qualified Cryptol.TypeCheck.Type as C import Verifier.SAW.TypedTerm ( TypedTerm ) --- A proved bisimulation theorem. See the comment at the top of --- 'SAWScript.Bisimulation' for an explanation of some of the terms used here. +-- | A proved bisimulation theorem. See the comment at the top of +-- "SAWScript.Bisimulation" for an explanation of some of the terms used here. data BisimTheorem = BisimTheorem { bisimTheoremStateRelation :: TypedTerm -- ^ State relation