Lean library rust integration?

Stream: Program verification

[David Stainton 🦡]

What is the current state of Lean 4's rust integration?

I want to be able to use Lean to implement/model cryptographic protocols where ALL the cryptographic primitives are implemented in Rust... and Lean "knows the properties" they are supposed to have. I want to be able to use the interactive theorem prover for making proofs about the protocol construction itself and completely disregard the correctness of the cryptographic primitive functions.

[Henrik Böving]

There have been projects that use Rust and Lean such as Cedar and Niko Matsakis is looking into doing Rust and Lean things as well, so it's certainly underway/doable but not very heavily present in the eco system yet.

[Marcus Rossel]

I also use Lean and Rust in https://reservoir.lean-lang.org/@marcusrossel/egg. So I'd be happy to try to help if you have specific questions.

[David Stainton 🦡]

wow cool thanks! I'll look at these and try to figure it out.

[Jannis Limperg]

See also @Son Ho's Aeneas.

[David Stainton 🦡]

I did manage to find Aeneas... but that going in another direction and is about model extraction. Where I want to program my own lean models... but have those models rely on rust code.

[David Stainton 🦡]

looks like https://github.com/lurk-lab/RustFFI.lean is what i need

[David Stainton 🦡]

okay... finally, i have another question about Lean FFI and program verification; is there a way to fix this proof?

@[extern "add_one"]
opaque addOne : UInt32 → UInt32

def specialAddOne : (x : Nat) → Nat :=
  fun x => (addOne (UInt32.ofNat x)).toNat

variable (a b c d e : Nat)
variable (h1 : a = b)
variable (h2 : b = specialAddOne c)
--variable (h2 : b = c + 1)
variable (h3 : c = d)
variable (h4 : e = 1 + d)

theorem T : a = e :=
  calc
    a = b := h1
    b = c + 1 := h2
    c + 1 = d + 1 := congrArg Nat.succ h3
    d + 1 = 1 + d := Nat.add_comm d 1
    1 + d = e := Eq.symm h4

[David Stainton 🦡]

you see, the proof works if we remove the h2 line and replace it with the commented out h2 line.

[David Stainton 🦡]

how to coerce the theorem prover into accepting the mathematical properties of our FFI function implemented in Rust?

[David Stainton 🦡]

Aha, I can write an axiom for the FFI function and then include the axiom in the proof like this:

@[extern "add_one"]
opaque addOne : UInt32 → UInt32

def specialAddOne : (x : Nat) → Nat :=
  fun x => (addOne (UInt32.ofNat x)).toNat

axiom specialAddOne_eq_add_one : ∀ x : Nat, specialAddOne x = x + 1

variable (a b c d e : Nat)
variable (h1 : a = b)
variable (h2 : b = specialAddOne c)
--variable (h2 : b = c + 1)
variable (h3 : c = d)
variable (h4 : e = 1 + d)

theorem T : a = e :=
  calc
    a = b := h1
    b = specialAddOne c := h2
    specialAddOne c = c + 1 := specialAddOne_eq_add_one c
    c + 1 = d + 1 := congrArg Nat.succ h3
    d + 1 = 1 + d := Nat.add_comm d 1
    1 + d = e := Eq.symm h4

[Mario Carneiro]

your axiom is provably false:

@[extern "add_one"]
opaque addOne : UInt32 → UInt32

def specialAddOne : (x : Nat) → Nat :=
  fun x => (addOne (UInt32.ofNat x)).toNat

axiom specialAddOne_eq_add_one : ∀ x : Nat, specialAddOne x = x + 1

example : False :=
  have (x : UInt32) : x.toNat ≠ UInt32.size := Nat.ne_of_lt x.1.2
  this _ (specialAddOne_eq_add_one (UInt32.size - 1))

[David Stainton 🦡]

oh sure... because of the limits of using a UInt32

[Mario Carneiro]

What you can do instead is to put the @[extern] attribute on a def instead of an opaque:

@[extern "add_one"]
def addOne (x : UInt32) : UInt32 := x + 1

[Mario Carneiro]

This isn't about the limits of using a UInt32, note that I never actually had to call the function

[David Stainton 🦡]

i don't understand you example

[Mario Carneiro]

false axioms are bad, you can use them to break things

[Mario Carneiro]

a simple fix to the axiom is ∀ x : Nat, x + 1 < UInt32.size -> specialAddOne x = x + 1

[Mario Carneiro]

but you don't need to use an axiom here since with the def example this axiom becomes a provable theorem

[Mario Carneiro]

it's much easier to see that I didn't break logical consistency with the second example because I never used axiom

[Mario Carneiro]

it is not recommended to use axiom to add facts post facto to opaque because of the dangers of introducing inconsistency like this

[David Stainton 🦡]

okay... this is just a toy example that i used to essentially ask a question about lean, which is: can i use an FFI function in a proof?

[Mario Carneiro]

yes, that's what the second example is doing

[Mario Carneiro]

you could also just take/return Nat from the FFI function

[David Stainton 🦡]

i'm interested in proving correctness of cryptographic protocols without implementing the primitive functions in lean

[David Stainton 🦡]

and my first challenge now is to prove the KEM correctness

[Mario Carneiro]

in that case you should use a def where the body of the def is the "model" of the function

[Mario Carneiro]

and the @[extern] attribute points to the actual implementation in C

[David Stainton 🦡]

For all (pk, sk) ∈ [K.gen] and (k, c) ∈ [K.enc(pk)] we have K.dec(sk, c) = k.

[Mario Carneiro]

