Float design document

Stream: lean4

[cognivore]

I'm a bit confused with what's FloatSpec and why is Float capturing Unit in val?

I'm guessing that it has something to do with the fact that most of Float.lean is externed.

But I'm writing an overlay for these functions because I need a pure Lean implementation for compilation to different targets, so I wonder what's the shortest path to override externed functions.

[Mario Carneiro]

the purpose of the body of the opaque floatSpec : FloatSpec := ... definition is only to prove that the set of conditions required on the float type are consistent

[Mario Carneiro]

This is fairly trivial because there are basically no laws regarding the operations, so Unit suffices to give a model

[Mario Carneiro]

This does not imply that the type of floats is Unit, the logic only sees that it is a type satisfying those axioms

[cognivore]

Sorry for perhaps a silly question... In the module there's floatSpec, which is the model of floats, I assume, and, say, Float.lt, which matches two Floats, destrucutres those and calls floatSpec.lt.

[cognivore]

But floatSpec.lt is True. Aside from the fact that I'm too stupid to understand how to even represent a float using type Float given this code.

[Mario Carneiro]

That last line is the one that is false

[Mario Carneiro]

floatSpec is an opaque object of type FloatSpec. It is not equal to the thing on the other side of the :=

[Mario Carneiro]

I'm not sure what you mean with your other questions though. What exactly are you trying to do? Are you making / contemplating changes to Float.lean, or making your own float-like type unrelated to Float, or making some additional external overlay on the same type Float defined in core?

[Mario Carneiro]

The model of floats is FloatSpec itself (the type, not the value)

[Mario Carneiro]

That is, we have a type Float, a designated value val : Float, two predicates lt and le and a decidability instance for them

[Mario Carneiro]

we know nothing at all about the type beyond that

[cognivore]

I'm basically doing quality assurance on yatima, a lean compiler that targets other languages. It can't use extern. So I need to patch Lean to have native Floats for my work.

[cognivore]

Mario Carneiro said:

That is, we have a type Float, a designated value val : Float, two predicates lt and le and a decidability instance for them

I think I begin to understand.

[cognivore]

No, not really. I mean, I understand what you wrote, but I fail to see how it correlates to the code.

[cognivore]

def Float.lt : Float → Float → Prop := fun a b =>
  match a, b with
  | ⟨a⟩, ⟨b⟩ => floatSpec.lt a b

Isn't floatSpec.lt is always True?

[Henrik Böving]

floatSpec is an opaque you wont be able to prove it.

[Henrik Böving]

All of this Float stuff in Lean is just there to make the type system happy, the compiler doesn't care about it at all, it will use native floating point implementations and functions.

[cognivore]

Right. But if I need to make native (lean) implementation rather than foreign, I would still use the same FloatSpec, right?

[Mario Carneiro]

these two declarations are exactly the same:

opaque p : Prop := True

opaque p : Prop := False

This one too:

opaque p : Prop

[cognivore]

As I'm re-reading section on opaque keyword in "Significant Changes" document [a better source?], I wonder...

Could I read the def like this:

def Float.lt : Float \r Float \r (floatSpec : FloatSpec) \r Prop := ...

?

[Mario Carneiro]

In all cases you get an arbitrary proposition about which you know nothing other than it is a Prop, and the only purpose of the thing on the other side of the := is to prove that the type Prop is inhabited so that you can't do opaque contradiction : False

[cognivore]

So to rephrase your answer. The purpose of def Float.lt is to show that there are propositions about pairs of floats?

[Henrik Böving]

cognivore said:

Right. But if I need to make native (lean) implementation rather than foreign, I would still use the same FloatSpec, right?

If you want to make a native implementation you want to get away of all of this floatSpec stuff and just roll your own Float type around a 32 or 64 bit integer with custom functions that treat it like a mantissa around it I guess.

But you will also have to reimplmenent fixed with integers now since those are also offloaded by the compiler to native code, as well as natural numbers which are offloaded to a C based big num implementation, also Array, String, Task and maybe others I'm forgetting, in general this whole undertaking will just be a huge PITA for you I'd say.

[cognivore]

Or rather. If there is some Float implementation (the purpose of structure Float), there is a proposition for pairs of those.

[cognivore]

Henrik Böving said:

cognivore said:

Right. But if I need to make native (lean) implementation rather than foreign, I would still use the same FloatSpec, right?

If you want to make a native implementation you want to get away of all of this floatSpec stuff and just roll your own Float type around a 32 or 64 bit integer with custom functions that treat it like a mantissa around it I guess.

But you will also have to reimplmenent fixed with integers now since those are also offloaded by the compiler to native code, as well as natural numbers which are offloaded to a C based big num implementation, also Array, String, Task and maybe others I'm forgetting, in general this whole undertaking will just be a huge PITA for you I'd say.

Yes, we already know about Array. And yes, there are others. Gladly we won't need Task. But we're taking an incremental approach. :)

[cognivore]

Thanks for heads-up.

[Henrik Böving]

And I mean once you are done ripping all of this stuff out you will have lost parts of the Lean system that actually make it good to use as a language for real world programming such as the fact that Arrays are actually updated in place and that they (just like strings) are actually slices of memory with good cache behaviour and so on. I really don't think it's a particular good idea to work against the runtime.

[cognivore]

Of course, I understand. We target a zk-SNARK frontend. The run times of our programs are days :)

[cognivore]

Here's what my colleague wrote:

@Arthur Paulino @cognivore LCNF does not go viral on every @[extern] declaration. I'm afraid this is just a case of the Lean compiler having bad/unexpected behavior. The reason why is because

protected opaque Float.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float :=
   if s then
    let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
    let m := (m <<< (3 * e + s)) / 5^e
    Float.ofBinaryScientific m (-4 * e - s)
  else
    Float.ofBinaryScientific (m * 5^e) e

is tagged opaque, so it has no body. (so @cognivore you instinct was correct lol). Now, why is it tagged opaque and
why does the compiler generate no body even though it clearly has one? I have no idea -- but I've come to accept that there are just "things" the Lean compiler does that are undocumented, and we will have to work around them.