From 072de66556ead8720502a857e10e02fe7a87bf53 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 31 Aug 2022 13:10:29 -0700 Subject: [PATCH 1/3] In the `goal_eval` and `hoist_ifs_in_goal` tactics, take more care to properly deal with dependencies arising from Pi binders. --- src/SAWScript/Proof.hs | 42 ++++++++++++++++++++++++++---------------- 1 file changed, 26 insertions(+), 16 deletions(-) diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index feefdc367e..ab8b483a86 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -421,41 +421,51 @@ simplifySequent sc ss (HypFocusedSequent (FB hs1 h hs2) gs) = hoistIfsInProp :: SharedContext -> Prop -> IO Prop -hoistIfsInProp sc (Prop p) = do - let (args, body) = asPiList p +hoistIfsInProp sc p = do + (ecs, body) <- unbindProp sc p body' <- case asEqTrue body of Just t -> pure t Nothing -> fail "hoistIfsInProp: expected EqTrue" - ecs <- traverse (\(nm, ty) -> scFreshEC sc nm ty) args - vars <- traverse (scExtCns sc) ecs - t0 <- instantiateVarList sc 0 (reverse vars) body' - t1 <- hoistIfs sc t0 + t1 <- hoistIfs sc body' t2 <- scEqTrue sc t1 t3 <- scGeneralizeExts sc ecs t2 return (Prop t3) +-- | Turn any leading Pi binders in the given prop into +-- fresh ExtCns values, being careful to ensure that +-- dependent types are properly substituted. +unbindProp :: SharedContext -> Prop -> IO ([ExtCns Term], Term) +unbindProp sc (Prop p0) = loop [] [] p0 + where + loop ecs vs p = + case asPi p of + Nothing -> + case vs of + [] -> return ([], p) + _ -> do p' <- instantiateVarList sc 0 vs p + return (reverse ecs, p') + Just (nm, tp, tm) -> + do tp' <- instantiateVarList sc 0 vs tp + ec <- scFreshEC sc nm tp' + v <- scExtCns sc ec + loop (ec:ecs) (v:vs) tm + -- | Evaluate the given proposition by round-tripping -- through the What4 formula representation. This will -- perform a variety of simplifications and rewrites. evalProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop -evalProp sc unints (Prop p) = - do let (args, body) = asPiList p - +evalProp sc unints p = + do (ecs, body) <- unbindProp sc p body' <- case asEqTrue body of Just t -> pure t - Nothing -> fail ("goal_eval: expected EqTrue\n" ++ scPrettyTerm defaultPPOpts p) - - ecs <- traverse (\(nm, ty) -> scFreshEC sc nm ty) args - vars <- traverse (scExtCns sc) ecs - t0 <- instantiateVarList sc 0 (reverse vars) body' + Nothing -> fail ("goal_eval: expected EqTrue\n" ++ scPrettyTerm defaultPPOpts (unProp p)) sym <- Common.newSAWCoreExprBuilder sc st <- Common.sawCoreState sym - (_names, (_mlabels, p')) <- W4Sim.w4Eval sym st sc mempty unints t0 + (_names, (_mlabels, p')) <- W4Sim.w4Eval sym st sc mempty unints body' t1 <- W4Sim.toSC sym st p' - t2 <- scEqTrue sc t1 -- turn the free variables we generated back into pi-bound variables t3 <- scGeneralizeExts sc ecs t2 From a0dcf3e7598ea7d2249d40ca70cf7c8935cf8b08 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 31 Aug 2022 13:15:49 -0700 Subject: [PATCH 2/3] Add a test case for the dangling variables bug. Fixes #1316 --- intTests/test_dangling_hoist/README | 6 ++++++ intTests/test_dangling_hoist/test.saw | 22 ++++++++++++++++++++++ intTests/test_dangling_hoist/test.sh | 1 + 3 files changed, 29 insertions(+) create mode 100644 intTests/test_dangling_hoist/README create mode 100644 intTests/test_dangling_hoist/test.saw create mode 100644 intTests/test_dangling_hoist/test.sh diff --git a/intTests/test_dangling_hoist/README b/intTests/test_dangling_hoist/README new file mode 100644 index 0000000000..1895a2d104 --- /dev/null +++ b/intTests/test_dangling_hoist/README @@ -0,0 +1,6 @@ +This test is related to https://github.com/GaloisInc/saw-script/issues/1316 +Previously, the hoist_ifs_in_goal and goal_eval tactics would not properly +take care of the dependencies arising from Pi binders and this would +result in dangling variables. This test exercises those tactics +with dependent binders to check that this does not occur. + diff --git a/intTests/test_dangling_hoist/test.saw b/intTests/test_dangling_hoist/test.saw new file mode 100644 index 0000000000..efae71c339 --- /dev/null +++ b/intTests/test_dangling_hoist/test.saw @@ -0,0 +1,22 @@ +enable_experimental; + +prove_extcore do { + print_goal; + check_goal; + hoist_ifs_in_goal; + print_goal; + check_goal; + admit "sure"; + } + (parse_core "(x : Integer) -> (y:Integer) -> (z:Integer) -> (b:Bool) -> EqTrue (intEq z (ite Integer b x y)) -> EqTrue (ite Bool b (intEq z x) (intEq z y))"); + + +prove_extcore do { + print_goal; + check_goal; + goal_eval; + print_goal; + check_goal; + admit "sure"; + } + (parse_core "(x : Integer) -> (y:Integer) -> (z:Integer) -> (b:Bool) -> EqTrue (intEq z (ite Integer b x y)) -> EqTrue (ite Bool b (intEq z x) (intEq z y))"); diff --git a/intTests/test_dangling_hoist/test.sh b/intTests/test_dangling_hoist/test.sh new file mode 100644 index 0000000000..0b864017cd --- /dev/null +++ b/intTests/test_dangling_hoist/test.sh @@ -0,0 +1 @@ +$SAW test.saw From 9985cd1b3ffd642eceebe21ffa56e66b53042b48 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 7 Sep 2022 15:46:32 -0400 Subject: [PATCH 3/3] s/unbindProp/unbindAndFreshenProp/g --- src/SAWScript/Proof.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index ab8b483a86..30a488911e 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -422,7 +422,7 @@ simplifySequent sc ss (HypFocusedSequent (FB hs1 h hs2) gs) = hoistIfsInProp :: SharedContext -> Prop -> IO Prop hoistIfsInProp sc p = do - (ecs, body) <- unbindProp sc p + (ecs, body) <- unbindAndFreshenProp sc p body' <- case asEqTrue body of Just t -> pure t @@ -435,8 +435,8 @@ hoistIfsInProp sc p = do -- | Turn any leading Pi binders in the given prop into -- fresh ExtCns values, being careful to ensure that -- dependent types are properly substituted. -unbindProp :: SharedContext -> Prop -> IO ([ExtCns Term], Term) -unbindProp sc (Prop p0) = loop [] [] p0 +unbindAndFreshenProp :: SharedContext -> Prop -> IO ([ExtCns Term], Term) +unbindAndFreshenProp sc (Prop p0) = loop [] [] p0 where loop ecs vs p = case asPi p of @@ -456,7 +456,7 @@ unbindProp sc (Prop p0) = loop [] [] p0 -- perform a variety of simplifications and rewrites. evalProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop evalProp sc unints p = - do (ecs, body) <- unbindProp sc p + do (ecs, body) <- unbindAndFreshenProp sc p body' <- case asEqTrue body of Just t -> pure t