to do that you will certainly need an implementation, unless you just want to assume it?

[David Stainton 🦡]

and so... i'm not clear on what i'd put for the "body" in the case of a KEM encapsulation function.

[Mario Carneiro]

you would implement the function in lean

[David Stainton 🦡]

yeah already have implementation in rust, libcrux

[Mario Carneiro]

i.e. something that performs the same operations, but maybe inefficiently

[David Stainton 🦡]

no... too complicated to implement in lean

[Mario Carneiro]

then how are you going to prove it has properties?

[Mario Carneiro]

what are you taking as given?

[David Stainton 🦡]

i mean... wouldn't it be possible to instead assert some axioms?

[David Stainton 🦡]

i want to take the KEM as a given

[David Stainton 🦡]

i want to assume the KEM works perfectly

[Mario Carneiro]

yes you can do that too, as long as you can prove that a function with the desired properties exists

[David Stainton 🦡]

the goal is to build cryptographic protocols using KEMs and other primitives

[Mario Carneiro]

what are the properties? Do you have a spec?

[Mario Carneiro]

is it just enc/dec cancellation?

[David Stainton 🦡]

yeah... super simple encrypt/decrypt cancellation. All KEMs are the same. I don't want to specify the specifics of a KEM but keep it KEM agnostic.

[David Stainton 🦡]

s/agnostic/generic/

[Mario Carneiro]

can you write that in lean?

[Mario Carneiro]

the properties that is

[David Stainton 🦡]

yes i think so... although i haven't tried yet because honestly i'm stuck on some stupid pointer fuckery in the rust FFI. but once i've exposed all the rust FFI functions properly then i should be able to define some variable and write some propositions that are essentially expressing the KEM correctness proof which is a very well known proof in cryptographic. which is essentially this: A KEM must satisfy the following standard correctness property: P[(pk, sk) ←Gen,(c,k)← Enc(pk), k′ ← Dec(sk, c) : k = k′] = 1 .

[David Stainton 🦡]

i open source all my work, made some progress today but not finished yet https://github.com/katzenpost/crypt_walker

[Mario Carneiro]

does Enc return both the ciphertext and the message?

[David Stainton 🦡]

for this FFI stuff... i made a bunch of opaque types such as Ciphertext, Plaintext and so any propositions i write would necessarily involve those types.

[Mario Carneiro]

how do you decide what to send?

[David Stainton 🦡]

https://github.com/katzenpost/crypt_walker/blob/main/Main.lean

[David Stainton 🦡]

returns an "Encapsulation" type which contains both the shared secret and the ciphertext

[David Stainton 🦡]

anyway... even after i fix the rust ffi... it's not clear to me if this is going to work because perhaps Lean prover doesn't work with opaque types... or perhaps it'll work as long as i've specified the correct series of propositions about the types. very unclear right now.

[Mario Carneiro]

the free_* functions look wrong

[David Stainton 🦡]

okay so here's the corrected toy proof:

@[extern "add_one"]
opaque addOne : UInt32 → UInt32

def specialAddOne : (x : Nat) → Nat :=
  fun x => (addOne (UInt32.ofNat x)).toNat

axiom addOne_eq_add_one : ∀ x : Nat, x + 1 < UInt32.size -> specialAddOne x = x + 1

variable (a b c d e : Nat)
variable (h1 : a = b)
variable (h2 : b = specialAddOne c)
variable (h3 : c = d)
variable (h4 : e = 1 + d)
variable (h5 : c + 1 < UInt32.size)

theorem T : a = e :=
  calc
    a = b := h1
    b = specialAddOne c := h2
    specialAddOne c = c + 1 := addOne_eq_add_one c h5
    c + 1 = d + 1 := congrArg Nat.succ h3
    d + 1 = 1 + d := Nat.add_comm d 1
    1 + d = e := Eq.symm h4

def main : IO Unit :=
  IO.println $ addOne 1

[Mario Carneiro]

Here's a version of your definition with provable properties:

import Batteries.Classes.SatisfiesM

structure EncDecSpec where
  State : Type
  PublicKey : Type
  PrivateKey : Type
  Ciphertext : Type
  Plaintext : Type
  decap : PrivateKey → Ciphertext → StateM State Plaintext
  encap : PublicKey → StateM State (Ciphertext × Plaintext)
  init : State
  generate : StateM State (Σ' (pk : PublicKey), {sk : PrivateKey //
    ∀ s, let (c, k) := (encap pk s).1; ∀ s, (decap sk c s).1 = k})
  [plaintextEq : DecidableEq Plaintext]

instance : Inhabited EncDecSpec := ⟨{
  State := Unit
  PublicKey := Unit
  PrivateKey := Unit
  Ciphertext := Unit
  Plaintext := Unit
  decap := fun _ _ => pure ()
  encap := fun _ => pure ((), ())
  init := ()
  generate := pure ⟨(), (), fun () () => rfl⟩
  plaintextEq := inferInstance
}⟩

opaque encDecSpec : EncDecSpec

instance : Inhabited encDecSpec.State := ⟨encDecSpec.init⟩

abbrev EncDecM := StateM encDecSpec.State

def PublicKey : Type := encDecSpec.PublicKey
instance : Inhabited PublicKey := ⟨(encDecSpec.generate default).1.1⟩

def PrivateKey : Type := encDecSpec.PrivateKey
instance : Inhabited PrivateKey := ⟨(encDecSpec.generate default).1.2.1⟩

def Ciphertext : Type := encDecSpec.Ciphertext
instance : Inhabited Ciphertext :=
  ⟨(encDecSpec.encap (encDecSpec.generate default).1.1 default).1.1⟩

