Matching on enum inside `flux::sig(...)`?

[enjhnsn2]

I have an opaque wrapper struct used to represent pointers in Tock:

#[flux_rs::opaque]
#[derive(Clone, Copy, Debug, PartialOrd, Ord, PartialEq, Eq)]
#[flux_rs::refined_by(ptr: int)]
pub struct FluxPtr {
    inner: *mut u8,
}

However, comparisons do not work when using this wrapper. The following code:

pub fn compare_fluxptr(p1: FluxPtr, p2: FluxPtr) -> bool {
    if p1 < p2 {
        return false;
    }
    assert(p1 >= p2);
    true
}

fails with:

error[E0999]: refinement type error
   --> src/main.rs:370:5
    |
370 |     assert(p1 >= p2);
    |     ^^^^^^^^^^^^^^^^ a precondition cannot be proved
=

This is because FluxPtr is opaque and Flux has no way to know that for the comparison self: &FluxPtr[@self_index] < other: &FluxPtr[@other_index] that self < other => self_index < other_index

I tried to fix this by implementing the cmp function myself instead of deriving it:

#[flux_rs::trusted]
impl Ord for FluxPtr {
    #[flux::sig(fn(self: &Self[@s], other: &Self[@o]) -> Ordering {
        order: order == Ordering::Less => s < o &&
               order == Ordering::Equal => s == o && 
               order == Ordering::Greater => s > 0
    })]
    fn cmp(&self, other: &Self) -> Ordering {
        self.inner.cmp(&other.inner)
    }
}

However this fails with:

error[E0999]: cannot find value `Ordering::Less` in this scope
   --> src/main.rs:299:25
    |
299 |         order: order == Ordering::Less => s < o &&
    |                         ^^^^^^^^^^^^^^ not found in this scope

Is it possible to match on enum variants within a flux signature? Alternately, do you have any suggestions about handling comparisons on opaque structs?

[nilehmann]

Sadly no :(

The only way now is to refine Ordering by an int.

use std::cmp::Ordering;

#[flux_rs::extern_spec]
#[flux_rs::refined_by(val: int)]
#[flux_rs::invariant(val == -1 || val == 0 || val == 1)]
enum Ordering {
    #[flux::variant(Ordering[-1])]
    Less,
    #[flux::variant(Ordering[0])]
    Equal,
    #[flux::variant(Ordering[1])]
    Greater,
}

#[flux_rs::opaque]
#[flux_rs::refined_by(n: int)]
struct Wrapper {
    x: *mut u8
}

#[flux_rs::trusted]
impl Wrapper {
    #[flux_rs::sig(
        fn(self: &Wrapper[@lhs], other: &Wrapper[@rhs]) -> Ordering{val: val == -1 => lhs < rhs && 
                                                                         val == 0 => lhs == rhs && 
                                                                         val == 1 => lhs > rhs}
    )]
    fn cmp(&self, other: &Wrapper) -> Ordering {
        todo!()
    }
}

My idea for stuff like this is to implement a feature that let you mark an enum (without payload for now) with #[flux::reflect] such that it becomes something in the logic you can use.

[enjhnsn2]

Is this something I could do on an extern_spec of Ordering? Otherwise I'd have to rewrite every pointer comparison in flux.

[nilehmann]

yes, what I wrote should work see https://flux.programming.systems/?code=tVJNT8MwDL3nV3iaVLVok9YbCmzigrggceRQVVNY3S1Smnb5GEVb_ztJaUs3BBwQviS2n5_j50wnCROifA2ttBqzKCXEnaBNRummqCh9UhkqLrc3hEyTXNh6rTSlWBtUcq0r3KTjuMKcS8zWL2_hgQkKXJroDMDlgSnOpPF5WC5hHsPpBJ2zGN1jV4jSFtC_AI4EnH2QUdrz9OlkHqeuxEMeUevZz-BFj73fWyZ-AQ_EDwqZG3xGGnImR1mxvcXvlJC9DtoouzHwrFhVoermqSlcFdaAvfasIwYH1gazlPCiEhdFI5jm27CNectlqFHkFIIOn9yJnU5nUJodqnFYuXAE89Ug77Fd2OdWlitwpXALDglBAEOPP9uw7K6Fu_9Xj2GMlW_RtPzdLnMJ7oOHgdfriz5nynSaezNlVk7CqPUb0rwD

[nilehmann]

@enjhnsn2 I'am looking at the mir produced by your example and calling < and >= uses PartialOrd::lt and PartialOrd::ge so you should refine those and it's not necessary to refine Ord::cmp

[enjhnsn2]

cool, I'll try that and let you know how it works

[enjhnsn2]

Cool, both the extern_spec on Ordering and refining le,lt,ge,gt works. I'll post my implementation before closing:

#[flux_rs::trusted]
impl PartialOrd for FluxPtr {
    fn partial_cmp(&self, other: &Self) -> Option<Ordering>{todo!()}

    #[flux_rs::sig(fn(self: &Self[@lhs], other: &Self[@rhs]) -> bool[lhs < rhs])]
    fn lt(&self, other: &Self) -> bool { todo!() }
    #[flux_rs::sig(fn(self: &Self[@lhs], other: &Self[@rhs]) -> bool[lhs <= rhs])]
    fn le(&self, other: &Self) -> bool { todo!() }
    #[flux_rs::sig(fn(self: &Self[@lhs], other: &Self[@rhs]) -> bool[lhs > rhs])]
    fn gt(&self, other: &Self) -> bool { todo!() }
    #[flux_rs::sig(fn(self: &Self[@lhs], other: &Self[@rhs]) -> bool[lhs >= rhs])]
    fn ge(&self, other: &Self) -> bool { todo!() }
}