Properly axiomatizing foreign functions

Stream: lean4

[James Gallicchio]

Currently trying to learn how to build reasonable FFIs (in my case, for not-dynamic arrays).

I came across the definition of USize.ofNat (here)[https://github.com/leanprover/lean4/blob/da4ad465d0a8a1267268def14af779ea0244f78e/src/Init/Data/UInt.lean#L285] and am a bit confused by it

• The Lean definition mods by the system usize (which I don't think is ever the desired use-case here?)
• I'm pretty sure the C definition panics if the nat can't fit in a usize (which I think is the desired behavior)

Why was this definition chosen instead of making an opaque constant or, at most, an unsafe function which panics on too-large inputs? Right now the behaviors just don't match up, which seems like a recipe for issues

[James Gallicchio]

The C definition is across a few places:
https://github.com/leanprover/lean4/blob/35e623fca0b949b373fac42063881f606c7abbe0/src/include/lean/lean.h#L1661
https://github.com/leanprover/lean4/blob/412691c9581138028e9a98e1b7c99dd136cefed8/src/runtime/object.cpp#L1521
and here I get stuck, since I don't know where these definitions came from. Maybe this does actually mod?

[James Gallicchio]

Okay, I guess my actual question is whether there's a different function somewhere I can use that unsafe converts Nat to USize, panicking if it is too large

[Tomas Skrivan]

You can define your own function that does that:

def Nat.toUSize! (n : Nat) : USize :=
  if n < USize.size then
    n.toUSize
  else
    panic! s!"Integer {n} is to larget for usize"

#eval (USize.size-1).toUSize! -- PANIC at toUSize doodle:9:4: Integer 18446744073709551616 is to larget for usize
#eval (USize.size).toUSize!   -- 18446744073709551615

If you want to have something that is really safe, I would expect to always provide a proof that provided Nat fits to usize

def Nat.toUSizeSafe (n : Nat) (h : n < USize.size) : USize := ⟨n,h⟩

#eval (USize.size - 1).toUSizeSafe (by native_decide)

But I have a feeling I'm misunderstanding your question.

[James Gallicchio]

Tomas Skrivan said:

You can define your own function that does that:

Yeah, I can write my own, but was wondering why the disparity on this definition

[Mario Carneiro]

I believe it should be possible to bind to those functions directly, but it doesn't seem to be working:

@[extern "lean_usize_of_nat"]
def Nat.toUSize! (n : @& Nat) : USize :=
  if n < USize.size then
    n.toUSize
  else
    panic! s!"Integer {n} is to larget for usize"

#eval (USize.size-1).toUSize!
-- could not find native implementation of external declaration 'Nat.toUSize!' (symbols 'l_Nat_toUSize_x21___boxed' or 'l_Nat_toUSize_x21')
#eval (USize.size).toUSize!