def Plaintext : Type := encDecSpec.Plaintext
instance : Inhabited Plaintext :=
  ⟨(encDecSpec.encap (encDecSpec.generate default).1.1 default).1.2⟩

@[extern "generate_key_pair"]
def generate : EncDecM (PublicKey × PrivateKey) := fun s =>
  let (⟨pk, sk, _⟩, s) := encDecSpec.generate s
  ((pk, sk), s)

@[extern "encapsulate"]
def encap : PublicKey → EncDecM (Ciphertext × Plaintext) := encDecSpec.encap

@[extern "decapsulate"]
def decap : PrivateKey → Ciphertext → EncDecM Plaintext := encDecSpec.decap

@[extern "is_plaintext_equal"]
instance : DecidableEq Plaintext := encDecSpec.plaintextEq

def IsEncapsulation (sk : PrivateKey) (c : Ciphertext) (k : Plaintext) :=
  ∀ s, (decap sk c s).1 = k

def KeyPair (pk : PublicKey) (sk : PrivateKey) :=
  ∀ s, let (c, k) := (encap pk s).1; IsEncapsulation sk c k

theorem generate_ok : SatisfiesM (fun (pk, sk) => KeyPair pk sk) generate := by
  simp [generate]; intro s; split; rename_i h1 s1 _; exact h1

theorem encap_ok {pk sk} (h : KeyPair pk sk) :
    SatisfiesM (fun (c, k) => IsEncapsulation sk c k) (encap pk) := by simpa using h

theorem decap_ok {sk c k} (h : IsEncapsulation sk c k) :
    SatisfiesM (fun k' => k' = k) (decap sk c) := by simpa using h

[David Stainton 🦡]

wow very interesting!

[David Stainton 🦡]

hmm how do i get my lean to use the Batteries module?

human@computer ~/code/crypt_walker (main) $ lake update
batteries: URL has changed; deleting ./lake-packages/batteries and cloning again
cloning https://github.com/leanprover-community/batteries to ./lake-packages/batteries
error: ././lake-packages/batteries/lakefile.lean:9:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig'
error: ././lake-packages/batteries/lakefile.lean:18:2: error: 'srcDir' is not a field of structure 'Lake.LeanExeConfig'
error: ././lake-packages/batteries/lakefile.lean:21:2: error: unknown attribute [test_driver]
error: ././lake-packages/batteries/lakefile.lean:23:2: error: 'srcDir' is not a field of structure 'Lake.LeanExeConfig'
error: ././lake-packages/batteries/lakefile.lean: package configuration has errors
human@computer ~/code/crypt_walker (main) $

[David Stainton 🦡]

oh i see my lean-toolchain was specifying a two year old lean version

[David Stainton 🦡]

Does this here imply my C/Rust must return a lean object tuple?

@[extern "generate_key_pair"]
def generate : EncDecM (PublicKey × PrivateKey) := fun s =>
  let (⟨pk, sk, _⟩, s) := encDecSpec.generate s
  ((pk, sk), s)

currently i have

#[no_mangle]
pub extern "C" fn generate_key_pair() -> *const KeyPair {
    let randomness = random_array();
    let key_pair = mlkem768::generate_key_pair(randomness);
    let (privkey, pubkey) = key_pair.into_parts();
    let ffi_pubkey: MlKemPublicKey<1184> = pubkey;
    let ffi_privkey: MlKemPrivateKey<2400> = privkey;
    return Box::into_raw(Box::new(KeyPair { pubkey: ffi_pubkey, privkey: ffi_privkey }));
}

which was meant to be passed around as an opaque type and not a tuple... but yeah it would be so much
better if the rust function could actually return a tuple of opaque types pub/private keys.

[David Stainton 🦡]

tomorrow i'll take another look at lean-egg which has a lot of this FFI stuff figured out

[Mario Carneiro]

yes it seemed easier for lean code if you just returned a tuple directly. You can do so using the functions in lean.h

[David Stainton 🦡]

or better yet, i use your rust crate lean_sys

[David Stainton 🦡]

@Mario Carneiro so if i can just arbitrarily define opaque types and write axioms or theorems for them... i could in theory do that for the whole suite of cryptographic functions that i would need to construct protocols. but then is there even any point in having those functions actually use FFI? i mean... if i care only about proving properties of cryptographic protocols then couldn't i construct "protocol models" from the opaque functions?

[David Stainton 🦡]

also as a side note, my intention was to write a lean cryptography library that only exposes one implementation per primitive... and would have the following primitives: PRP, AEAD, NIKE, KEM, HKDF, HMAC, PRF, stream cipher, signature scheme

[David Stainton 🦡]

also... another side note, from my perspective having used formal verification tools like ProVerif where we must write a series of equations to define our primitive functions before building up protocols... if i was to do the same exact thing in Lean there would probably be much more benefit to doing so in Lean because the prover is interactive.

[Mario Carneiro]

David Stainton said:

Mario Carneiro so if i can just arbitrarily define opaque types and write axioms or theorems for them... i could in theory do that for the whole suite of cryptographic functions that i would need to construct protocols. but then is there even any point in having those functions actually use FFI? i mean... if i care only about proving properties of cryptographic protocols then couldn't i construct "protocol models" from the opaque functions?

Presumably the reason you are using FFI here is for performance reasons. Lean has an okay compiler but it's clearly not going to be able to compete with a cryptographic primitive hand coded in assembly. Nevertheless, it is useful to have some slow and simple code as a point of comparison to the fast code since you can do differential fuzzing and such to detect errors, in addition to being able to prove properties of the code

