Arena allocation for ITPs

Stream: Program verification

[Chris B]

Hi,
I've been working on a rewrite of the Rust version of Lean's kernel for a while; it uses arenas to manage the type checker items (instead of reference counting). All of the ITPs I'm familiar with are either GC'd or are Lean, so I thought this would be an interesting data point for the CS people here who might find themselves writing software in the same vein. I rewrote it this way just to see whether some new insights about how the kernel is laid out could yield a performance benefit, and it ended up being ~3-4x faster than the other checkers while having a smaller memory footprint. The arena API is completely type safe and uses phantom lifetimes to achieve memory safety (arenas can't be dropped if there are outstanding pointers into their contents, so pointers can't deref to bad data).
There's some more information/stats in the readme. https://github.com/ammkrn/nanoda_lib

[Simon Hudon]

Nice! When you say "better than other checkers", does that include the C++ implementation?

[Chris B]

Hey I only said 'faster' lol. The one that was in the lean3 repo is the only C++ I know of, but yeah those numbers are the same (3-4x), maybe a little bit more depending on how big the export file is. leanchecker, trepplein, and the RC version of the Rust one were all really close in terms of speed. Leanchecker had some issues with memory consumption spikes IIRC. The last time I asked about it lean4 didn't have a free-standing checker and there isn't an export format.

[Simon Hudon]

I'm surprised that the speed up would be so consistent across the different checkers. I thought the Haskell checker was much much slower than the C++ one

[Chris B]

Oh yeah the Haskell one is way, way slower than the other ones. Do you know why that is?

[Chris B]

I assumed it was a Haskell thing about like unoptimized collections in the prelude or something.

[Simon Hudon]

I haven't looked closely at it, I can't say

[Simon Hudon]

Does the arena guarantee some sort uniqueness property for the term nodes it stores?

[Chris B]

Yeah, when you go to insert an item it checks whether it already exists in the collection. The underlying structure is from a rust library called indexmap that's like a hashmap with indices that preserve insertion order.

[Chris B]

The actual process is slightly more complicated since you have to check the persistent collection first then the temporary one.

[Simon Hudon]

Cool. i like the analysis you make about temporary garbage. I wonder how it will apply to Lean 4 since Lean 4 uses destructive updates whenever possible instead of allocating more memory

[Mario Carneiro]

Ah, this will be useful for isabelle proof generation. I wasn't sure how well this strategy would perform so it's good to hear the numbers bear it out

[Chris B]

Yeah neither was I lol. The one thing I'm worried about is someone managing to line up just the right tactic proof that produces like 100gb worth of garbage, but we'll see. The largest one a few months ago was 1.6 million nodes, now it's over 10 million.

[Chris B]

Simon Hudon said:

I wonder how it will apply to Lean 4 since Lean 4 uses destructive updates whenever possible instead of allocating more memory

Yeah I'm interested to see this as well. If you roll your own RC stuff like they did you can avoid a lot of the small to medium sized performance hang-ups I ran into in the last version, and I know they've done a lot of thinking about how to make the most of their system.

[Mario Carneiro]

It might be good to collect statistics on what the largest proofs are from this point of view, because they could just be bad proofs

[Mario Carneiro]

That growth in proof size sounds more like a regression than an improvement

[Simon Hudon]

Large proofs are clearly a problem but the other thing to consider is non-trivial kernel computations. The proof size could be moderate but you could be running ackerman's function for instance. That would produce a lot of trash that reference counting wouldn't keep around but arenas would

[Chris B]

I made another thread earlier today in general to try and get some insight into that; the biggest one by far is polynomial.monic.next_coeff_mul, and the runner up is finset.sum_range_sub_of_monotone

[Mario Carneiro]

one man's trash is another man's treasure :P

[Chris B]

Yeah, I would like to go back and address that more thoroughly in the future. I had an idea to do it where the arenas were telescoped out, so each arena had an Option<&mut Arena> to a parent whose lifetime was longer, so when you finish one computation the thing's scope ends and you insert the result into the parent, effectively dropping all of the garbage. The problem is that searching for duplicates now forces you to check as many arenas as you have alive instead of just the two.

[Chris B]

The RC solution is much more general, so props to Lean.

[Kevin Buzzard]

I'm pretty sure there would be people who would be interested in seeing a list of the 100 biggest proofs

[Mario Carneiro]

it's another way to play the -T50000 game

[Kevin Buzzard]

It's a better way perhaps, because when I've played that game some lemma times out and then lots of other things break and you basically have to deal with the first problem.

[Chris B]

Kevin Buzzard said:

I'm pretty sure there would be people who would be interested in seeing a list of the 100 biggest proofs

