Delay unfolding #928

nilehmann · 2024-12-05T22:26:27Z

Delay unfolding of definitions until after refinement type checking (and before fixpoint encoding). I tested this in vtock and veriasm, and I didn't notice any changes in performance.

There's one change in behavior. The following code

#![allow(unused)]
#![flux::defs {
    fn inc1(x: int) -> int {
        x + 1
    }
}]

#[flux::sig(fn() -> i32[inc1(0)])]
fn moo() -> i32 {
    2
}

previously produced

error[E0999]: refinement type error
  --> attic/playground.rs:10:5
   |
10 |     2
   |     ^ a postcondition cannot be proved
-Ztrack-diagnostics: created at crates/flux-refineck/src/lib.rs:202:10
   |
note: this is the condition that cannot be proved
  --> attic/playground.rs:4:9
   |
4  |         x + 1
   |         ^^^^^
note: inside this call
  --> attic/playground.rs:8:25
   |
8  | #[flux::sig(fn() -> i32[inc1(0)])]
   |                         ^^^^^^^

but now it produces

error[E0999]: refinement type error
  --> attic/playground.rs:10:5
   |
10 |     2
   |     ^ a postcondition cannot be proved
-Ztrack-diagnostics: created at crates/flux-refineck/src/lib.rs:202:10
   |
note: this is the condition that cannot be proved
  --> attic/playground.rs:8:25
   |
8  | #[flux::sig(fn() -> i32[inc1(0)])]
   |                         ^^^^^^^

This is because previously we first unfolded inc1(0) into 0 + 1 and then generated a head 2 = 0 + 1 assigning the span of 0 + 1 to the entire head. With this change, we first generate 2 = inc1(0) assigning it the span of inc1(0). We later unfold it to 2 = 0 + 1 but the span of the entire head doesn't change. We could recover the behavior by having a different type of head for equalities and adjusting spans accordingly after unfolding. However, I don't think this is objectively worse, I found the old behavior a bit confusing.

nilehmann added 3 commits December 6, 2024 08:57

Delay unfolding

ccc54a7

Move some stuff around

66ee036

ASdf

e9908a5

nilehmann force-pushed the nico/delay-unfolding branch from 62bdfdc to e9908a5 Compare December 6, 2024 17:11

nilehmann marked this pull request as ready for review December 6, 2024 17:13

ups

c545c46

nilehmann merged commit bf34120 into main Dec 6, 2024
7 checks passed

nilehmann deleted the nico/delay-unfolding branch December 6, 2024 17:58

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Delay unfolding #928

Delay unfolding #928

nilehmann commented Dec 5, 2024 •

edited

Loading

Delay unfolding #928

Delay unfolding #928

Conversation

nilehmann commented Dec 5, 2024 • edited Loading

nilehmann commented Dec 5, 2024 •

edited

Loading