[David Stainton 🦡]

No not all. I care not one bit about performance. I also do not care at all to fuzz or to otherwise detect faults in the cryptographic primtives... this is in fact a completely different concern from the concern of proving protocol properties which are composed of many many cryptographic primtiives.

[David Stainton 🦡]

just a minute... i'll show your some of my ProVerif specs... which prove nothing about cryptographci primitives

[David Stainton 🦡]

for example https://github.com/katzenpost/formal_specifications/blob/main/sphinx/kem_sphinx.passive.pv

[David Stainton 🦡]

The reason I don't want to implement cryptographic primitives in Lean is because that isn't what I do in any language so why start now?

[David Stainton 🦡]

I compose protocols not primitives

[Mario Carneiro]

I'm confused then as well, what are you hoping to get out of this library?

[Mario Carneiro]

if you just want to write a theorem about functions with inverses you certainly don't need FFI to do that

[David Stainton 🦡]

I'm hoping to use it to build prototypes of cryptographic protocols which I can test and demonstrate that they work and I can also prove various properties of the protocol with the propositions and theorems and proofs. All that having been said, the observation that I made earlier still stands: I can do all the proving with just opaque types without any need for FFI... just write pure algebra like i normally do when i'm modeling a protocol in ProVerif. that in of itself would be useful to all kinds of cryptographers... if there was a small library of equations that represent the cryptographic primitives that they use to compose protocols.

[David Stainton 🦡]

yes! that's what I was thinking.

[Mario Carneiro]

I'm not sure I'd call it an "implementation" of the protocol though in that case, more of a specification

[Mario Carneiro]

because since you aren't writing any implementation code in lean and aren't hooking up an implementation from rust you won't be able to run them at all

[David Stainton 🦡]

indeed. anyway... if i did all the FFI work to bring in all the cryptographic primitives then i could write protocol prototypes and that might have some advantages... like being testable with unit tests.

[Mario Carneiro]

at which point I don't even really see the point of calling it KEM, HKDF etc, these are just the bare structure of the functions and not even enough to differentiate them

[Mario Carneiro]

normally when I think of what would qualify as a "spec for AES" that means writing down all the cipher tables such that you can prove what the output is given any input and you can compare differing implementations to see if they agree with the spec

[David Stainton 🦡]

you lost me on that last point. all the cryptographic primitive categories are quite different. they have different return values, different arguments etc. and their relationships are different.

[Mario Carneiro]

If all you say is that dec(enc(k)) = k then I imagine quite a few of them will have basically that shape

[David Stainton 🦡]

okay, that's true if we compare say an AEAD to a stream cipher... if they have the same number of arguments.... because the algebraic relationship doesn't express what's going on and their properties

[David Stainton 🦡]

this is often referred to as the symbolic model of cryptography

[Mario Carneiro]

right

[David Stainton 🦡]

but i can see some advantages to actually implementing the primitives in lean... lean would then be able to test for the bitwise properties... like the avalanche effect if a single bit is flipped on a PRP ciphertext versus no such effect on a stream ciphertext

[Mario Carneiro]

I could imagine having a typeclass StreamCipher which collects these basic properties, and maybe add some more and have symbolic models for all of the types you are interested in

[Mario Carneiro]

that would cover the high level properties, and wouldn't commit to being an "implementation" in the same way as an opaque

[David Stainton 🦡]

yeah... i'd have to make such typeclasses for all the primitives. and in order to compose protocols they would have to share some of the types. probably easy to just coerce them. i have no experience with interactive theorem proving... so mostly i've been learning the functional programming parts of lean so far.

[David Stainton 🦡]

would the symbolic models for the types use opaque types? it sounds like they could just be some kind of inductive types or something.

[Mario Carneiro]

no, the typeclasses are not opaque types, they are record types

[David Stainton 🦡]

okay i guess i don't have enough experience with lean typeclasses... i thought they were similar to rust traits in that they specify some functions... ah that operate on the type of the typeclass i guess.

[Mario Carneiro]

In fact, I wrote one earlier as the specification for the EncDec functions, see EncDecSpec

[David Stainton 🦡]

right

[Mario Carneiro]

you can prove things about EncDecSpecs without ever actually having one

[Mario Carneiro]

the opaque was just to create a particular one (to which some FFI code is attached)

[David Stainton 🦡]

okay... so Lean used in this way can be used for symbolic cryptographic models. that's pretty interesting to me.

[David Stainton 🦡]

I have zero experience using cryptoverif and the like that use the computational model. lean can obviously do that and the advantages would be that i could test the more complicated protocol properties which the symbolic model just skips over.

[David Stainton 🦡]

perhaps if a bunch of cryptography professors adopts Lean then their students will implement a bunch of primitives in lean.

[David Stainton 🦡]

trying to use the lean-sys rust crate so i can return Lean objects to Lean via the FFI... FFI works fine but I'm unable to actually use the lean-syscrate because of this build error:

human@computer ~/code/leanprojects/lean-ffi-tuple2 $ lake build
ℹ [6/14] Ran crypt_walker/crypt_walker_for_lean.static
info: stderr:
    Finished release [optimized] target(s) in 0.00s
