Did a quick impromptu talk on flux

[nihalpasham]

Over the weekend, I decided to do an impromptu talk on functional correctness and ended up exploring flux (just the basics).

https://bit.ly/3jTrASs

One question that popped up after the talk was - is flux being used in a real (production) project and if yes, what's the experience been like?

[ranjitjhala]

Hi @nihalpasham --

Awesome, looking forward to seeing the whole talk!!!

To your question: as far as I know, no -- or not yet!

I suspect flux is still not yet sufficiently mature. For example, right now we're working
on adding support for closures. Still, if there are particular use cases you have in mind
would love to chat. In fact we were just talking the other day about how various constraints
in the embedded domain may be ripe for encoding as refinements, so this is particularly timely.

• Ranjit.

[nilehmann]

This is awesome @nihalpasham! I just finished watching the talk. It's great to see a perspective on flux from the outside.

As Ranjit said, there are currently no real/production projects as the tool is not yet sufficiently mature (we are getting there). But we are in a stage where we are looking for real projects to verify. I found the application to parsers mentioned in the talk particularly compelling. We would love to chat about this or any other particular use cases you may have in mind.

[nihalpasham]

A couple of embedded use-cases I can think of - the first two (I guess) involve usize refining,

• memory mapped IO: i.e. all hardware access in an embedded-device (such as a microcontroller) is usually memory-mapped i.e. registers for an mcu peripheral can be simply read-from or written-to a predefined memory-address range. For example: uart controller, interrupt controller, crypto accelerator, all have vendor-designated memory address ranges dedicated to each of them. These address ranges are usually just defined as constants and used as bounds but its pretty easy to make mistakes. The other use-case I see here is catching invalid (values for) register writes.
• bounds checked control-flow: like the example from the talk
• parsers: rustBoot (a project of mine) is a secure bootloader. It uses a relatively straightforward type-length-value (or tlv) encoding parser to parse a 256 byte header that contains (among other things) a firmware digest and signature. My goal was to functionally verify the parser, more specifically the extractors here. The parser uses nom - a parser-combinator framework that works in a no_std environment.

I'm assuming this may already be the case but just thought I'd check -can flux provide hints/info for translating or encoding validations/refinements at the rust type-level i.e apart from the ability to annotate rust code with flux-specs to test functional properties (which is awesome)

example, in the snippet of code below, flux shows a post-condition error at compile time, which is great but if for some reason the developer doesn't catch this, the rust compiler is still going to compile this.

#[flux::sig(
    fn<p: int -> bool>(x: i32, y: i32) -> i32{v: p(v) && v >= x && v >= y}
    requires p(x) && p(y)
)]
fn max(x: i32, y: i32) -> i32 {
    if x > y {
        x
    } else {
        y
    }
}

#[flux::sig(fn(x: i32, y: i32) -> i32{v: v % 2 == 0})]
fn modulo_max(x: i32, y: i32) -> i32 {
    max(4, 5)
}

[nihalpasham]

Hi, just re-trying

any pointers on this question?

I'm assuming this may already be the case but just thought I'd check -can flux provide hints/info for translating or encoding validations/refinements at the rust type-level i.e apart from the ability to annotate rust code with flux-specs to test functional properties (which is awesome)

example, in the snippet of code below, flux shows a post-condition error at compile time, which is great but if for some reason the developer doesn't catch this, the rust compiler is still going to compile this.

#[flux::sig(
    fn<p: int -> bool>(x: i32, y: i32) -> i32{v: p(v) && v >= x && v >= y}
    requires p(x) && p(y)
)]
fn max(x: i32, y: i32) -> i32 {
    if x > y {
        x
    } else {
        y
    }
}

#[flux::sig(fn(x: i32, y: i32) -> i32{v: v % 2 == 0})]
fn modulo_max(x: i32, y: i32) -> i32 {
    max(4, 5)
}

[nilehmann]

Thank you for following up on this.

I'm not sure I completely understand the question but I'm just going to say what comes to mind.

There's currently no way to prevent your code from compiling if there's a flux error. This is partially by design. We don't want flux to be a hard dependency because our experience with liquid haskell is that people have some fear of vendor lock-in. So, one of our design goals is that your code should compile just fine without flux. Of course, you could mitigate missing errors by adding flux to the ci.

That being said, flux is a compiler driver so it would be relatively easy to implement a mode in which you can use it as a drop-in replacement for rustc/cargo in a way that will prevent your code from compiling if there's a refinement error (more like a compiler plugin). A tighter integration with the compiler pipeline, e.g., using refinement information during code generation for optimizations, is something we haven't explored but I assume will make people even more suspicious.

On a more technical level, having flux run as a completely separate analysis from compilation gives us some flexibility to tweak the generated mir code we analyze. For example, we can generate semantically equivalent code which is easier to analyze but you wouldn't want to compile.

[nilehmann]

* **memory mapped IO:** i.e. all hardware access in an embedded-device (such as a microcontroller) is usually memory-mapped i.e. registers for an `mcu` peripheral can be simply read-from or written-to a predefined memory-address range. For example: `uart` controller, `interrupt` controller, `crypto` accelerator, all have `vendor-designated` memory address ranges dedicated to each of them. These address ranges are usually just defined as constants and used as bounds but its pretty easy to make mistakes. The other use-case I see here is catching invalid (values for) register writes.

* **bounds checked control-flow:** like the example from the talk

* **parsers:** [rustBoot](https://github.com/nihalpasham/rustBoot) (a project of mine) is a secure bootloader. It uses a relatively straightforward `type-length-value` (or tlv) encoding parser to parse a [256 byte header](https://nihalpasham.github.io/rustBoot-book/arch/images.html#mcu-image-format) that contains (among other things) a firmware digest and signature. My goal was to functionally verify the parser, more specifically the `extractors` [here](https://github.com/nihalpasham/rustBoot/blob/a5edc3e9af4282bee34f3e9e9470e4accf8fc087/rustBoot/src/parser.rs#L170). The parser uses [nom](https://github.com/rust-bakery/nom) - a parser-combinator framework that works in a no_std environment.

The first two use cases sound like should be relatively easy to handle with flux. How does the memory-mapped IO work in practice? Is there some library people use to abstract over the hardware? One effective way of using refinement types is to provide a refined api, so a good starting point would be to take an existing library and see if one can drop refinements on top of it.

I'm still intrigued about the parsers. Can you elaborate a bit on what specific properties you want to verify?

[nihalpasham]

The first two use cases sound like should be relatively easy to handle with flux.

I agree. this is like some low hanging fruit. flux is pretty helpful for these cases.

How does the memory-mapped IO work in practice? Is there some library people use to abstract over the hardware?

there is no 'one' library per-se. It varies depending on the micro-architecture, available tooling and documentation. For example, here is a serial driver I implemented using memory mapped IO. In practice, for a given development-board (in this case a rpi4), we get the board's datasheet, create register definitions for the peripheral and start accessing IO. But sometimes, these crates tend to have a large number of peripherals (and consequently a large number of register addresses) which can get tedious and introduce errors (as we're hand-coding this)

One effective way of using refinement types is to provide a refined api, so a good starting point would be to take an existing library and see if one can drop refinements on top of it.

this was kind of my goal with the bounds-checking example from the talk. But my impl mostly involved runtime checks. It would be cool if we were use flux's errors to build a template for writing good bounds checks that can be checked at compile time.

I'm still intrigued about the parsers. Can you elaborate a bit on what specific properties you want to verify?

For the parser, my starting goals are as follows,

• check if initial input (header) supplied is equal to 256 bytes (i.e. a rust slice)
• if byte-indexes have pre-designated values
• and subsequent parsing (i.e. as we parse each field), we keep checking if the header's length is equal to an expected length.

[nilehmann]

@nihalpasham I tried to teach myself some embedded over the weekend and went over the rust embedded book . To check if I'm following, the code you are linking here corresponds (roughly) to what they call the PAC? If so, then there's no way around writing that layer either manually or automatically with something like svd2rust, correct?

If all of this makes sense, then my follow-up question is: after writing that layer what else can go wrong?

[nihalpasham]

@nihalpasham I tried to teach myself some embedded over the weekend and went over the rust embedded book . To check if I'm following, the code you are linking here corresponds (roughly) to what they call the PAC?

This is correct.

However, the option to automate PAC-building is not available in all cases as 'pacs' are built using 'svd' files. While we can procure an svd file for many cortex-m mcus, the same is not available for cortex-a (based) SoCs.

The premise I was working with is - can we build this layer using refined types to avoid all the macro work involved in the current set of apis (as using the macro-based api is quite tedious and usage is not always as obvious as regular rust code)

So, something like the following

• construct refined-usize types for each memory mapped peripheral with sub-refinements for each register within the peripheral
• construct accessor methods (with read-modify-write semantics) for these types

I have not gotten around to it yet but I assume this should be possible- right

The other use case for which I have a vague picture is 'bit patterns'. To elaborate - some peripheral registers are supposed hold a set of valid bit patterns (or values). This is either something the developer wants to enforce for security or performance reasons or the reference manual says that using an invalid value here can lead to instability or undefined behaviour.

[nilehmann]

However, the option to automate PAC-building is not available in all cases as 'pacs' are built using 'svd' files. While we can procure an svd file for many cortex-m mcus, the same is not available for cortex-a (based) SoCs.

The premise I was working with is - can we build this layer using refined types to avoid all the macro work involved in the current set of apis (as using the macro-based api is quite tedious and usage is not always as obvious as regular rust code)

Yeah assumed the svd option may not always be available, but I also assumed that since you have to create the layer anyways, it's something you just need to deal with even if it is a manual process But you are totally right, even if it is a painful manual process, there's no reason you couldn't get some help to get it right.

So, something like the following

* construct refined-usize types for each memory mapped peripheral with sub-refinements for each register within the peripheral

* construct accessor methods (with read-modify-write semantics) for these types

I don't quite follow. What is a sub-refinement in this case? Do you have an idea on how the code should look like? Even if it is not valid flux, seeing some code would help me understand.

The other use case for which I have a vague picture is 'bit patterns'. To elaborate - some peripheral registers are supposed hold a set of valid bit patterns (or values). This is either something the developer wants to enforce for security or performance reasons or the reference manual says that using an invalid value here can lead to instability or undefined behaviour.

This is a good point. I came across this while reading the embedded book. If I understand correctly svd2rust will create an unsafe function in those cases. Are these restrictions in practice really arbitrary bit patterns or they follow some structure? We don't have support right now for encoding integers as bit vectors, but we knew they will become necessary at some point, maybe this is the time to implement it.

[nihalpasham]

[I've been out sick for a while ..]

In terms of pseudo-code: something (pretty) basic along these lines

#[flux::sig(v:Min<=v && Max<=v)]
struct RefinedUsize{
      v: u32
}

I can then use the (above) refined-type definition in code to define a registerblock or a register within that block (a further sub-refinement) or an address-range. Right now, the only available option (I've come up with) is a runtime check, like the one below

struct RefinedUsize<const MIN: u32, const MAX: u32, const VAL: u32>(u32);

impl<const MIN: u32, const MAX: u32, const VAL: u32> RefinedUsize<MIN, MAX, VAL> {
    pub fn bounded_int(i: u32) -> Self {
        assert!(i >= MIN && i <= MAX);
        RefinedUsize(i)
    }
    pub fn single_valued_int(i: u32) -> Self {
        assert!(i == VAL);
        RefinedUsize(i)
    }
}

#[rustfmt::skip]
pub fn boot_from(fw_base_address: usize) -> ! {
    let mut core_peripherals = hal::pac::CorePeripherals::take().unwrap();
    let mut scb = core_peripherals.SCB;
    unsafe {
        let base_img_addr = fw_base_address as u32;
        let stack_pointer = RefinedUsize::<STACK_LOW, STACK_UP, 0>::bounded_int(
            *(fw_base_address as *const u32)).0;
        let reset_vector = RefinedUsize::<0, 0, FW_RESET_VTR>::single_valued_int(
            *((fw_base_address + 4) as *const u32)).0;
        let jump_vector = core::mem::transmute::<usize, extern "C" fn() -> !>(reset_vector as usize);

        cortex_m::asm::dsb();
        cortex_m::asm::isb();
        scb.vtor.write(base_img_addr);
        cortex_m::register::msp::write(stack_pointer);
        jump_vector()
    }
}

This doesn't compose very well either like say if I want additional conditional refinements.