chore: Ctxt API cleanup

[alexkeizer]

This PR cleans up some of the Ctxt API, in particular by structuring the existing lemmas more explicitly inside sections with header-comments, and by organizing variable declarations a bit better

[github-actions]

Alive Statistics: 90 / 93 (3 failed)

[github-actions]

bitwuzla proved and bv_decide failed theorem 3 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gexact_proof
bitwuzla proved and bv_decide failed theorem 14 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 19 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 51 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 53 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 3 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdistribute_proof
bitwuzla proved and bv_decide failed theorem 4 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdistribute_proof
bitwuzla proved and bv_decide failed theorem 12 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gnarrowhmath_proof
bitwuzla proved and bv_decide failed theorem 9 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gapinthsub_proof
bitwuzla proved and bv_decide failed theorem 1 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gapinthrem2_proof
bitwuzla proved and bv_decide failed theorem 1 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd4_proof
bitwuzla proved and bv_decide failed theorem 3 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd4_proof
bitwuzla proved and bv_decide failed theorem 0 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/g2008h02h23hMulSub_proof
bitwuzla proved and bv_decide failed theorem 0 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/g2010h11h23hDistributed_proof
bitwuzla proved and bv_decide failed theorem 4 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd_or_sub_proof
bitwuzla proved and bv_decide failed theorem 15 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gshifthshift_proof
bitwuzla proved and bv_decide failed theorem 7 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gtrunchinseltpoison_proof
bitwuzla proved and bv_decide failed theorem 14 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gshlhfactor_proof
bitwuzla proved and bv_decide failed theorem 21 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 22 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 23 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 24 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 6 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd2_proof
bitwuzla proved and bv_decide failed theorem 5 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/g2012h08h28hudiv_ashl_proof
bitwuzla proved and bv_decide failed theorem 13 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gsubhxorhcmp_proof
bv_decide solved 7925 theorems.
bitwuzla solved 7950 theorems.
bv_decide found 0 counterexamples.
bitwuzla found 0 counterexamples.
bv_decide only failed on 25 problems.
bitwuzla only failed on 0 problems.
both bitwuzla and bv_decide failed on 28 problems.
In total, bitwuzla saw 7978 problems.
In total, bv_decide saw 7978 problems.
ran rg 'LeanSAT provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'Bitwuzla provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'LeanSAT proved' | wc -l, this file found 7925, rg found 0, FAIL
ran rg 'Bitwuzla proved' | wc -l, this file found 7950, rg found 0, FAIL
The InstCombine benchmark contains 4520 theorems in total.
Saved dataframe at: /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/raw-data/InstCombine/instcombine_ceg_data.csv
all_files_solved_bitwuzla_times_stddev avg: 186.374325 | stddev: 0.0
all_files_solved_bv_decide_times_stddev avg: 224.745077 | stddev: 0.0
all_files_solved_bv_decide_rw_times_stddev avg: 105.744454 | stddev: 0.0
all_files_solved_bv_decide_bb_times_stddev avg: 0.097507 | stddev: 0.0
all_files_solved_bv_decide_sat_times_stddev avg: 76.971884 | stddev: 0.0
all_files_solved_bv_decide_lratt_times_stddev avg: 0.127438 | stddev: 0.0
all_files_solved_bv_decide_lratc_times_stddev avg: 27.766805 | stddev: 0.0
mean of percentage stddev/av: 0.0%
max of percentage stddev/av: 0.0%
Saved dataframe at: /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/raw-data/InstCombine/instcombine_solved_data.csv