✖ [8/14] Building crypt_walker_for_lean.static:shared
trace: .> /home/human/.elan/toolchains/leanprover--lean4---v4.8.0/bin/leanc -shared -o ././.lake/build/lib/libcrypt_walker_for_lean.so -Wl,--whole-archive ././.lake/build/lib/libcrypt_walker_for_lean.a -Wl,--no-whole-archive
info: stderr:
ld.lld: error: relocation R_X86_64_TPOFF32 against lean::g_finalizing cannot be used with -shared
>>> defined in ././.lake/build/lib/libcrypt_walker_for_lean.a(thread.cpp.o)
>>> referenced by thread.cpp
>>>               thread.cpp.o:(lean_finalize_thread) in archive ././.lake/build/lib/libcrypt_walker_for_lean.a

ld.lld: error: relocation R_X86_64_TPOFF32 against lean::g_finalizing cannot be used with -shared
>>> defined in ././.lake/build/lib/libcrypt_walker_for_lean.a(thread.cpp.o)
>>> referenced by thread.cpp
>>>               thread.cpp.o:(lean_finalize_thread) in archive ././.lake/build/lib/libcrypt_walker_for_lean.a

[David Stainton 🦡]

I noticed that lean-egg doesn't actually use the lean-sys rust crate. it just has the C and Rust code directly in it's Lean package

[Mario Carneiro]

it looks like lean-egg doesn't need lean-sys because rust code is not handling lean objects in any way

[Mario Carneiro]

A quick google search suggests that you need to compile your C code or other libraries with -fPIC

[David Stainton 🦡]

import Lake
open Lake DSL

package crypt_walker where
  srcDir := "Lean"

@[default_target]
lean_lib CryptWalker where
  precompileModules := true

extern_lib crypt_walker_for_lean pkg := do
  proc { cmd := "cargo", args := #["rustc", "--release", "--", "-C", "relocation-model=pic"], cwd := pkg.dir / "Rust" }
  let name := nameToStaticLib "crypt_walker_for_lean"
  let srcPath := pkg.dir / "Rust" / "target" / "release" / name
  IO.FS.createDirAll pkg.nativeLibDir
  let tgtPath := pkg.nativeLibDir / name
  IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)
  return pure tgtPath

human@computer ~/code/leanprojects/lean-ffi-tuple2 (main) $ lake build
ℹ [1/9] Ran crypt_walker/crypt_walker_for_lean.static
info: stderr:
   Compiling autocfg v1.3.0
   Compiling libc v0.2.155
   Compiling parking_lot_core v0.9.10
   Compiling smallvec v1.13.2
   Compiling cfg-if v1.0.0
   Compiling scopeguard v1.2.0
   Compiling lean-sys v0.0.7
   Compiling static_assertions v1.1.0
   Compiling lock_api v0.4.12
   Compiling memoffset v0.9.1
   Compiling parking_lot v0.12.3
   Compiling crypt_walker_for_lean v0.1.0 (/home/human/code/leanprojects/lean-ffi-tuple2/Rust)
    Finished release [optimized] target(s) in 1.11s
✖ [3/9] Building crypt_walker_for_lean.static:shared
trace: .> /home/human/.elan/toolchains/leanprover--lean4---v4.8.0/bin/leanc -shared -o ././.lake/build/lib/libcrypt_walker_for_lean.so -Wl,--whole-archive ././.lake/build/lib/libcrypt_walker_for_lean.a -Wl,--no-whole-archive
info: stderr:
ld.lld: error: relocation R_X86_64_TPOFF32 against lean::g_finalizing cannot be used with -shared
>>> defined in ././.lake/build/lib/libcrypt_walker_for_lean.a(thread.cpp.o)
>>> referenced by thread.cpp
>>>               thread.cpp.o:(lean_finalize_thread) in archive ././.lake/build/lib/libcrypt_walker_for_lean.a

ld.lld: error: relocation R_X86_64_TPOFF32 against lean::g_finalizing cannot be used with -shared
>>> defined in ././.lake/build/lib/libcrypt_walker_for_lean.a(thread.cpp.o)
>>> referenced by thread.cpp
>>>               thread.cpp.o:(lean_finalize_thread) in archive ././.lake/build/lib/libcrypt_walker_for_lean.a

[Mario Carneiro]

Your project is not using a fixed lean version, this is not recommended

[Mario Carneiro]

what lean version are you compiling against?

[David Stainton 🦡]

oh good question... let me check

[David Stainton 🦡]

leanprover/lean4:v4.8.0

[David Stainton 🦡]

i specifically matched it with the version the lean-sys uses

[Mario Carneiro]

you have things that don't make sense on 4.8.0, like @[test_driver]

[Mario Carneiro]

I've managed to replicate your error message on v4.9.0

[Mario Carneiro]

and so far I haven't found anything in lean-sys that would need to change on 4.9.0

[David Stainton 🦡]

i just pushed my ffi experiment to https://github.com/katzenpost/lean-ffi ... i'm not using any test_driver in that particular lakefile that i just pushed and posted.

[David Stainton 🦡]

if you replicated the error using v4.9.0... then it sounds like i have a elan or lake tooling problem locally

[Mario Carneiro]

why?

[David Stainton 🦡]

you just told me that you replicated the error. using v4.9.0

[Mario Carneiro]

yes, that means the report is valid, no?

[David Stainton 🦡]

the lakefile i posted has no "test" string in it

[Mario Carneiro]

I needed to use 4.9.0 because 4.8.0 had some issues with missing attributes, but I suspect that lean-sys also works in the same way on 4.9.0 even though it has not had a release for that version

[David Stainton 🦡]

i'm curious if i'm using lean-sys incorrectly.

[Mario Carneiro]

I pulled the master branch of crypt_walker for the first replication

[Mario Carneiro]

