Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

need to assert postcondition of [forall statement / containing function] #6029

Open
erniecohen opened this issue Jan 8, 2025 · 0 comments
Open
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@erniecohen
Copy link

Dafny version

4.9.1

Code to produce this issue

type Ord<!T(!new)> = (T,T)->bool
ghost predicate iChain<T(!new)>(o:Ord<T>,c:nat->T) { forall n:nat :: o(c(n),c(n+1)) }
ghost predicate wf<T(!new)>(o:Ord<T>) { forall c:nat->T :: !iChain(o,c) }
type WfO<!T(!new)> = o:Ord<T> | wf(o) witness *
ghost predicate inductiveP<T(!new)>(p:T->bool,o:WfO<T>) { forall t:T | (forall t0:T | o(t,t0) :: p(t0)) :: p(t) }
ghost function iRegress<T(!new)>(p:T->bool,o:WfO<T>,t:T,n:nat):(r:T) requires inductiveP(p,o) && !p(t) decreases n {
    if n == 0 then t else var t1 := iRegress(p,o,t,n-1); var r :| o(t1,r) && !p(r); r
}
ghost function rf<T(!new)>(p:T->bool,o:WfO<T>,t:T):(r:nat->T) requires inductiveP(p,o) && !p(t) ensures iChain(o,r) {
    (n:nat) => iRegress(p,o,t,n)
}
lemma wfi<T(!new)>(p:T->bool,o:WfO<T>,t:T) requires inductiveP(p,o) ensures forall t :: p(t) {
    forall t ensures p(t) { if !p(t) { var ch := rf(p,o,t); assert wf(o); }} 
    //assert forall t :: p(t); // proof diverges without this
}

Command to run and resulting output

No response

What happened?

The last line of the last lemma triggers three problems (when it is removed):

  1. Without the final assertion, the proof not only diverges, but causes Z3 to allocate memory at a rate of about 5Gb/min until the system runs out of memory. Given that there should be no relevant function symbols outside the forall statement (which verifies), it seems that there shouldn't be a matching loop.
  2. The final assertion should not be needed, as it simply repeats the postcondition. This perhaps indicates a triggering issue.
  3. The final assertion should already be assumed at the end of the preceding forall statement, so again should be redundant.

What type of operating system are you experiencing the problem on?

Mac

@erniecohen erniecohen added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Jan 8, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

No branches or pull requests

1 participant