Skip to content

Commit

Permalink
Merge pull request #1736 from GaloisInc/dangling-vars
Browse files Browse the repository at this point in the history
Dangling vars
  • Loading branch information
mergify[bot] authored Sep 13, 2022
2 parents a07490d + 4750250 commit e6a3e62
Show file tree
Hide file tree
Showing 4 changed files with 55 additions and 16 deletions.
6 changes: 6 additions & 0 deletions intTests/test_dangling_hoist/README
Original file line number Diff line number Diff line change
@@ -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.

22 changes: 22 additions & 0 deletions intTests/test_dangling_hoist/test.saw
Original file line number Diff line number Diff line change
@@ -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))");
1 change: 1 addition & 0 deletions intTests/test_dangling_hoist/test.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
$SAW test.saw
42 changes: 26 additions & 16 deletions src/SAWScript/Proof.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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) <- unbindAndFreshenProp 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.
unbindAndFreshenProp :: SharedContext -> Prop -> IO ([ExtCns Term], Term)
unbindAndFreshenProp 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) <- unbindAndFreshenProp 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
Expand Down

0 comments on commit e6a3e62

Please sign in to comment.