but the lean-ffi project also produces the same issue on 4.8.0 as you say

[Mario Carneiro]

I am sure you are "using it incorrectly" but I also don't know how to use it, this linking stuff takes years off my life

[Mario Carneiro]

I would really like lean-sys to just be plug and play but somehow there is always one more issue

[Mario Carneiro]

the cargo invocation line in your lakefile is also unexpectedly complex, did you get that from lean-egg?

[David Stainton 🦡]

hmm yeah i think i copied that from lean-egg

[David Stainton 🦡]

yeah this linking stuff is tricky. i suppose it's a matter of messing with the Cargo.toml and the lakefile.lean

[Mario Carneiro]

the other free variable is the build script in lean-sys

[David Stainton 🦡]

oh it's build.rs

[David Stainton 🦡]

aha feature="static"

[Mario Carneiro]

yeah that was my next suggestion, I'm not sure if you want to statically link or not

[Mario Carneiro]

lake usually statically links, but I think something is still missing from the script

[David Stainton 🦡]

it kind of seems like i'm supposed to use static linking... i'll try it.

[Mario Carneiro]

feature="static" is on by default

[Mario Carneiro]

if you set default-features=false you can turn it off

[David Stainton 🦡]

yes but it looks like lean-sys's build.rs has some logic for choosing how to link with lean... and if not static then it picks the .so to link with. the error messages i'm getting make me think it's linking with a .so when it should not

[Mario Carneiro]

I have noticed the strange behavior that if you disable the static feature then the build works, and if you re-enable the feature then the build still works, including if you delete the Rust/target folder but not if you delete .lake

[David Stainton 🦡]

interesting. sounds like a lake tooling bug of some sort

[Mario Carneiro]

I'm starting to suspect lake... lake build crypt_walker_for_lean:static works but lake build crypt_walker_for_lean:shared fails, and somehow the default build is calling the crypt_walker_for_lean:shared facet even though there is nothing in the lakefile which says anything about whether to build this lib as static or shared

[Mario Carneiro]

cc: @Mac Malone

[Mac Malone]

@Mario Carneiro crypt_walker_for_lean is an extern_lib and CryptWalker has precompileModules := true. Lake will build the shared library of crypt_walker_for_lean, so it can be passed as a precompiled --load-dynlib for CryptWalker modules.

[Mario Carneiro]

is there a way the extern_lib can know that it is being built as a shared lib so it can tell rust about this?

[Mario Carneiro]

also, precompileModules := false doesn't seem to make a difference

[Mac Malone]

@Mario Carneiro extern_lib targets should assume they are being built for both static and shared linking. Enabling different build scripts for each is on the to-do list, but we have not been able to dedicate time to improving the FFI experience yet.

[Mario Carneiro]

I don't know what that means. As far as I can tell you only return one path from the target, is it supposed to build it twice?

[Mario Carneiro]

also it would be good to have a way to say that an extern lib is static only and does not support whatever features precompileModules needs a shared lib for

[David Stainton 🦡]

yeah building with lake build crypt_walker_for_lean:static works but i guess that just causes the rust to be built and then it's not linked with the lean stuff.

[Mac Malone]

Mario Carneiro said:

I don't know what that means. As far as I can tell you only return one path from the target, is it supposed to build it twice?

It returns a static library and that static library is then used to link its corresponding shared library.

[Mac Malone]

Mario Carneiro said:

also it would be good to have a way to say that an extern lib is static only and does not support whatever features precompileModules needs a shared lib for

While good for terminal packages, packages meant to be used as libraries should support both options as failure to provide this has as cascading effect on dependent packages (i.e., they are all now static-only).

[Mac Malone]

Mario Carneiro said:

also, precompileModules := false doesn't seem to make a difference

This is odd. It is still building shared without precompileModules?

[Mario Carneiro]

yes

[Mac Malone]

@Mario Carneiro Do you have some error output you can share (preferably with -v)?

[Mario Carneiro]

The input is exactly the lean-ffi project with the precompileModules := true line removed.

$ lake build
ℹ [1/7] Ran crypt_walker/crypt_walker_for_lean.static
info: stderr:
   Compiling autocfg v1.3.0
   Compiling libc v0.2.155
   Compiling parking_lot_core v0.9.10
   Compiling smallvec v1.13.2
   Compiling scopeguard v1.2.0
   Compiling cfg-if v1.0.0
   Compiling lean-sys v0.0.7
   Compiling static_assertions v1.1.0
   Compiling lock_api v0.4.12
   Compiling memoffset v0.9.1
   Compiling parking_lot v0.12.3
   Compiling crypt_walker_for_lean v0.1.0 (/home/mario/Documents/lean/lean-ffi/Rust)
    Finished `release` profile [optimized] target(s) in 7.08s
✖ [3/7] Building crypt_walker_for_lean.static:shared
trace: .> /home/mario/.elan/toolchains/leanprover--lean4---v4.8.0/bin/leanc -shared -o ././.lake/build/lib/libcrypt_walker_for_lean.so -Wl,--whole-archive ././.lake/build/lib/libcrypt_walker_for_lean.a -Wl,--no-whole-archive
info: stderr:
ld.lld: error: relocation R_X86_64_TPOFF32 against lean::g_finalizing cannot be used with -shared
>>> defined in ././.lake/build/lib/libcrypt_walker_for_lean.a(thread.cpp.o)
>>> referenced by thread.cpp
>>>               thread.cpp.o:(lean_finalize_thread) in archive ././.lake/build/lib/libcrypt_walker_for_lean.a
...

