Incorrect/missing translation for non-bool '!'

[simonjwinwood]

Given

pub fn doit(x : usize) -> usize {
    !x
}

Running charon --print-llbc yields

# Final LLBC before serialization:

fn bang_vs_not::doit(@1: usize) -> usize
{
    let @0: usize; // return
    let x@1: usize; // arg #1
    let @2: usize; // anonymous local

    @2 := copy (x@1)
    @0 := ~(move (@2))
    drop @2
    return
}

and running aeneas -dest out -backend lean then results in

[Info ] Imported: bang_vs_not.llbc
[Info ] Generated the partial file (because of errors): out/BangVsNot.lean
[Error] Invalid input for unop
Source: 'src/lib.rs', lines 1:0-3:1

Fir reference,

pub fn doit_works(x : usize) -> usize {
    std::ops::Not::not(x)
}

yields

# Final LLBC before serialization:                                                                                                                          
                                                                                                                                                            
trait core::ops::bit::Not<Self>                                                                                                                             
{
    type Output
    fn not : core::ops::bit::Not::not
}

fn core::ops::bit::{impl core::ops::bit::Not for usize}#2::not(@1: usize) -> usize

impl core::ops::bit::{impl core::ops::bit::Not for usize}#2 : core::ops::bit::Not<usize>
{
    type Output = usize
    fn not = core::ops::bit::{impl core::ops::bit::Not for usize}#2::not
}

fn core::ops::bit::Not::not<Self>(@1: Self) -> Self::Output

fn bang_vs_not::doit_works(@1: usize) -> usize
{
    let @0: usize; // return
    let x@1: usize; // arg #1
    let @2: usize; // anonymous local

    @2 := copy (x@1)
    @0 := core::ops::bit::{impl core::ops::bit::Not for usize}#2::not(move (@2))
    drop @2
    return
}

and

-- ...

namespace bang_vs_not

/- Trait declaration: [core::ops::bit::Not]
   Source: '/rustc/library/core/src/ops/bit.rs', lines 34:0-34:13
   Name pattern: core::ops::bit::Not -/
structure core.ops.bit.Not (Self : Type) where
  Output : Type
  not : Self → Result Output

/- [core::ops::bit::{core::ops::bit::Not for usize}#2::not]:
   Source: '/rustc/library/core/src/ops/bit.rs', lines 61:12-61:30
   Name pattern: core::ops::bit::{core::ops::bit::Not<usize>}::not -/
axiom core.ops.bit.NotUsize.not : Usize → Result Usize

/- Trait implementation: [core::ops::bit::{core::ops::bit::Not for usize}#2]
   Source: '/rustc/library/core/src/ops/bit.rs', lines 57:8-57:23
   Name pattern: core::ops::bit::Not<usize> -/
def core.ops.bit.NotUsize : core.ops.bit.Not Usize := {
  Output := Usize
  not := core.ops.bit.NotUsize.not
}

/- [bang_vs_not::doit_works]:
   Source: 'src/lib.rs', lines 5:0-5:37 -/
def doit_works (x : Usize) : Result Usize :=
  core.ops.bit.NotUsize.not x

end bang_vs_not

more or less as expected (although having something other than an axiom would be nice).

[Nadrieril]

To be precise, ! is always translated to a call to Not::not except for the built-in cases, which are bool and integers. What's missing is the implementation of the builtin for integers.

Btw that should be straightforard to add as long as you know the correct fstar/coq/etc operator to translate it to.

[sonmarcho]

The ! operator on scalars was solved by this PR.

[sonmarcho]

Let me leave aside for now the problem of adding definitions to the Lean library for things like std::ops::Not::not(x)