San Francisco, CA, USA

Stream: Geographic locality

[David Stainton 🦡]

Is anyone who is in SF interested in pair programming in Lean or discussing Lean topics such as program verification, functional programming, category theory, type theory and related books?

I am currently working on a cryptography library for Lean, currently focused on a Merkle Hash Tree implementation in Lean where I translate a very nice Haskell implementation into Lean.

As for books, I do eventually want to read The Little Typer, but I've instead been prioritizing my understanding of category theory. I'm also working my way through Category Theory For Programmers and watching the lectures by Bartosz Milewski.

My suggestion for such a group is that we meet at Noisebridge hacker space once per week. But I'd be curious to hear other location suggestions.

[Chris Bailey]

I'm in San Francisco, always down to meet Lean people.

[Kyle Ellefsen]

I'm also in SF and would be down to join a weekly Lean meetup at Noisebridge or wherever. I recently finished working through The Little Typer, am nearly through Matthew Macauley's abstract algebra lectures, and would like to go further into category theory. I'd also like to implement a simple lean-esque theorem prover language.

[David Stainton 🦡]

Okay cool. Three peeps is obviously the magic threshold for starting a new meetup. hmm maybe i should tell Noisebridge we are coming. Shall we meet sometime next week?

[Kyle Ellefsen]

Any day next week works for me.

[Chris Bailey]

I'm out of town on Tuesday the 20th, free other than that.

[David Stainton 🦡]

Let's meet at Noisebridge on Thursday the 22nd at 2pm?
If they won't let us in we can just walk to a park or cafe. But it would be better if we get inside Noisebridge because then there is more space to use and we can look at Lean code examples or interact with it's theorem prover or whatever we wanna do as a small group.

[David Stainton 🦡]

Keep in mind, Noisebridge is in a kind of "bad neighborhood" in a bad alley way so make sure you have good proprioceptive awareness of your surroundings.

[David Stainton 🦡]

https://www.noisebridge.net/wiki/Noisebridge

[Chris Bailey]

That works for me.

[Kyle Ellefsen]

Me too

[David Stainton 🦡]

cool

[Quinn]

I might make it up from east bay!

[David Stainton 🦡]

the more the merrier. bring your Lean questions and answers. maybe we can help each other get unstuck on Lean related problems? I know my focus has been very narrowly teaching myself functional progamming in Lean and I haven't managed to learn much about proving tactics. not a proof engineer ;-)

[David Stainton 🦡]

recently wrote X25519 ECDH using Lean's ZMod from Mathlib

[David Stainton 🦡]

it's field arithmetic, simple

[David Stainton 🦡]

https://github.com/katzenpost/crypt_walker/blob/main/Lean/CryptWalker/nike/x25519pure.lean

[David Stainton 🦡]

actually... i know nothing of elliptic curves

[David Stainton 🦡]

i just copied other implementations of the "montgomery bridge"

[David Stainton 🦡]

also ported a haskell merkle tree to lean here https://github.com/katzenpost/crypt_walker/blob/main/Lean/CryptWalker/protocol/merkle_tree.lean

what have you all been working on? perhaps show and tell your projects when we meet if you like.

[Kyle Ellefsen]