ld.lld: error: too many errors emitted, stopping now (use --error-limit=0 to see all errors)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/mario/.elan/toolchains/leanprover--lean4---v4.8.0/bin/leanc' exited with code 1
Some builds logged failures:
- crypt_walker_for_lean.static:shared
error: build failed

[Mac Malone]

@Mario Carneiro Could you run with -v? I would try myself, but I am not sure I have a properly configured Rust.

[Mario Carneiro]

$ lake build -v
ℹ [1/7] Ran crypt_walker/crypt_walker_for_lean.static
trace: ././Rust> cargo rustc --release -- -C relocation-model=pic
info: stderr:
    Finished `release` profile [optimized] target(s) in 0.01s
✖ [3/7] Building crypt_walker_for_lean.static:shared
trace: .> /home/mario/.elan/toolchains/leanprover--lean4---v4.8.0/bin/leanc -shared -o ././.lake/build/lib/libcrypt_walker_for_lean.so -Wl,--whole-archive ././.lake/build/lib/libcrypt_walker_for_lean.a -Wl,--no-whole-archive
info: stderr:
ld.lld: error: relocation R_X86_64_TPOFF32 against lean::g_finalizing cannot be used with -shared
>>> defined in ././.lake/build/lib/libcrypt_walker_for_lean.a(thread.cpp.o)
>>> referenced by thread.cpp
>>>               thread.cpp.o:(lean_finalize_thread) in archive ././.lake/build/lib/libcrypt_walker_for_lean.a

[David Stainton 🦡]

https://justpaste.it/9w7oe

[Mac Malone]

Oh, I forgot the build ANSI progress counter hides the other jobs. Could you also try -v --no-ansi?

[Mario Carneiro]

$ lake build -v --no-ansi
ℹ [1/7] Ran crypt_walker/crypt_walker_for_lean.static
trace: ././Rust> cargo rustc --release -- -C relocation-model=pic
info: stderr:
    Finished `release` profile [optimized] target(s) in 0.01s
✔ [2/7] Ran crypt_walker_for_lean.static:static
✖ [3/7] Building crypt_walker_for_lean.static:shared
trace: .> /home/mario/.elan/toolchains/leanprover--lean4---v4.8.0/bin/leanc -shared -o ././.lake/build/lib/libcrypt_walker_for_lean.so -Wl,--whole-archive ././.lake/build/lib/libcrypt_walker_for_lean.a -Wl,--no-whole-archive
info: stderr:
ld.lld: error: relocation R_X86_64_TPOFF32 against lean::g_finalizing cannot be used with -shared
>>> defined in ././.lake/build/lib/libcrypt_walker_for_lean.a(thread.cpp.o)
>>> referenced by thread.cpp
>>>               thread.cpp.o:(lean_finalize_thread) in archive ././.lake/build/lib/libcrypt_walker_for_lean.a

ld.lld: error: relocation R_X86_64_TPOFF32 against lean::g_finalizing cannot be used with -shared
>>> defined in ././.lake/build/lib/libcrypt_walker_for_lean.a(thread.cpp.o)
>>> referenced by thread.cpp
>>>               thread.cpp.o:(lean_finalize_thread) in archive ././.lake/build/lib/libcrypt_walker_for_lean.a
...
ld.lld: error: too many errors emitted, stopping now (use --error-limit=0 to see all errors)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/mario/.elan/toolchains/leanprover--lean4---v4.8.0/bin/leanc' exited with code 1
✔ [4/7] Ran crypt_walker_for_lean.static:dynlib
✔ [5/7] Ran CryptWalker.Basic
✔ [6/7] Ran CryptWalker
✔ [7/7] Ran crypt_walker/CryptWalker:leanArts
Some builds logged failures:
- crypt_walker_for_lean.static:shared
error: build failed

[Mac Malone]