Mathlib high scores :
https://gist.github.com/ammkrn/dab311e0d2d27b3bcd15ec6c4a2b019d

[Chris B]

I'll add a command line flag for it or something.

[Mario Carneiro]

oh wow that escalated quickly

[Mario Carneiro]

where is src#polynomial.monic.next_coeff_mul

[Mario Carneiro]

hm, perhaps it is the omega calls at the end?

[Chris B]

omega does seem to be a common thread between no.1 and no.2

[Mario Carneiro]

How does the length of this version of the proof stack up:

lemma next_coeff_mul_omega_1 (dp : ℕ) (hp0 : ¬dp = 0) : dp ≠ dp - 1 := by omega

lemma next_coeff_mul_omega_2 (x : ℕ × ℕ) (dp dq : ℕ)
  (hp0 : ¬dp = 0) (hq0 : ¬dq = 0) (hx : x.fst + x.snd = dp + dq - 1)
  (h : x.fst ≤ dp) (hx1 : x.fst = dp - 1) : x.snd = dq := by omega

lemma next_coeff_mul_omega_3 (x : ℕ × ℕ) (dp dq : ℕ)
  (hp0 : ¬dp = 0) (hq0 : ¬dq = 0) (hx : x.fst + x.snd = dp + dq - 1)
  (h : x.fst ≤ dp) (this : x.fst ≠ dp - 1) (hx1 : x.fst = dp) : x.snd = dq - 1 := by omega

lemma next_coeff_mul_omega_4 (x : ℕ × ℕ) (dp dq : ℕ)
  (hp0 : ¬dp = 0) (hq0 : ¬dq = 0) (hx : x.fst + x.snd = dp + dq - 1)
  (hx1 : ¬(x = (dp, dq - 1) ∨ x = (dp - 1, dq)))
  (h : x.fst ≤ dp) (this : x.fst ≠ dp - 1) (this_1 : x.fst ≠ dp) : dq < x.snd := by omega

lemma next_coeff_mul {p q : polynomial R} (hp : monic p) (hq : monic q) :
next_coeff (p * q) = next_coeff p + next_coeff q :=
begin
  classical,
  by_cases h : nontrivial R, swap,
  { rw nontrivial_iff at h, push_neg at h, apply h, },
  haveI := h, clear h,
  have := monic.nat_degree_mul hp hq,
  dsimp only [next_coeff], rw this,
  simp only [hp, hq, degree_eq_zero_iff_eq_one, add_eq_zero_iff], clear this,
  split_ifs; try { tauto <|> simp [h_1, h_2] },
  rename h_1 hp0, rename h_2 hq0, clear h,
  rw ← degree_eq_zero_iff_eq_one at hp0 hq0, assumption',
  -- we've reduced to the case where the degrees dp and dq are nonzero
  set dp := p.nat_degree, set dq := q.nat_degree,
  rw coeff_mul,
  have : {(dp, dq - 1), (dp - 1, dq)} ⊆ nat.antidiagonal (dp + dq - 1),
  { rw insert_subset, split,
    work_on_goal 0 { rw [nat.mem_antidiagonal, nat.add_sub_assoc] },
    work_on_goal 1 { simp only [singleton_subset_iff, nat.mem_antidiagonal],
      apply nat.sub_add_eq_add_sub },
    all_goals { apply nat.succ_le_of_lt, apply nat.pos_of_ne_zero, assumption } },
  rw ← sum_subset this,
  { rw [sum_insert, sum_singleton], iterate 2 { rw coeff_nat_degree }, ring, assumption',
    suffices : dp ≠ dp - 1, { rw mem_singleton, simp [this] }, apply next_coeff_mul_omega_1; assumption }, clear this,
  intros x hx hx1,
  simp only [nat.mem_antidiagonal] at hx, simp only [mem_insert, mem_singleton] at hx1,
  suffices : p.coeff x.fst = 0 ∨ q.coeff x.snd = 0, cases this; simp [this],
  suffices : dp < x.fst ∨ dq < x.snd, cases this,
  { left,  apply coeff_eq_zero_of_nat_degree_lt, assumption },
  { right, apply coeff_eq_zero_of_nat_degree_lt, assumption },
  by_cases h : dp < x.fst, { left, exact h }, push_neg at h, right,
  have : x.fst ≠ dp - 1, { contrapose! hx1, right, ext, assumption, dsimp only, apply next_coeff_mul_omega_2; assumption },
  have : x.fst ≠ dp,     { contrapose! hx1, left,  ext, assumption, dsimp only, apply next_coeff_mul_omega_3; assumption },
  apply next_coeff_mul_omega_4; assumption
end

[Mario Carneiro]

(all I did was extract_goal on all of the omega calls)

[Chris B]

The new leaders are (1, 2, and 3) are the factored out omegas.

garbage terms
6335962 : polynomial.monic.next_coeff_mul_omega_3
2922613 : polynomial.monic.next_coeff_mul_omega_4
1885162 : polynomial.monic.next_coeff_mul_omega_2
1090313 : composition_as_set_equiv._proof_5


time (milliseconds)
3998 : polynomial.monic.next_coeff_mul_omega_3
1783 : polynomial.monic.next_coeff_mul_omega_4
1091 : polynomial.monic.next_coeff_mul_omega_2
680 : composition_as_set_equiv._proof_5

[Kevin Buzzard]

import tactic

lemma next_coeff_mul_omega_3 (x : ℕ × ℕ) (dp dq : ℕ)
  (hp0 : ¬dp = 0) (hq0 : ¬dq = 0) (hx : x.fst + x.snd = dp + dq - 1)
  (h : x.fst ≤ dp) (this : x.fst ≠ dp - 1) (hx1 : x.fst = dp) : x.snd = dq - 1 :=
begin
  cases dq, contradiction,
  subst hx1,
  rwa [nat.succ_eq_add_one, ←add_assoc, nat.add_sub_cancel, add_right_inj] at hx,
end

[Mario Carneiro]

oh, are we playing this game?

lemma next_coeff_mul_omega_3 (x : ℕ × ℕ) (dp dq : ℕ)
  (hp0 : ¬dp = 0) (hq0 : ¬dq = 0) (hx : x.fst + x.snd = dp + dq - 1)
  (h : x.fst ≤ dp) (this : x.fst ≠ dp - 1) (hx1 : x.fst = dp) : x.snd = dq - 1 :=
by rwa [hx1, nat.add_sub_assoc (nat.pos_of_ne_zero hq0), add_right_inj] at hx

[Kevin Buzzard]

I was just trying to make mathlib compile quicker!

[Kevin Buzzard]

How many times has CI compiled that four second proof?

[Kevin Buzzard]

More seriously, do we just have a rubbish omega, or is this the actual nature of omega -- I've heard that the algorithm is super-slow.

[Mario Carneiro]

probably a bit of both

[Mario Carneiro]

I looked at the proof terms and they are seriously bizarre

[Mario Carneiro]

                                           (nat.preform.le ((nat.preterm.var 1 6).add (nat.preterm.cst 1))
                                              (nat.preterm.var 1 2))))))))).and
                        ((nat.preform.eq (nat.preterm.var 1 1) ((nat.preterm.cst 1).add (nat.preterm.var 1 4))).or
                           ((nat.preform.le (nat.preterm.var 1 1) (nat.preterm.cst 1)).and
                              (nat.preform.eq (nat.preterm.var 1 4) (nat.preterm.cst 0))))).and
                       ((nat.preform.eq ((nat.preterm.var 1 1).add (nat.preterm.var 1 3))
                           ((nat.preterm.cst 1).add (nat.preterm.var 1 5))).or
                          ((nat.preform.le ((nat.preterm.var 1 1).add (nat.preterm.var 1 3)) (nat.preterm.cst 1)).and
                             (nat.preform.eq (nat.preterm.var 1 5) (nat.preterm.cst 0))))).and
                      ((nat.preform.eq (nat.preterm.var 1 3) ((nat.preterm.cst 1).add (nat.preterm.var 1 6))).or
                         ((nat.preform.le (nat.preterm.var 1 3) (nat.preterm.cst 1)).and
                            (nat.preform.eq (nat.preterm.var 1 6) (nat.preterm.cst 0)))))
                   ⟨⟨⟨⟨⟨trivial, trivial⟩,
                       ⟨trivial,
                        ⟨trivial,
                         ⟨trivial,
                          ⟨⟨trivial, trivial⟩,
                           ⟨⟨trivial, trivial⟩, ⟨trivial, trivial⟩⟩⟩⟩⟩⟩⟩,
                      ⟨trivial, ⟨trivial, trivial⟩⟩⟩,
                     ⟨trivial, ⟨trivial, trivial⟩⟩⟩,
                    ⟨trivial, ⟨trivial, trivial⟩⟩⟩
                   ⟨⟨⟨⟨⟨⟨⟨trivial, trivial⟩, trivial⟩, ⟨⟨trivial, trivial⟩, trivial⟩⟩,
                       ⟨⟨trivial, trivial⟩,
                        ⟨⟨⟨trivial, trivial⟩, ⟨trivial, trivial⟩⟩,
                         ⟨⟨⟨trivial, trivial⟩, trivial⟩,
                          ⟨⟨⟨⟨trivial, trivial⟩, trivial⟩, ⟨⟨trivial, trivial⟩, trivial⟩⟩,
                           ⟨⟨⟨⟨trivial, trivial⟩, trivial⟩, ⟨⟨trivial, trivial⟩, trivial⟩⟩,
                            ⟨⟨⟨trivial, trivial⟩, trivial⟩,
                             ⟨⟨trivial, trivial⟩, trivial⟩⟩⟩⟩⟩⟩⟩⟩,
                      ⟨⟨trivial, ⟨trivial, trivial⟩⟩,
                       ⟨⟨trivial, trivial⟩, ⟨trivial, trivial⟩⟩⟩⟩,
                     ⟨⟨⟨trivial, trivial⟩, ⟨trivial, trivial⟩⟩,
                      ⟨⟨⟨trivial, trivial⟩, trivial⟩, ⟨trivial, trivial⟩⟩⟩⟩,
                    ⟨⟨trivial, ⟨trivial, trivial⟩⟩, ⟨⟨trivial, trivial⟩, ⟨trivial, trivial⟩⟩⟩⟩
                   (clauses.unsat_cons
                      ([(int.of_nat 0, [-[1+ 0], int.of_nat 1]), (int.of_nat 0,
                          [-[1+ 0], int.of_nat 0, -[1+ 0], int.of_nat 0, int.of_nat 0, int.of_nat 1]), (int.of_nat 1,
                          [int.of_nat 0, -[1+ 0], int.of_nat 0, int.of_nat 0, int.of_nat 1]), (int.of_nat 1,
                          [int.of_nat 0, -[1+ 0], int.of_nat 0, -[1+ 0], int.of_nat 0, int.of_nat 1]), (int.of_nat 1,
                          [int.of_nat 0, int.of_nat 0, int.of_nat 0, -[1+ 0], int.of_nat 0, int.of_nat 0, int.of_nat
                              1])],
                       [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat
                              1]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat
                              0, int.of_nat 1]), (-[1+ 0],
                          [-[1+ 0], int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                          [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                          [int.of_nat 0, int.of_nat 0, int.of_nat 0, -[1+ 0]]), (-[1+ 0],
                          [int.of_nat 0, -[1+ 0]]), (-[1+ 0],
                          [int.of_nat 0, int.of_nat 0, -[1+ 0], int.of_nat 0, int.of_nat 0, int.of_nat 0, int.of_nat
                              1])])
                      […, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, …, ([…, …, …, …, (int.of_nat
                              1,
                            […, …, …, …, …, int.of_nat 0, int.of_nat 1])],
                         …), ([(int.of_nat 0, [-[1+ 0], int.of_nat 1]), (int.of_nat 0,
                            [-[1+ 0], int.of_nat 0, -[1+ 0], int.of_nat 0, int.of_nat 0, int.of_nat 1]), (int.of_nat 1,
                            [int.of_nat 0, -[1+ 0], int.of_nat 0, int.of_nat 0, int.of_nat 1]), (int.of_nat 1,
                            [int.of_nat 0, -[1+ 0], int.of_nat 0, -[1+ 0], int.of_nat 0, int.of_nat 1]), (int.of_nat 0,

[Mario Carneiro]

I think we will have to do something about omega soon. It has no maintainer and the author doesn't seem interested in maintenance

[Simon Hudon]

I think Seul really wanted to have part of it running in the kernel

[Mario Carneiro]

I'm guessing that's what the array of trivialities are doing

[Rob Lewis]

Mario Carneiro said:

I think we will have to do something about omega soon. It has no maintainer and the author doesn't seem interested in maintenance

I'm certain we'll have to do something about omega before the Lean 4 transition, because I can't imagine the current one getting ported.

[Kevin Buzzard]

I'm assuming that 213ms : real.pi_lt_31416 is implied by 346ms : real.pi_lt_3141593?

[Chris Wong]

How much work would it take to clean up omega? That sounds like something I can help out with, but I don't want to lick the cookie if I can't eat it.

[Rob Lewis]

omega is 3k lines of pretty intricate code with limited documentation. It's a good proof of concept for reflexive tactics in Lean but I'm not sure it's the right approach overall. Fixing some of the open bugs would be nice, but for serious improvements it might be easier to start from scratch.

[Rob Lewis]

For comparison, cloc says linarith is 711 code lines and 752 comment lines, omega is 2342 code and 367 comment.

[Rob Lewis]

A rewrite should probably take some inspiration from the lra/lia interaction in Coq and share some code with linarith.