VSCode extension

[ranjitjhala]

A list of possible improvements for the vscode extensions

• Render function parameter index sorts (currently missing from rcx) (fixed in Pretty print records using field names #927)
• Render compressed-sort-bindings i.e. show a0 a1 a2 a3 a4 : int instead of splitting into separate lines (fixed in VSCODE: Collapse names, remove dup constraints #926)
• Elide duplicate constraints dont show n > 0, n > 0 ... once is enough! (fixed in VSCODE: Collapse names, remove dup constraints #926)
• Render record-fields e.g. n.cols instead of n.0 (fixed in Pretty print records using field names #927) or @vrindisbacher example below
• Render record-indices (fixed in Pretty print records using field names #927)
• Render source-level variable names x, y, z instead of places _1, _2, _3 (pending @Samir-Rashid 's PR) (fixed in Source-level names in JSON trace #930)
• Elide lifetimes e.g. e.g. instead of _1 : &'?5 [&'?6 ∃b0. str[b0]][n] show _1 : &[&∃b0. str[b0]][n] (fixed in Source-level names in JSON trace #930)
• Toggleable records (fixed in NestedString representation for VSCode extension #934)
• Render kvar-solutions solutions
• Elide trivial-existentials e.g. e.g. instead of _1 : &[&∃b0. str[b0]][n] show _1 : &[&str][n]
• Expandable function applications
• More "meaningful" names for refinement indices e.g. derived from source-level variable, instead of a0,a1,... ?

record-indices

Instead of CSV[ CSV { n } ] we should show CSV[ { cols : n } ]

record-fields via @vrindisbacher

For example. If I have:

pub struct SP {
    sp_main: u32,
    sp_main: u32
}

and this is part of a bigger struct like:

pub struct Armv7m {
    sp: SP
}

Then, in constraints I will see something like if old_cpu.0.0 = 0 ∨ ... which is difficult to understand what that corresponds to. Instead I think something like this would be more useful if old_cpu.sp.sp_main = 0 ...

[vrindisbacher]

Just thought of something that I think would be helpful as well. In constraints, sometimes it would be helpful to hide certain clauses joined by conjunctions. Here is a concrete example from something that I'm working on:

I have the following precondition for a function (what it actually means is not so important):

 requires mode_is_thread_privileged(old_cpu.mode, old_cpu.control) && sp_can_handle_exception_entry(old_cpu)

The constraint for this is as follows:

old_cpu.7.0 = 1 ∧ ¬old_cpu.2.1 ∧ (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0, (bv_int_to_bv32)(32)) }, old_cpu.1.1 } } else { SP { old_cpu.1.0, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0, (bv_int_to_bv32)(32)) } } }.0 } else { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0, (bv_int_to_bv32)(32)) }, old_cpu.1.1 } } else { SP { old_cpu.1.0, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0, (bv_int_to_bv32)(32)) } } }.1 }.0) ≥ armv7m::mem::RAM_START ∧ (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0, (bv_int_to_bv32)(32)) }, old_cpu.1.1 } } else { SP { old_cpu.1.0, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0, (bv_int_to_bv32)(32)) } } }.0 } else { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0, (bv_int_to_bv32)(32)) }, old_cpu.1.1 } } else { SP { old_cpu.1.0, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0, (bv_int_to_bv32)(32)) } } }.1 }.0) ≤ armv7m::mem::RAM_END ∧ (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0) ≥ armv7m::mem::RAM_START ∧ (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 }.0) ≤ armv7m::mem::RAM_END

where

 old_cpu.7.0 = 1 ∧ ¬old_cpu.2.1

corresponds to mode_is_thread_privileged(old_cpu.mode, old_cpu.control) while the rest corresponds to sp_can_handle_exception_entry(old_cpu).

It would be extremely helpful in contexts like this if we could have the option to hide the constraint that corresponds to a specific surface level function. e.g. I don't want to see sp_can_handle_exception_entry(old_cpu) anymore. Or maybe I don't even want to see the constraint that corresponds to this precondtion?

[vrindisbacher]

In a similar vein as above, it might be nice to be able to hide these sorts of things in postconditions as well. I'm trying to debug something not checking and there is a very very specific field that I am interested in but it is cluttered by others.

My postcondition looks like this:

ensures self: Armv7m { new_cpu: get_gpr(r0(), new_cpu) == bv32(10) }

but the constraint looks like:

Armv7m { a0, SP { BV32 { a1 }, BV32 { a2 } }, Control { a3, a4 }, BV32 { a5 }, BV32 { a6 }, BV32 { a7 }, Memory { a8 }, CPUMode { a9 } } = Armv7m { (map_store)((map_store)(old_cpu.0, GPR { 0 }, BV32 { (bv_int_to_bv32)(10) }), GPR { 0 }, (map_select)((map_store)(old_cpu.6.0, (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.0 } else { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.1 }.0), (map_select)((map_store)(old_cpu.0, GPR { 0 }, BV32 { (bv_int_to_bv32)(10) }), GPR { 0 })), if BV32 { (bv_int_to_bv32)(4294967289) } = BV32 { (bv_int_to_bv32)(68719476729) } { (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.0.0) } else { (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.1.0) })), if BV32 { (bv_int_to_bv32)(4294967289) } = BV32 { (bv_int_to_bv32)(68719476729) } { SP { BV32 { (bv_add)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.0.0, (bv_int_to_bv32)(32)) }, if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.1 } } else { SP { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.0, BV32 { (bv_add)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.1.0, (bv_int_to_bv32)(32)) } } }, Control { old_cpu.2.0, BV32 { (bv_int_to_bv32)(4294967289) } ≠ BV32 { (bv_int_to_bv32)(4294967289) } }, (map_select)((map_store)(old_cpu.6.0, (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.0 } else { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.1 }.0), (map_select)((map_store)(old_cpu.0, GPR { 0 }, BV32 { (bv_int_to_bv32)(10) }), GPR { 0 })), if BV32 { (bv_int_to_bv32)(4294967289) } = BV32 { (bv_int_to_bv32)(68719476729) } { (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.0.0) } else { (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.1.0) } + 20), BV32 { old_cpu.4.0 }, (map_select)((map_store)(old_cpu.6.0, (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.0 } else { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.1 }.0), (map_select)((map_store)(old_cpu.0, GPR { 0 }, BV32 { (bv_int_to_bv32)(10) }), GPR { 0 })), if BV32 { (bv_int_to_bv32)(4294967289) } = BV32 { (bv_int_to_bv32)(68719476729) } { (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.0.0) } else { (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.1.0) } + 28), Memory { (map_store)(old_cpu.6.0, (bv_bv32_to_int)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.0 } else { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { SP { BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) }, BV32 { old_cpu.1.1.0 } } } else { SP { BV32 { old_cpu.1.0.0 }, BV32 { (bv_sub)(if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { BV32 { old_cpu.1.0.0 } } else { BV32 { old_cpu.1.1.0 } }.0, (bv_int_to_bv32)(32)) } } }.1 }.0), (map_select)((map_store)(old_cpu.0, GPR { 0 }, BV32 { (bv_int_to_bv32)(10) }), GPR { 0 })) }, CPUMode { 1 } }

which is just not parseable.

I think there are two things that might be helpful here:

1. Allowing a user to toggle the constraint to be showed in terms of the higher level surface syntax.
   • I'm honestly not sure this is possible but I figured I'd just put it out there.
2. Allowing a user to hide fields they don't care about.
   • In the example above, I only care about a0 on the left side and it's corresponding constraint on the right side. I don't want to look at the rest of the fields because they are not related to my postcondition.

[ranjitjhala]

Even the other thing (collapse to higher-level syntax) I think we could do if we changed the representation of Expr to "record" the provenance. So using (ahem) Haskell syntax

data Expr 
  = EVar Var | ECon Con | EBin Op Expr Expr | EApp Var [Expr] | ...
  |  EFrom Expr Var [Expr]

So if you had definitions

fn foo(x, y) { x + 10 < y }
fn bar(a, b) { foo(a, 2*b) } 

Consider a constraint bar(n, n + 1)

CURRENTLY: Gets "expanded" to foo(n, 2*(n+1)) and then to n + 10 < 2 * (n + 1)

PROPOSED: Gets "expanded" to (( n + 10 < 2 * (n+1) ) from foo(n, 2*(n+1)) from bar(n, n + 1)

Where each "application" / "expansion" explicitly records where it came from.

When sending to fixpoint, we just erase the From i.e. EFrom e f arg is just the same as e

When rendering however, we can hold onto that structure and do various things in vscode...

[nilehmann]

we currently normalize expressions (i.e., beta reduce functions) eagerly after conversion and then do refinement type checking with expressions normalized. I don't think we need to, we could do refinement type checking without normalizing and delay the normalization to before fixpoint encoding. As a matter of fact, we need to stop evaluating functions eagerly if we ever want to support recursive definitions.

[ranjitjhala]

Do we carry the definitions all the way forward? It may be most compact to defer unfolding stuff all the way till the end... or even just leave it to fixpoint ...

[nilehmann]

A couple of things are in place here that make the constraints/types hard to read.

1. We are expanding user-defined abstractions. This could be fundamentally solved by delaying the unfolding as hinted above (or letting fixpoint do the unfolding).
2. Flux likes to eta expand things, e.g,, if you have

   #[refined_by(x: int, y: int)]
   struct S { ... }

   and then declare a parameter a of sort S, we don't simply add a: S to the environment but instead add x: int, y: int and then replace the occurrences of a with S{ x, y }. This is done recursively and that's why Armv7 is hard to read. We mostly do this for historical reasons and I believe we could stop doing it. If anything, we should do it during fixpoint encoding or as a pass on the constraint and not during refinement type checking.
3. This is minor and very specific for this case but it's annoying that Bv32 is a data sort with a bit-vector as a single field and not the bit vector itself. I've been thinking for a while that we could have an #[indexed_by(sort)] annotation that indexes the type directly by the sort as opposed to #[refined_by()] that implicitly declares a data sort and then indexes the type by it.

[vrindisbacher]

indexed_by would be awesome!

[ranjitjhala]

Btw @nilehmann - I think for all these fancier selective show/hide -- presumably we should render the flux information as some sort of structured JSON and deal with show/hide in the vscode-extension, yes?

[nilehmann]

yeah probably the most flexible would be to do the "rendering" in vscode for which we would need to serialize types. I was thinking that we could share some of the code by implementing the logic in Rust and compiling it to wasm (assuming that's a thing in vscode)

Alternatively, we could implement an lsp-server in Rust and do the rendering server-side.

[ranjitjhala]

wasm?! This may be relevant https://code.visualstudio.com/blogs/2024/05/08/wasm

[nilehmann]

I tried to implement point 2 in #922 (reply in thread), but veriasm hangs if we stop eta-expanding data sorts. We can do the same we did with unfolding and implement it as a pass on the constraint, but this requires meddling with the structure of the RefineTree, i.e., adding more foralls. This is not too hard but needs some considerations, because, for example, we assume in various parts that all the names in a path in the tree are contiguous.

[ranjitjhala]

Hmm not following this entirely? One method that would be compatible with the NestedString route is to have a new ExprKind

   ExpApp(Expr, Expr, List<Expr>)

where we just "record" what the folded version was, so we still do the expansion in flux, exactly as is in main now, except

1. during expansion wherever we currently expand App(f, args) to e we instead expand it to ExpApp(e, f, args)
2. in the fixpoint encoding, we just "erase" the f and args ... i.e. use the expanded e (recursively)
3. during the rendering we can print f(args) and, on clicking, give the definition (interactively).

[nilehmann]

This is not related to unfolding definitions; that part is already implemented, and you already get folded definitions in the checker trace. This is about eta expanding structs. For example, suppose you have

#[refined_by(x: int, y: int)]
struct S {
    #[field(i32[x])]
    x: i32,
    #[field(i32[y])]
    y: i32,
}

fn foo(x: S) { ... }

The normal way to initialize the context when checking foo would be

Φ := a0: S
Γ := x: S[a0] 

but we instead do

Φ := a0: int, a1: int
Γ := x: S[{x: a0, y: a1}]

If S has nested structs that easily becomes unreadable.

It turns out that if we blindly stop doing it z3 doesn't like it and veriasm hangs. But we can still do it after refinement type checking the same way we now unfold definitions after refinement type checking.

[ranjitjhala]

@vrindisbacher I added nested/toggleable fields to the vscode-flux thing, lmk if that helps!

[vrindisbacher]

Awesome! I'll take a look in a bit.