Ah, this is the bug I fixed last month (lean4#4566) where Lake would always precompile the package of a module. If it is possible to bump the project up to v4.10.0-rc2, the shared library should not be built.

[Mario Carneiro]

it does seem to work now (without precompileModules := true)

[Mario Carneiro]

I'm not clear on whether there is any way to make this work with shared and static simultaneously

[Mac Malone]

@Mario Carneiro It suprises me that Rust cannot build a static library that can be linked into a shared object.

[Mario Carneiro]

I don't know, does that error message make sense to you?

[Mario Carneiro]

I can pass whatever arguments I need to to the linker but I have no idea what the right voodoo is

[David Stainton 🦡]

cool. it works.

[David Stainton 🦡]

now i'm trying to get my test target to work... because ideally i'd be able to run a series of tests via lake in the same project directory

[David Stainton 🦡]

Adding this to the lakefile:

@[test_driver]
lean_exe tests {
  root := `tests.Main
}

lake test -v --no-ansi

lake test -v --no-ansi
ℹ [1/9] Replayed CryptWalker.Basic
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/human/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/lean ././Lean/./CryptWalker/Basic.lean -R ././Lean/. -o ././.lake/build/lib/CryptWalker/Basic.olean -i ././.lake/build/lib/CryptWalker/Basic.ilean -c ././.lake/build/ir/CryptWalker/Basic.c --json
ℹ [2/9] Replayed CryptWalker
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/human/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/lean ././Lean/./CryptWalker.lean -R ././Lean/. -o ././.lake/build/lib/CryptWalker.olean -i ././.lake/build/lib/CryptWalker.ilean -c ././.lake/build/ir/CryptWalker.c --json
ℹ [3/9] Replayed tests.Main
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/human/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/lean ././Lean/./tests/Main.lean -R ././Lean/. -o ././.lake/build/lib/tests/Main.olean -i ././.lake/build/lib/tests/Main.ilean -c ././.lake/build/ir/tests/Main.c --json
ℹ [4/9] Replayed tests.Main:c.o (with exports)
trace: .> /home/human/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/leanc -c -o ././.lake/build/ir/tests/Main.c.o.export ././.lake/build/ir/tests/Main.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [5/9] Replayed CryptWalker.Basic:c.o (with exports)
trace: .> /home/human/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/leanc -c -o ././.lake/build/ir/CryptWalker/Basic.c.o.export ././.lake/build/ir/CryptWalker/Basic.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [6/9] Replayed CryptWalker:c.o (with exports)
trace: .> /home/human/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/leanc -c -o ././.lake/build/ir/CryptWalker.c.o.export ././.lake/build/ir/CryptWalker.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [7/9] Ran crypt_walker/crypt_walker_for_lean.static
trace: ././Rust> cargo rustc --release -- -C relocation-model=pic
info: stderr:
    Finished release [optimized] target(s) in 0.00s
✔ [8/9] Ran crypt_walker_for_lean.static:static
✖ [9/9] Building tests
trace: .> /home/human/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/leanc -o ././.lake/build/bin/tests ././.lake/build/ir/tests/Main.c.o.export ././.lake/build/ir/CryptWalker/Basic.c.o.export ././.lake/build/ir/CryptWalker.c.o.export ././.lake/build/lib/libcrypt_walker_for_lean.a
info: stderr:
ld.lld: error: duplicate symbol: lean_internal_panic
>>> defined at object.cpp
>>>            object.cpp.o:(lean_internal_panic) in archive ././.lake/build/lib/libcrypt_walker_for_lean.a
>>> defined at object.cpp
>>>            object.cpp.o:(.text+0x0) in archive /home/human/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/lib/lean/libleanrt.a

[Mac Malone]

That error makes it seem like lean-sys is including duplicate symbols from the core Lean runtime when building a shared libaray. @Mario Carneiro?

[Mario Carneiro]

lean-sys doesn't define those symbols, it references them

[Mac Malone]

The linker doesn't appear to agree?

[Mario Carneiro]

@David Stainton try setting the extern feature in lean-sys

[Mario Carneiro]

I tried adding a test runner via David's directions (and also adding an empty file in Lean/tests/Main.lean) and I get a funny result:

$ lake test -v --no-ansi
ℹ [1/5] Built tests.Main
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/mario/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/lean ././Lean/./tests/Main.lean -R ././Lean/. -o ././.lake/build/lib/tests/Main.olean -i ././.lake/build/lib/tests/Main.ilean -c ././.lake/build/ir/tests/Main.c --json
ℹ [2/5] Built tests.Main:c.o (with exports)
trace: .> /home/mario/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/leanc -c -o ././.lake/build/ir/tests/Main.c.o.export ././.lake/build/ir/tests/Main.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [3/5] Ran crypt_walker/crypt_walker_for_lean.static
trace: ././Rust> cargo rustc --release -- -C relocation-model=pic
info: stderr:
   Compiling autocfg v1.3.0
   Compiling libc v0.2.155
   Compiling parking_lot_core v0.9.10
   Compiling cfg-if v1.0.0
   Compiling scopeguard v1.2.0
   Compiling smallvec v1.13.2
   Compiling lean-sys v0.0.7
   Compiling static_assertions v1.1.0
   Compiling lock_api v0.4.12
   Compiling memoffset v0.9.1
   Compiling parking_lot v0.12.3
   Compiling crypt_walker_for_lean v0.1.0 (/home/mario/Documents/lean/lean-ffi/Rust)
    Finished `release` profile [optimized] target(s) in 1.31s
info: stdout/stderr:
running cargo
ran cargo
ran cargo: ././.lake/build/lib/libcrypt_walker_for_lean.a
✔ [4/5] Ran crypt_walker_for_lean.static:static
ℹ [5/5] Built tests
trace: .> /home/mario/.elan/toolchains/leanprover--lean4---v4.10.0-rc2/bin/leanc -o ././.lake/build/bin/tests ././.lake/build/ir/tests/Main.c.o.export ././.lake/build/lib/libcrypt_walker_for_lean.a
Lake version 5.0.0-702c31b (Lean version 4.10.0-rc2)

USAGE:
  lake [OPTIONS] <COMMAND>

COMMANDS:
  new <name> <temp>     create a Lean package in a new directory
  init <name> <temp>    create a Lean package in the current directory
  build <targets>...    build targets
  exe <exe> <args>...   build an exe and run it in Lake's environment
  test                  test the package using the configured test driver
  check-test            check if there is a properly configured test driver
  lint                  lint the package using the configured lint driver
...

for some reason it prints a usage note at runtime

[Mario Carneiro]

I'm not getting the duplicate definition error

[David Stainton 🦡]

@Mario Carneiro yes that was exactly what was needed to make the test target work; setting the extern feature. okay cool.

[David Stainton 🦡]

@Mario Carneiro and @Mac Malone Thanks for helping me with the FFI stuff. Since then I've decided to take a different tack in my work using Lean where I write protocols in Lean without any FFI. However.. I'm hoping that my colleague will soon start integrating a benchmarking library into Lean using the FFI.

[David Stainton 🦡]

I'm going to document the things you've taught me so that my colleague can use Lean FFI for projects.

[Mac Malone]

You're welcome. That all sounds great! :tada: