Code

feat: implement MBA blast algorithm #977

Code

Merged

bollu merged 27 commits intomainopencompl/lean-mlir:mainfrom mba-blastopencompl/lean-mlir:mba-blastCopy head branch name to clipboardJan 27, 2025

+5,957-5,013

Commits

Commits on Jan 20, 2025

• chore: add fast impl

  bollu

  committed
  582c8e4

  Copy full SHA for 582c8e4

• chore: write correct thm statement

  bollu

  committed
  b36fee6

  Copy full SHA for b36fee6

Commits on Jan 21, 2025

• feat: structure MBA proof

  bollu

  committed
  5b65165

  Copy full SHA for 5b65165

• chore: Sid just realized that we don't have bitwise ops defined for Int. WTF!

  bollu

  committed
  243b1bb

  Copy full SHA for 243b1bb

• chore: checkpoint

  bollu

  committed
  56d4309

  Copy full SHA for 56d4309

• chore: checkpoint

  bollu

  committed
  9636af8

  Copy full SHA for 9636af8

Commits on Jan 22, 2025

• chore: write cast APIs

  bollu

  committed
  8bfe7eb

  Copy full SHA for 8bfe7eb

• feat: show that eqn obeys the recurrence

  Show description for d1c48cf
  bollu

  committed
  d1c48cf

  Copy full SHA for d1c48cf

• chore: add MBA proof of equality between denotefin and denote

  bollu

  committed
  c9960ed

  Copy full SHA for c9960ed

• chore: add hard proof

  bollu

  committed
  f34c312

  Copy full SHA for f34c312

• chore: finish core reflective lemma

  Show description for 7bb7e55
  bollu

  committed
  7bb7e55

  Copy full SHA for 7bb7e55

• chore: show the Decidable instance for MBA

  bollu

  committed
  270b7a3

  Copy full SHA for 270b7a3

Commits on Jan 27, 2025

• feat: write bitvec theorem about eq from sub

  bollu

  committed
  a31df83

  Copy full SHA for a31df83

• feat: build rewrite system to bring to reflection-normal-form

  Show description for 8cbfee9
  bollu

  committed
  8cbfee9

  Copy full SHA for 8cbfee9

• chore: add reassoc into simp-set

  bollu

  committed
  3c2c652

  Copy full SHA for 3c2c652

• chore: reflect, to expr, shebang

  bollu

  committed
  1248714

  Copy full SHA for 1248714

• chore: keep hacking on reflection

  bollu

  committed
  79ad8de

  Copy full SHA for 79ad8de

• feat: almost close the loop

  bollu

  committed
  248dcfe

  Copy full SHA for 248dcfe

• chore: bollu is confused, the reflect fails to be defeq? confusnig

  bollu

  committed
  f9192d6

  Copy full SHA for f9192d6

• chore: cleanup whitespace

  bollu

  committed
  0635572

  Copy full SHA for 0635572

• chore: add axiom for unproven bitvec lemmas about ring properties

  bollu

  committed
  c92cc8c

  Copy full SHA for c92cc8c

• feat: change dataset2 to use MBA

  bollu

  committed
  99a87dd

  Copy full SHA for 99a87dd

• chore: fixup reflection for mba to reflect xor correctly

  bollu

  committed
  dd8de58

  Copy full SHA for dd8de58

• chore: switch to MBA

  bollu

  committed
  0811edf

  Copy full SHA for 0811edf

• feat: add bv_mba to the set of tactics run by tac_bench

  bollu

  committed
  e519e7c

  Copy full SHA for e519e7c

• feat: merge main

  bollu

  committed
  de6290a

  Copy full SHA for de6290a

• feat: fixup TacticAuto

  bollu

  committed
  aca5692

  Copy full SHA for aca5692