I'm still pretty new to lean, so I'm still working on warmup exercises. Last year I very slowly worked through the first advent of code problem (https://github.com/kyleellefsen/lean_aoc_2023). I've played around with other functional languages since then and now I'm going through the Functional Programming in Lean book. I do have quite a few questions and will be happy to attempt to find answers for others'. Looking forward to seeing y'all later today.

[Chris Bailey]

how do we enter?

[Chris Bailey]

ok theres a doorbell

[Kyle Ellefsen]

I just rang as well

[David Stainton 🦡]

Here's the newer Lean 4 games, including that logic game: https://adam.math.hhu.de/
And for books on proving things in Lean, I was considering to maybe start with one of these:

• https://hrmacbeth.github.io/math2001/
• https://leanprover.github.io/logic_and_proof/introduction.html
  ... i'll look up the test tomorrow

[David Stainton 🦡]

Lean 4 tactic cheat sheet https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf

[Kyle Ellefsen]

That logic-and-proof book looks interesting, I'll check it out. I'm currently reading "How to Prove It: A Structured Approach" (which is very well written) and it seems like good topic overlap.

[David Stainton 🦡]

I've got that book and haven't yet started to read it. But also the author, Daniel Velleman wrote a Lean prover book...

[David Stainton 🦡]

https://djvelleman.github.io/HTPIwL/

[David Stainton 🦡]

"How To Prove It With Lean"

[Kyle Ellefsen]

Very cool!

I'm noticing that a lot of these guides were written a while ago and lean 4.10 isn't executing them. For example, the "assume" tactic and the "begin ... end" pattern doesn't seem to work. These show up in https://leanprover.github.io/logic_and_proof/the_natural_numbers_and_induction_in_lean.html and https://djvelleman.github.io/HTPIwL/ (and even in the reference manual https://leanprover.github.io/reference/tactics.html).

Do y'all know if lean made breaking changes or if I'm doing something wrong? If these are breaking changes, I'd rather go through a book/guide that has tests on its example code.

[David Stainton 🦡]

begin and end is definitely Lean 3 . In Lean 4 we just write "by ..."

[Ruben Van de Velde]

HTPIwL looks like lean 4, Logic and Proof and https://leanprover.github.io/reference/index.html are definitely lean 3. I wish we could put a big warning on those

[Ruben Van de Velde]

I don't know where either of them comes from, though

[Kyle Ellefsen]

HTPIwL seems to make frequent use of the assume tactic (e.g. https://github.com/djvelleman/HTPIwL/blob/main/Chap3.qmd#L111-L114), but when running in lean I get an "unknown tactic' error (here). This is a very basic question, but what imports are required to use that tactic?

I cloned the https://hrmacbeth.github.io/math2001/ repo and started working through that; it uses lean 4.3 and everything is working for me in VSCode so far. Looks like an excellent book!

[Kyle Ellefsen]

To answer my own question, it seems that a lot of the tactics used in HTPIwL are defined in a lean file as part of that project, and that includes that assume tactic. https://djvelleman.github.io/HTPIwL/Appendix.html

[Kyle Miller]

For what it's worth, the analogous core Lean tactic would be intro (h2 : ¬R)

[Kyle Ellefsen]

Kyle Miller said:

For what it's worth, the analogous core Lean tactic would be intro (h2 : ¬R)

Got it working. For future reference.

[David Stainton 🦡]

okay i'll start reading The Mechanics of Proof. @Kyle Ellefsen thanks for figuring out the lean books.
our next meeting, i think we should try to use the Noisebridge's projector and projector screen that way we can easily show off code to multiple people. It's probably located in one of the smaller rooms. If we can't find it or if they won't let us use I can buy one and bring it the following Lean meetup.

[David Stainton 🦡]

um also... I do want to work my way slowly through the Functional Programming in Lean. I'll probably start reading that again soon. I stopped reading about halfway or so.

[Kyle Ellefsen]

@David Stainton sounds good. I'll also work through both books.

[Pietro Monticone]

Kyle Ellefsen said:

HTPIwL seems to make frequent use of the assume tactic (e.g. https://github.com/djvelleman/HTPIwL/blob/main/Chap3.qmd#L111-L114), but when running in lean I get an "unknown tactic' error (here). This is a very basic question, but what imports are required to use that tactic?

I cloned the https://hrmacbeth.github.io/math2001/ repo and started working through that; it uses lean 4.3 and everything is working for me in VSCode so far. Looks like an excellent book!

The assume tactic is defined here in the accompanying package HTPILeanPackage.

[Koundinya Vajjha]

Any more Lean meetings planned? I missed the last one. I'm in the East Bay in Fremont.

[David Stainton 🦡]

@Koundinya Vajjha Yes! We want to meet sometime this week at Noisebridge in San Francisco. What time works for you all? Last time we met at 2pm on a Thursday. It's best if we can find a time that works and stick to it. That way I can eventually put it up on the Noisebridge wiki schedule...

[Kim Morrison]

Ruben Van de Velde said:

HTPIwL looks like lean 4, Logic and Proof and https://leanprover.github.io/reference/index.html are definitely lean 3. I wish we could put a big warning on those

[Kim Morrison]

I've put a big warning on the Lean 3 reference manual.

[David Stainton 🦡]

Koundinya Vajjha said:

Any more Lean meetings planned? I missed the last one. I'm in the East Bay in Fremont.

We're planning on meeting Thursday at 2pm again this week.

[Koundinya Vajjha]

Aw shucks, can't make it this week! I'll keep an eye out for the next one.

[Chris Bailey]

Meeting notes: https://gist.github.com/ammkrn/1688038761909b609b44fd411ec62c22

https://lean-lang.org/lean4/doc/examples/widgets.lean.html
https://github.com/leanprover-community/ProofWidgets4
https://leanprover.github.io/theorem_proving_in_lean4/conv.html?highlight=conv#other-tactics-inside-conversion-mode

[David Stainton 🦡]

I'm enjoying Chapter 5 the Logic chapter. My brain doesn't want to do the exercises in chapters 1-4. Was tortured in school already.

[David Stainton 🦡]

Fixed my NIKE to KEM adapter, made it work as a ordinary function that returns a KEM... it's weird though because the KEM structure functions are acting as a closures around the arguments passed into the function that created the KEM structure instance

[David Stainton 🦡]

I think I need to learn how to use SatisfiesM as soon as possible to fix a few technical debt aspects in my code:

1. stop using OS RNG... the "RNG" should be part of it's monadic context, I'd like the option to replace it with a deterministic RNG like an HKDF or ChaCha20 etc
2. currently doing caveman style error handle via if bad condition occured then panic, else continue.

I implemented a security preserving KEM combiner from one of the best cryptography papers on the subject...
But the code itself is sloppy looking with my "panic" error handling... otherwise it would have been a 3 line function closely resembling the math from their paper.

/-
SplitPRF can be used with any number of KEMs
and it implement split PRF KEM combiner as:

  cct := cct1 || cct2 || cct3 || ...
       return H(ss1 || cct) XOR H(ss2 || cct) XOR H(ss3 || cct)

in order to retain IND-CCA2 security
as described in KEM Combiners  https://eprint.iacr.org/2018/024.pdf
by Federico Giacon, Felix Heuer, and Bertram Poettering
-/

def hashSize := 32

def xorByteArrays (a b : ByteArray) : ByteArray :=
  if a.size ≠ b.size then
    panic! "xorByteArrays: ByteArrays must be of equal size"
  else
    ByteArray.mk (Array.zipWith a.data b.data fun x y => x ^^^ y)

def splitPRF (hash : ByteArray → ByteArray) (ss : List ByteArray) (ct : List ByteArray) : ByteArray :=
  if ss.length != ct.length then
    panic! "splitPRF failure: mismatched List lengths"
  else
    let bigCt : ByteArray := ct.foldl (fun acc blob => acc ++ blob) ByteArray.empty
    (ss.map (fun x => hash (x ++ bigCt))).foldl (fun acc h => xorByteArrays acc h) (ByteArray.mk (Array.mkArray hashSize 0))

[David Stainton 🦡]

Perhaps in our weekly meetings we should audit some of Batteries or the Lean standard library like the Prelude section.

[Kyle Ellefsen]

Perhaps in our weekly meetings we should audit some of Batteries or the Lean standard library like the Prelude section.

I'm really digging into the standard library continuing on the AOC. Lists, Arrays, HashMaps, HashSets (which, I don't believe have a "set difference" operator defined on, I've had to write my own). I've added a the docs to my search bar so I can search by typing l.

image.png

My code for day 3 pt 2 of AOC 2023: https://github.com/kyleellefsen/lean_aoc_2023/blob/main/day03/pt2.lean

[David Stainton 🦡]

what's AOC?

[Kyle Ellefsen]

Advent of Code. https://adventofcode.com/2023/about

[David Stainton 🦡]

Yeah using the standard library stuff is making me curious about it's source code, how it's written. maybe i can even understand some of it.

[David Stainton 🦡]

there a programming puzzles for learning cryptography, called cryptopals https://cryptopals.com/ they get super tricky real fast. i got most of the way through the first and second sets of problems and just sort of lost interest after that. i do believe i'm capable of solving all of them... but it sort of feels like a waste of time when i could be writing a cryptography library.

[David Stainton 🦡]

your code looks impressively complicated... like i'm sure it had to be to solve whatever problem that was

[Kyle Ellefsen]

I only know a pretty small subset of lean; I'm sure there are more elegant ways of doing this with much more of the language, but gotta start somewhere.

A couple pain point:

• In my numpos_of_chargrid function, I wanted to iterate through each dimension of the 2D array, so I nested a row.foldl inside a grid.foldl, and created a tuple of objects in each accumulator; I found reasoning about what to put into the accumulator of each tricky. I don't know if it's because I'm still getting used to the .fold pattern as a substitute for for loops, or if there's a better best practice.
• A few things I instinctively reached for that I expected would be in the standard library weren't. Hashset difference operations, numpy-like array operations like .sum(), etc. I assume the standard library is still being built out.

A few things I loved:

• Using by omega to prove a list/array index was in bounds; it's so easy.
• Pinning #eval lines in the lean infoview. I could really quickly write functions by leaving out the function return type, and constantly seeing what the function was returning on sample data as I built it up. Seeing the in-progress data structure removes a lot of mental effort as I built up functions
• Chaining pipe operators. Combined with using #eval, it's really easy to visualize the data flow with all the pipes on their own line. Also very easy to reason about pieces of the code.

Looking forward to digging deeper.

[Kyle Ellefsen]

Also, I posted this in another thread, but I could not figure out how to run my code using lean --run myfile.lean, because i'm importing Mathlib, and my global lean install cannot find the mathlib stored inside my git repo's .lake directory. I'd really appreciate any help on this, I spent several hours on this and I remember back in December I also got stuck on it.

[David Stainton 🦡]

i think you need lake exe lean run blah or something similar

[David Stainton 🦡]

probably you'll get a faster response if you post it in lean4

[Kyle Ellefsen]

lake exe cache get builds a cache. The problem is that lean doesn't know where to find mathlib.

[Matthew Ballard]

lake env lean --run XYZ?

[David Stainton 🦡]

yeah! that's what i was going for

[Kyle Ellefsen]

That's it! Thanks @Matthew Ballard!!!

[David Stainton 🦡]

I don't yet know what I'm doing but I managed to use StateM from Batteries.. and it allowed me to use "let mut" and a for loop inside a "do" block:

import Batteries.Classes.SatisfiesM

structure LadderState :=
  a : ZMod p
  b : ZMod p
  c : ZMod p
  d : ZMod p

abbrev LadderM := StateM LadderState

def scalar_mult (scalarBytes : ByteArray) (pointBytes : ByteArray) : LadderM Unit := do
  let clampedScalar := clampScalar scalarBytes
  let point := toField pointBytes

  let mut a : ZMod p := 1
  let mut b : ZMod p := point
  let mut c : ZMod p := 0
  let mut d : ZMod p := 1
  let mut r : UInt8 := 0

  for i in (List.range 414).reverse do
    r := (clampedScalar.get! (i >>> 3) >>> UInt8.ofNat (i &&& 7)) &&& 1
    (a, b) := cswap r a b
    (c, d) := cswap r c d
    let e := a + c
    a := a - c
    c := b + d
    b := b - d
    d := e^2
    let f := a^2
    a := a * c
    c := b * e
    let e := a + c
    a := a - c
    b := a^2
    c := d - f
    a := c * A24
    a := a + d
    c := c * a
    a := d * f
    d := b * point
    b := e^2
    (a, b) := cswap r a b
    (c, d) := cswap r c d

  modify fun state => { state with a := a * c⁻¹ }

def scalar_mult_base (scalarBytes : ByteArray) : ByteArray :=
  let (_, st) := (scalar_mult scalarBytes basepoint).run {
    a := 1,
    b := toField basepoint,
    c := 0,
    d := 1
  }
  fromField st.a

[David Stainton 🦡]

it kind of looks like rust when i those language features

[Kyle Miller]

VS Code / Lean hint: if you hover over StateM you can see import Init.Control.State. That means StateM comes from core Lean (the Init module is the prelude).

[Bjørn Kjos-Hanssen]

@Matthew Ballard that's what I was looking for as well! Should have known to search within "San Francisco"

[David Stainton 🦡]

Lean study meetup: Tomorrow, Thursday 2pm at Noisebridge https://www.noisebridge.net/wiki/Noisebridge

[Carbon]

I’m learning Lean mostly using the Functional Programming in Lean book. I am interested in implementing cryptography primitives for fun, learning about them, and program correctness. No background in dependent typing, and pure functional programming. I’ve implemented Keccak e.g. SHA3/SHAKE in Lean. Interested in improving the implementation, and then moving to post quantum ciphers. I am based in San Francisco, and I am very much interested to join!

[David Stainton 🦡]

Carbon said:

I’m learning Lean mostly using the Functional Programming in Lean book. I am interested in implementing cryptography primitives for fun, learning about them, and program correctness. No background in dependent typing, and pure functional programming. I’ve implemented Keccak e.g. SHA3/SHAKE in Lean. Interested in improving the implementation, and then moving to post quantum ciphers. I am based in San Francisco, and I am very much interested to join!

Very cool! So far I've only implemented a merkle hash tree (a port from haskell) and X25519 ECDH... and a security preserving KEM combiner.But there's a long list of cryptographic primitives that I want to implement in Lean so that I can write prototypes of various protocols. Let's talk tomorrow at Noisebridge?

[David Stainton 🦡]

I have incorrectly implemented X448 and X41417 in Lean. I know it's incorrect because the vector tests fail. It's just a matter of comparing internal states with a known working implementation. With X448 that's easy. Plenty of them. But with the more obscure safe curves like X41417... I literally could not find any test vectors or runnable implemenetations. Just a 9 year old rust implementation that I cannot compile.

[David Stainton 🦡]

It would be cool if someone implemented MLKEM768 (and possible MLKEM1024) in Lean. What post quantum primitives did you have in mind? Also someone should fixup Joe Hendrix's bitrot Classic McEliece pq KEM, no?

[David Stainton 🦡]

Come tomorrow. Bring you laptop for a show and tell of your code. We'll try our best to help you improve it.

[Carbon]

I was thinking of implementing ML-DSA for a start; I wrote (a few) lines of code yesterday.

Awesome! I will meet you all today. My name is Gerald. Very interested in feedback, discuss improvements, future plans, Lean and Crypto (some of my colleagues are involved with cryptopals, and cryptohack, amongst other things).

[David Stainton 🦡]

Years ago i worked on the cryptopals exercises... I passed challenge 12 in the 2nd set and then just sort of lost interest.
Currently I'm part of a research team that designs/makes the Katzenpost mixnet/anonymous communication network.
We recently submitted an academic paper and it got rejected for lack of machine checkable proofs!!
My future goal is to produce machine checkable protocol proofs in Lean. I've written a bunch of ProVerif and I know that it cleverly uses the Pi calculus to synthesize proofs and whatnot; but I'd much rather use Lean and than ProVerif because it's way more fun and more powerful... but I have no idea how i'm going to prove protocol properties. First I need to actually write a protocol in Lean.

[David Stainton 🦡]

PXL_20240905_221519989.jpg

[Kyle Ellefsen]

I took the subtyping example we worked on together today and made a minimal version that uses the nice arr[idx] notation:

@[reducible]
def Array25 := {val: Array UInt64 // val.size=25} -- subtype with predicate

instance : GetElem Array25 ℕ UInt64 (λ _ i ↦ i < 25) where
  getElem arr idx _ := arr.val[idx]

def example_ok_access (arr25 : Array25) :=
  arr25[10]

def example_bad_access (arr25 : Array25) :=
  arr25[25] -- failed to prove index is valid, possible solutions: ...

def regular_arr : Array UInt64 := (List.range 25).map (λa↦(a*2).toUInt64) |>.toArray
def arr25 : Array25 := ⟨regular_arr, by rfl⟩

#eval regular_arr[10]
#eval example_ok_access arr25 -- 20
#eval example_bad_access arr25 -- cannot evaluate expression that depends on the `sorry` axiom.
#eval arr25[25]! -- PANIC

[Chris Bailey]

Kyle beat me to it, but here are some more mwes @Carbon : https://gist.github.com/ammkrn/adc36566e9402afaaa27797bcd5e1609

[Carbon]

This is awesome, thanks to both of you. This sure beats the ugly solution I was working on.

private def theta (A : State) : State := Id.run do
  let mut ⟨A,h⟩ := A
  have hlt (i : Fin 25) : i  < A.size  := by
    rw [h]
    simp
  let C0 := (A[0]'(hlt 0)) ^^^ (A[5]'(hlt 05)) ^^^ (A[10]'(hlt 10)) ^^^ (A[15]'(hlt 15)) ^^^ (A[20]'(hlt 20))
-- snip

[Carbon]

The code seems to validate when using an appropriate instance of getElem, and the subTypeModify as detailed above, with a short proof of concept implementation of theta:

private abbrev State := { val : Array UInt64 // val.size = 25}

private def mkState : State :=
  ⟨ mkArray 25 0, by decide ⟩

instance : GetElem State Nat UInt64 (λ _ i ↦ i < 25) where
  getElem state idx _ :=  state.val[idx]

def subtypeModify {A : Type u} {n : Nat} (xs : { val : Array A // val.size = n }) (i : Nat) (f: A →  A ) : { a : Array A // a.size = n } :=
  let val := xs.val.modify i f
  ⟨val, (Array.size_modify xs.val i f) ▸ xs.property⟩

private def theta' (A : State) : State := Id.run do
  let mut A := A

  let C0 := A[0] ^^^ A[5] ^^^ A[10] ^^^ A[15] ^^^ A[20]
  let C1 := A[1] ^^^ A[6] ^^^ A[11] ^^^ A[16] ^^^ A[21]
  let C2 := A[2] ^^^ A[7] ^^^ A[12] ^^^ A[17] ^^^ A[22]
  let C3 := A[3] ^^^ A[8] ^^^ A[13] ^^^ A[18] ^^^ A[23]
  let C4 := A[4] ^^^ A[9] ^^^ A[14] ^^^ A[19] ^^^ A[24]

  let mut D0 := C4 ^^^ ((C1 <<< 1) ||| (C1 >>> 63))

  A := subtypeModify A 0 (λ _ => A[0] ^^^ D0)
  A := subtypeModify A 5 (λ _ => A[5] ^^^ D0)
  A

However, when I implement the full theta, I am getting the following Lean error message:

(deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.
Additional diagnostic information may be available using the `set_option diagnostics true` command.Lean 4
A : State

I tried to increase the heartbeat value to 600000 without success. This is the full theta definition that Lean is rejecting:

private def theta (A : State) : State := Id.run do
  let mut A := A

  let C0 := A[0] ^^^ A[5] ^^^ A[10] ^^^ A[15] ^^^ A[20]
  let C1 := A[1] ^^^ A[6] ^^^ A[11] ^^^ A[16] ^^^ A[21]
  let C2 := A[2] ^^^ A[7] ^^^ A[12] ^^^ A[17] ^^^ A[22]
  let C3 := A[3] ^^^ A[8] ^^^ A[13] ^^^ A[18] ^^^ A[23]
  let C4 := A[4] ^^^ A[9] ^^^ A[14] ^^^ A[19] ^^^ A[24]

  let mut D0 := C4 ^^^ ((C1 <<< 1) ||| (C1 >>> 63))

  A := subtypeModify A 0 (λ _ => A[0] ^^^ D0)
  A := subtypeModify A 5 (λ _ => A[5] ^^^ D0)
  A := subtypeModify A 10 (λ _ => A[10] ^^^ D0)
  A := subtypeModify A 15 (λ _ => A[15] ^^^ D0)
  A := subtypeModify A 20 (λ _ => A[20] ^^^ D0)

  D0 := C0 ^^^ ((C2 <<< 1) ||| (C2 >>> 63))

  A := subtypeModify A 1 (λ _ => A[1] ^^^ D0)
  A := subtypeModify A 6 (λ _ => A[6] ^^^ D0)
  A := subtypeModify A 11 (λ _ => A[11] ^^^ D0)
  A := subtypeModify A 16 (λ _ => A[16] ^^^ D0)
  A := subtypeModify A 21 (λ _ => A[21] ^^^ D0)

  D0 := C1 ^^^ ((C3 <<< 1) ||| (C3 >>> 63))

  A := subtypeModify A 2 (λ _ => A[2] ^^^ D0)
  A := subtypeModify A 7 (λ _ => A[7] ^^^ D0)
  A := subtypeModify A 12 (λ _ => A[12] ^^^ D0)
  A := subtypeModify A 17 (λ _ => A[17] ^^^ D0)
  A := subtypeModify A 22 (λ _ => A[22] ^^^ D0)

  D0 := C2 ^^^ ((C4 <<< 1) ||| (C4 >>> 63))

  A := subtypeModify A 3 (λ _ => A[3] ^^^ D0)
  A := subtypeModify A 8 (λ _ => A[8] ^^^ D0)
  A := subtypeModify A 13 (λ _ => A[13] ^^^ D0)
  A := subtypeModify A 18 (λ _ => A[18] ^^^ D0)
  A := subtypeModify A 23 (λ _ => A[23] ^^^ D0)

  D0 := C3 ^^^ ((C0 <<< 1) ||| (C0 >>> 63))

  A := subtypeModify A 4 (λ _ => A[4] ^^^ D0)
  A := subtypeModify A 9 (λ _ => A[9] ^^^ D0)
  A := subtypeModify A 14 (λ _ => A[14] ^^^ D0)
  A := subtypeModify A 19 (λ _ => A[19] ^^^ D0)
  A := subtypeModify A 24 (λ _ => A[24] ^^^ D0)

  A

[David Stainton 🦡]

Your subtypeModify seems to be missing the definition of f in it's signature so I couldn't try it.

[Carbon]

Good catch, sorry - I updated the code snippets above. I am getting the same error (and it puts quite the load on my machine).

[Chris Bailey]

There's something nonlinear happening in long let chains when synthesis of these inequalities for array indices are generated in each binding. Mwe:

-- Elaborates normally if the `h` argument is removed.
set_option linter.unusedVariables false in
def subtypeSet (xs : {val : Array UInt64 // val.size = 25}) (i : Nat) (h : i < 25 := by decide) : {val : Array UInt64 // val.size = 25} :=
  xs

set_option linter.unusedVariables false in
def theta (x : {val : Array UInt64 // val.size = 25}) : {val : Array UInt64 // val.size = 25} :=
  let A := subtypeSet x 0
  let A := subtypeSet x 1
  let A := subtypeSet x 2
  let A := subtypeSet x 3
  let A := subtypeSet x 4
  let A := subtypeSet x 5
  let A := subtypeSet x 6
  let A := subtypeSet x 7
  let A := subtypeSet x 8
  let A := subtypeSet x 9
  let A := subtypeSet x 0
  let A := subtypeSet x 1
  let A := subtypeSet x 2
  let A := subtypeSet x 3
  let A := subtypeSet x 4
  let A := subtypeSet x 5
  let A := subtypeSet x 6
  let A := subtypeSet x 7
  -- Progressively more slow-down as these are uncommented
  --let A := subtypeSet x 8
  --let A := subtypeSet x 9
  --let A := subtypeSet x 0
  --let A := subtypeSet x 1
  --let A := subtypeSet x 2
  --let A := subtypeSet x 3
  --let A := subtypeSet x 4
  A

[Chris Bailey]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Slow.20elaboration.20of.20lets/near/468282213

[David Stainton 🦡]

https://www.typetheoryforall.com/episodes/z3-and-lean-the-spiritual-journey

[David Stainton 🦡]

^podcast interview with Leo, talking about some of the history of Lean

[Carbon]

I also liked https://www.typetheoryforall.com/episodes/haskell-lean-idris-and-the-art-of-writing-1

"In this episode we talk with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer."

[David Stainton 🦡]

Carbon said:

I also liked https://www.typetheoryforall.com/episodes/haskell-lean-idris-and-the-art-of-writing-1

"In this episode we talk with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer."

yeah that's another great episode. Type Theory Forall podcast is great!

[David Stainton 🦡]

I'm looking forward to seeing you all tomorrow at Noisebridge 2pm.

I just have some minor Lean language questions and I'm hoping to get help on the Logic proof game as I find myself stuck.
I'm hoping you all have some more Lean code to show us and questions or discussion topics.

[Carbon]

I've logged the issue on Github.

[Carbon]

I can't attend today, hopefully next week.

[Kyle Ellefsen]

I also won’t be able to come today, but can next week.

[Chris Bailey]

Same, unfortunately.

[Kevin Buzzard]

End of October/beginning of Nov I'll be in town! Do you have a regular weekly thing going now?

[David Stainton 🦡]

Kevin Buzzard said:

End of October/beginning of Nov I'll be in town! Do you have a regular weekly thing going now?

Yay! Yeah stop by Noisebridge on a Thursday at 2pm for our Lean theorem prover meetup.

But also... do you want to give a talk about Lean at Noisebridge at a different time?
Maybe more people would attend such a talk if I announced it at one of the Noisbridge meetings and on their mailing list as well.

[David Stainton 🦡]

hmm I think we might be the only Lean theorem prover meetup that is hosted at a hackerspace. https://www.noisebridge.net/wiki/Noisebridge

okay I'm not going to Noisebridge today since i'd be the only one. see y'all at Noisebridge next week.

[Alok Singh]

you guys meeting today?

[David Stainton 🦡]

Yes. 2pm at noisebridge.

[Kyle Ellefsen]

I'm at Noisebridge in the upstairs front room.

[Kevin Buzzard]

I'll be in San Francisco on Thurs 31st Oct -- will there be a meeting then?

[Quinn]

Man I gotta remember to come to these

[Tom]

Oh, just found this! Also a beginner Lean coder. I am in the South Bay, so may not be able to come regularly but I subscribed to the thread now!

[David Stainton 🦡]

Kevin Buzzard said:

I'll be in San Francisco on Thurs 31st Oct -- will there be a meeting then?

Yes. Definitely.

[David Stainton 🦡]

Tom said:

Oh, just found this! Also a beginner Lean coder. I am in the South Bay, so may not be able to come regularly but I subscribed to the thread now!

Hi Tom. Cool. All I use Lean for is functional programming thus far. Mostly cryptography. Come to Noisebridge sometime and show us your Lean code and we'll talk about functional programming in Lean!

[Tom]

Sounds great, thanks! I'm currently about to finish FPiL and am watching lectures on dependent types and HoTT.
Also, finding interesting ways of breaking Lean, and I've made some minor PRs against Lean itself, even though some are... controversial :smile:

[Tom]

Definitely more interested in using Lean as an interesting functional language but I am also an hobbyist mathematician so am planning to learn more about Mathlib/tactics next.

[David Stainton 🦡]

I work on the Katzenpost decryption mix network. We're a group of cypherpunks, we have one mathematician on our research team and we collaborate with various cryptographers. Mixnets are inherently more interesting and complicated than mere cryptographic protocols because we're trying to gain anonymity/privacy notions, not merely security notions. I was initially interested in using Lean to make machine checkable proofs for some of our protocol designs, however the lean software that is publicly available is very far away from being about to prototype any of our protocols. Here's a taste of what we can do: https://katzenpost.network/research/Literature_overview__website_version.pdf

[Kyle Ellefsen]

David Stainton 🦡 said:

Kevin Buzzard said:

I'll be in San Francisco on Thurs 31st Oct -- will there be a meeting then?

Yes. Definitely.

I'm traveling for the next 3 Thursdays, but I'll be back at Noisebridge for October 31st. :jack-o-lantern: :ghost: :computer:

[Quinn]

is the meetup weekly? on thursdays?

[David Stainton 🦡]

yes every thursday at 2pm at noisebridge. but i can't make it today because of a dentist appointment. And Kyle just said he won't make it today...so I'm not sure if anyone else will come.

[Chris Bailey]

I'll be there today, ~10 minutes late.

[Chris Bailey]

The venue is apparently closed right now. If anyone does show up and sees this, send me a dm or something, I'll be in the neighborhood for a little bit.

[David Stainton 🦡]

Chris Bailey said:

The venue is apparently closed right now. If anyone does show up and sees this, send me a dm or something, I'll be in the neighborhood for a little bit.

I'm sorry Noisebridge was closed at that time. If that ever happens again it might be possible to contact someone on the Noisebridge Discord channel and ask to be let into the building: https://www.noisebridge.net/wiki/Discord

[David Stainton 🦡]

Is anyone planning on attending the Lean theorem prover meetup tomorrow?

[Chris Bailey]

If there's buy-in this week I'll be there.

[Carbon]

I will be present

[David Stainton 🦡]

Okay cool.

[David Stainton 🦡]

anyone planning to come to the Lean Theorem prover meet up at the Noisebridge hacker space tomorrow at 2pm?

[Carbon]

I can’t make it unfortunately. Hopefully next week!

[Kevin Buzzard]

Next week (31st) I'll also be rocking up at Noisebridge at 2pm, assuming something's happening.

[Chris Bailey]

I'll be in the city today, I'll stop by and see if anyone's around.

[Tom]

Kevin Buzzard said:

Next week (31st) I'll also be rocking up at Noisebridge at 2pm, assuming something's happening.

Darn. I was looking forward to joining but had to fly back to Europe for family reasons. I hate to miss this, have fun!

[Quinn]

me and my coauthor are coming

[Quinn]

2p?

[David Stainton 🦡]

Yes 2pm at noisebridge. Ring the buzzer.

[Robert Maxton]

I'll be there as well!

[Carbon]

I will be there

[Robert Maxton]

Running a bit late, Google says I'll be there around 2:20 ^.^;

[Robert Maxton]

... Google also says Noisebridge won't open until 3, but I assume "thus the buzzer"?

[Carbon]

I am in, it is open ( but you still have to ring the buzzer)

[David Stainton 🦡]

https://www.noisebridge.net/wiki/Front_Door

[Quinn]

Where is the buzzer? Is it 272 capp st?

[Quinn]

I'm here but I can't fund red buzzer

[Quinn]

I see a payphone painted red

[Chris Bailey]

Hopefully you're not still outside, but for anyone else it's a black button on what would be the right hand side of the "door frame", about waist/chest high.

[David Stainton 🦡]

Be sure to ring the buzzer upon arrival at noisebridge... Or contact us here and we'll let you in.

[Quinn]

@Robert Maxton see also topos' string diagram editor https://github.com/ToposInstitute/CatColab

[Quinn]

@Chris Bailey where's your rust codebase?

[Kevin Buzzard]

Great to meet you all!

[Chris Bailey]

Quinn said:

Chris Bailey where's your rust codebase?

The rust one is here, the book is here, live version here.

[Alok Singh]

neurips_2024.pdf

no citations/figs bc latex issues and midnight deadline, have to add them in. the main text is there though

[Alok Singh]

name is bc it uses neurips template :lol:

[Yakov Pechersky]

Not sure why you need the sorry autoparam in the length proposition field in your vector structure

[Carbon]

(oops wrong chat)

[Alok Singh]

Yakov Pechersky said:

Not sure why you need the sorry autoparam in the length proposition field in your vector structure

Because I argue for sorry friendly programming, in this case maybe too friendly but it was shorter than adding more code to put sorries only at use sites.

[Alok Singh]

Coming to meetup today, 230 eta

[Kyle Ellefsen]

I’m here but it’s locked

[Kyle Ellefsen]

Waiting for someone with a key to show up.

[David Stainton 🦡]

Kyle Ellefsen said:

Waiting for someone with a key to show up.

still no entry into building? I'm trying to contact people on the Noisebridge discord to get someone to open the door for you.

[Kyle Ellefsen]

No still waiting

[Kyle Ellefsen]

Thanks

[David Stainton 🦡]

omg... i can't seem to find anyone with a key to the building. I'm sorry. To solve this problem it's probably a good idea for one of the Lean people to get a key; probably to get a key we might have to pay membership dues and attend the occasional weekly noisebridge meeting.

[David Stainton 🦡]

@Kyle Ellefsen I'm told that Noisebridge door status is now "open". Did you get into the building yet?

[David Stainton 🦡]

Here's the Noisebridge door status channel: https://discord.com/channels/720514857094348840/1034916379486322718

[Kyle Ellefsen]

Yes we got in! 3 of us here. Thanks!

[David Stainton 🦡]

https://github.com/katzenpost/lean-ffi

[David Stainton 🦡]

Hey my lean-ffi example repo above ^ I updated it to not use mathlib... and it uses the latest stable version of lean 4.13.0

[David Stainton 🦡]

I think the lean-sys rust crate evidently doesn't always need to be updated for it to work with future versions of lean

[Kyle Ellefsen]

I’m at Noisebridge, looking for a space because our usual table has electronics on it.

[Max Stoumen]

Yo I’m here too, where we meeting

[Robert Maxton]

Just arrived

[Kyle Ellefsen]

We are in the basement

[Robert Maxton]

(Apparently we're downstairs)

[Leni Aniva]

Are there more meetings coming up

[David Stainton 🦡]

Every week, 2pm at noisebridge hacker space

[Leni Aniva]

David Stainton 🦡 said:

Every week, 2pm at noisebridge hacker space

which day every week?

[David Stainton 🦡]

Thursday

[Kyle Ellefsen]

We’re in the electronics room today.

[Chris Bailey]

Can you let a brother in

[Alok Singh]

If one of you sets up a call, I can join (in Cupertino today)

[Chris Bailey]

I'll be out of town this week for thanksgiving.

[Kyle Ellefsen]

I’ll also be away.

[Alok Singh]

Happy thanksgiving to y’all, thankful for your company and knowledge

[Quinn]

we're out of space for the talks day, but more room for hackathon if you wanna come by and jam https://proof-scaling-meeting.vercel.app/ (some of you have already registered for one or two days) --- please don't use the registration form, DM me instead- if you're not already invited to the first day (talks) this is only an invitation to the second day

[Robert Maxton]

Running late, but will be there today

[Julian Berman]

Are all of you doing OK I hope?

[Julian Berman]

Did it reach SF?

[Robert Maxton]

.... Good question, seconded

[David Stainton 🦡]

If someone wants to start a Lean meetup in the east bay... It will be a little farther from the ocean and thus hopefully unaffected by tsunamis. But in San Francisco clearly we're all swimming underwater right now.

[David Stainton 🦡]

I won't be at noisebridge today because I'm trying to actually work on my mixnet project instead of having fun talking with you all about how cool Lean is.

[Robert Maxton]

At Noisebridge; is anyone else here?

[Kyle Ellefsen]

I’m sick today so couldn’t make it, not sure if anyone else is there.

[Kyle Ellefsen]

Julian Berman said:

Are all of you doing OK I hope?

The tsunami warning initially estimated it would impact SF at 12:10 PM but was cancelled just before then.

https://www.sfchronicle.com/weather/article/tsunami-warning-issued-canceled-19962346.php

[Greg Shuflin]

oh huh there's a regular lean meetup at noisebridge? I'm local to the sf bay area

[Robert Maxton]

Every thursday, in theory!
(The theory is because there appears to be nobody else here :v)

[Robert Maxton]

I'll be hanging out upstairs for a while though

[Kyle Ellefsen]

Yes every Thursday at 2. It’s pretty rare for no one to be there, usually at least 2 of us. Sorry Robert.

[Chris Bailey]

Yeah, there happened to be a conference in Berkeley yesterday that siphoned off most of the regulars. I'll be at noisebridge on the 12th.

[Alok Singh]

I’ll be there in an hour

[Robert Maxton]

Planning to be there tomorrow!

[Greg Shuflin]

I'm going to try to make this tomorrow

[Chris Bailey]

I'll be there today.

[Ching-Tsun Chou]

Where do you meet?

[Alok Singh]

Noisebridge, second floor

[Ching-Tsun Chou]

Thanks!

[Chris Bailey]

(at 2:00 pm)

[Ching-Tsun Chou]

Thanks! I probably won't be there.

[Kyle Ellefsen]

I’ll be there a bit later.

[Greg Shuflin]

fyi I am here now, I'm not sure if anyone else is

[Greg Shuflin]

not super-surprising if there's not much attendance the day after christmas

[Alok Singh]

oh i totally forgot it was thurs. anyone show?

[Greg Shuflin]

Alok Singh said:

oh i totally forgot it was thurs. anyone show?

Seemed like it was just me, although there were some other people doing other things at Noisebridge there at the time, so I hung out for a while.

[Chris Bailey]

I won't be able to attend this week (the 2nd), should be back next week.

[Kyle Ellefsen]

Same, I'm out this week but will be back next week.

[Kyle Ellefsen]

Sample code for proving extensional equality between functions:

def sum2 (n:ℕ) :=
  match n with
  | 0 => 1
  | m+1 => 2^n + sum2 m

def sum2' (n:ℕ) :=
  2^(n+1) - 1

example : sum2 = sum2' := by
  funext n
  induction n with
  | zero => rfl
  | succ m ih =>
    simp [sum2, sum2', ih]
    ring_nf
    omega

[Chris Bailey]

I'm out of town for work this week; won't make it today (23rd) but will be back for the 30th.

[Kyle Ellefsen]

I also won't be able to make it today.

[Greg Shuflin]

probably should've checked this before I headed into sf, but I am here today

[Alok Singh]

sorry bud, not coming either

[David Stainton 🦡]

Will anyone be attending the Lean meeting tomorrow in San Francisco at noisebridge? I'm thinking about coming tomorrow.

[Kyle Ellefsen]

I'll be there tomorrow at 2 (the usual time).

[Alok Singh]

@Robert Maxton ? @Winston Yin (尹維晨) ? (you two should meet too)

[Robert Maxton]

Probably not, I make plans for every other Thursday
If you show up next week I'll be there tho!

[Winston Yin (尹維晨)]

I’m looking forward to meeting some of you tomorrow! Coming from Berkeley

[Greg Shuflin]

I'll be there today

[Kyle Ellefsen]

I’m running 15 minutes late.

[Chris Bailey]

Can someone let me in?

[Robert Maxton]

Will be there tomorrow!

[Winston Yin (尹維晨)]

I most likely can’t tomorrow :( have a meeting in Berkeley at 3

[Kyle Ellefsen]

Unfortunately I'll also not be able to make it today.

[Chris Bailey]

I'll be a little late.

[Greg Shuflin]

I'll be there soon

[Greg Shuflin]

I expect to attend tomorrow

[Kyle Ellefsen]

I’ll be there as well

[Alok Singh]

Same. @Winston Yin (尹維晨)? @Robert Maxton ?

[Winston Yin (尹維晨)]

I can make it today, but it looks like this is an off-week for Robert again

[Winston Yin (尹維晨)]

Btw I'm driving from Berkeley @Alok Singh if you'd like a ride

[Alok Singh]

I’m driving from Cupertino but thanks

[Alok Singh]

Wanna get dinner after tho

[Winston Yin (尹維晨)]

I've got plans after, hence the driving

[Robert Maxton]

Bleh, never fails. :wry: Wasn't planning on showing up today but it's not too late to change my mind... how many of you are vaguely expecting to be there next week?

[Robert Maxton]

ah, what the hell. See y'all in an hour~

[Winston Yin (尹維晨)]

Kind of impossible to park here :grimacing:

[Alok Singh]

Who’s coming today

[Greg Shuflin]

I'm here

[Robert Maxton]

Who's coming tomorrow?

[Winston Yin (尹維晨)]

I can’t tomorrow :/

[Alok Singh]

I’m in Boston

[Greg Shuflin]

can't make it today

[Kyle Ellefsen]

Neither can I

[Winston Yin (尹維晨)]

Can't make it today...

[Robert Maxton]

Fortunately for you, it's tomorrow anyway :p
(I can't make it regardless, though)

[Chris Bailey]

I'll be attending tomorrow if anyone else is up for it.

[Chris Bailey]

Ok, probably will not be attending since there were no other takers.

[Alok Singh]

Sadly not today though I am meeting about lean 230-330

[Winston Yin (尹維晨)]

Rushing a Lean paper myself

[Alok Singh]

Anyone coming today?

[Robert Maxton]

I might, though I won't be leaving for a bit