Improve Pre- and Post-Conditions on `impl` blocks

[karthikbhargavan]

trafficstars

When writing the following contracts on an impl block, several errors are triggered:

#[hax_lib::attributes]
impl<const N: usize> TryDecodeOps<U8> for [U32; N] {
    #[hax_lib::requires(N < 65536 / 4)]
    #[hax_lib::ensures(|result| if x.len() == N * 4 {result.is_ok()} else {result.is_err()})] 
    fn try_from_le_bytes(x:&[U8]) -> Result<Self,()> {
        try_from_le_bytes(x)
    }
    #[hax_lib::requires(N < 65536 / 4)]
    #[hax_lib::ensures(|result| if x.len() == N * 4 {result.is_ok()} else {result.is_err()})] 
    fn try_from_be_bytes(x:&[U8]) -> Result<Self,()> {
        try_from_be_bytes(x)
    }
}

First, we must remove the hax_lib:: prefix from all the pre- and post-conditions inside the impl.

Second, we must remove Self and replace it by [U32; N]

Third, in the generated F* code, the pre-condition is not provided to the post-condition, so we end up having to repeat the pre-condition in the post-condition.

The version that works after these changes is the following:

#[hax_lib::attributes]
impl<const N: usize> TryDecodeOps<U8> for [U32; N] {
    #[requires(N < 65536 / 4)]
    #[ensures(|result| N < 65536 / 4 && (if x.len() == N * 4 {result.is_ok()} else {result.is_err()}))] 
    fn try_from_le_bytes(x:&[U8]) -> Result<[U32; N],()> {
        try_from_le_bytes(x)
    }
    #[requires(N < 65536 / 4)]
    #[ensures(|result| N < 65536 / 4 && (if x.len() == N * 4 {result.is_ok()} else {result.is_err()}))] 
    fn try_from_be_bytes(x:&[U8]) -> Result<[U32; N],()> {
        try_from_be_bytes(x)
    }
}

Individual issues:

• #782
• #783
• #784