Skip to content

Instantly share code, notes, and snippets.

@digama0

digama0/key-dist.rs

Last active May 12, 2022 14:55
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save digama0/78c5a2de9589d53b4667b9a75b3ca5f3 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save digama0/78c5a2de9589d53b4667b9a75b3ca5f3 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. digama0 revised this gist May 12, 2022. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion key-dist.rs
    View file
    Original file line number Diff line number Diff line change
    @@ -1,5 +1,5 @@
    // [dependencies]
    // metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife" }
    // metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife", tag = "v0.3.7" }
    // rand = "0.8"

    use metamath_knife::{statement::StatementAddress, verify::ProofBuilder, Database, StatementType};
  2. digama0 revised this gist May 12, 2022. 1 changed file with 22 additions and 23 deletions.
    45 changes: 22 additions & 23 deletions key-dist.rs
    View file
    Original file line number Diff line number Diff line change
    @@ -32,7 +32,7 @@ struct AccessSeq {
    }

    impl AccessSeq {
    fn score(&mut self, i: u32) -> u32 {
    fn push(&mut self, i: u32) {
    let mut best = u32::MAX;
    for &j in self.seq.iter().rev() {
    self.temp.insert(j);
    @@ -42,13 +42,12 @@ impl AccessSeq {
    best = best.min(self.temp.len() as u32 + j.abs_diff(i));
    }
    self.temp.clear();
    best
    }
    fn push(&mut self, i: u32) {
    let score = self.score(i) as f64;
    self.sum_score += score;
    self.sum_log_score += score.log2();
    self.sum_sqrt_score += score.sqrt();
    if best != u32::MAX {
    let score = best as f64;
    self.sum_score += score;
    self.sum_log_score += score.log2();
    self.sum_sqrt_score += score.sqrt();
    }
    self.seq.push(i)
    }
    }
    @@ -96,26 +95,26 @@ fn main() {
    // Results on https://github.com/metamath/set.mm/blob/3de3ae5/set.mm
    // number of theorems: 42879
    //
    // avg score: 4370145307 / 3075357 = 1421.0
    // avg lg(score): 10750033.8 / 3075357 = 3.4955 = lg(11.2788)
    // avg sqrt(score): 12705970.2 / 3075357 = 4.1315 = sqrt(17.0696)
    // avg score: 75178012 / 3075357 = 24.4
    // avg lg(score): 10750001.8 / 3075357) = 3.4955 = lg(11.2787)
    // avg sqrt(score): 12640434.2 / 3075357 = 4.1102 = sqrt(16.8940)
    //
    // shuffled 1:
    // avg score: 4452015191 / 3075357 = 1447.6
    // avg lg(score): 12857388.6 / 3075357 = 4.1808 = lg(18.1359)
    // avg sqrt(score): 17604771.6 / 3075357 = 5.7245 = sqrt(32.7695)
    // avg score: 157481709 / 3075357 = 51.2
    // avg lg(score): 12857460.5 / 3075357) = 4.1808 = lg(18.1362)
    // avg sqrt(score): 17549817.2 / 3075357 = 5.7066 = sqrt(32.5652)
    //
    // shuffled 2:
    // avg score: 4453096882 / 3075357 = 1448.0
    // avg lg(score): 12873701.1 / 3075357 = 4.1861 = lg(18.2027)
    // avg sqrt(score): 17659385.1 / 3075357 = 5.7422 = sqrt(32.9731)
    // avg score: 157220284 / 3075357 = 51.1
    // avg lg(score): 12861417.8 / 3075357) = 4.1821 = lg(18.1524)
    // avg sqrt(score): 17552661.4 / 3075357 = 5.7075 = sqrt(32.5758)
    //
    // completely random 1:
    // avg score: 4860210535 / 3075357 = 1580.4
    // avg lg(score): 22395391.0 / 3075357 = 7.2822 = lg(155.6550)
    // avg sqrt(score): 40220315.5 / 3075357 = 13.0783 = sqrt(171.0409)
    // avg score: 565223103 / 3075357 = 183.8
    // avg lg(score): 22394511.3 / 3075357) = 7.2819 = lg(155.6242)
    // avg sqrt(score): 40151474.7 / 3075357 = 13.0559 = sqrt(170.4559)
    //
    // completely random 2:
    // avg score: 4860319828 / 3075357 = 1580.4
    // avg lg(score): 22396702.0 / 3075357 = 7.2826 = lg(155.7010)
    // avg sqrt(score): 40224473.6 / 3075357 = 13.0796 = sqrt(171.0762)
    // avg score: 565104301 / 3075357 = 183.8
    // avg lg(score): 22394838.4 / 3075357) = 7.2820 = lg(155.6357)
    // avg sqrt(score): 40149999.7 / 3075357 = 13.0554 = sqrt(170.4433)
  3. digama0 revised this gist May 12, 2022. 1 changed file with 14 additions and 14 deletions.
    28 changes: 14 additions & 14 deletions key-dist.rs
    View file
    Original file line number Diff line number Diff line change
    @@ -87,35 +87,35 @@ fn main() {
    let avg_log_score = sum_log_score / n as f64;
    let avg_sqrt_score = sum_sqrt_score / n as f64;
    println!("avg score: {sum_score} / {n} = {avg_score:.1}");
    println!("2^(avg log(score)): \
    2^({sum_log_score:.1} / {n}) = 2^{avg_log_score:.4} = {:.4}", avg_log_score.exp2());
    println!("(avg sqrt(score))^2: \
    ({sum_sqrt_score:.1} / {n})^2 = {avg_sqrt_score:.4}^2 = {:.4}", avg_sqrt_score.powi(2));
    println!("avg lg(score): \
    {sum_log_score:.1} / {n}) = {avg_log_score:.4} = lg({:.4})", avg_log_score.exp2());
    println!("avg sqrt(score): \
    {sum_sqrt_score:.1} / {n} = {avg_sqrt_score:.4} = sqrt({:.4})", avg_sqrt_score.powi(2));
    }

    // Results on https://github.com/metamath/set.mm/blob/3de3ae5/set.mm
    // number of theorems: 42879
    //
    // avg score: 4370145307 / 3075357 = 1421.0
    // 2^(avg log(score)): 2^(10750033.8 / 3075357) = 2^3.4955 = 11.2788
    // (avg sqrt(score))^2: (12705970.2 / 3075357)^2 = 4.1315^2 = 17.0696
    // avg lg(score): 10750033.8 / 3075357 = 3.4955 = lg(11.2788)
    // avg sqrt(score): 12705970.2 / 3075357 = 4.1315 = sqrt(17.0696)
    //
    // shuffled 1:
    // avg score: 4452015191 / 3075357 = 1447.6
    // 2^(avg log(score)): 2^(12857388.6 / 3075357) = 2^4.1808 = 18.1359
    // (avg sqrt(score))^2: (17604771.6 / 3075357)^2 = 5.7245^2 = 32.7695
    // avg lg(score): 12857388.6 / 3075357 = 4.1808 = lg(18.1359)
    // avg sqrt(score): 17604771.6 / 3075357 = 5.7245 = sqrt(32.7695)
    //
    // shuffled 2:
    // avg score: 4453096882 / 3075357 = 1448.0
    // 2^(avg log(score)): 2^(12873701.1 / 3075357) = 2^4.1861 = 18.2027
    // (avg sqrt(score))^2: (17659385.1 / 3075357)^2 = 5.7422^2 = 32.9731
    // avg lg(score): 12873701.1 / 3075357 = 4.1861 = lg(18.2027)
    // avg sqrt(score): 17659385.1 / 3075357 = 5.7422 = sqrt(32.9731)
    //
    // completely random 1:
    // avg score: 4860210535 / 3075357 = 1580.4
    // 2^(avg log(score)): 2^(22395391.0 / 3075357) = 2^7.2822 = 155.6550
    // (avg sqrt(score))^2: (40220315.5 / 3075357)^2 = 13.0783^2 = 171.0409
    // avg lg(score): 22395391.0 / 3075357 = 7.2822 = lg(155.6550)
    // avg sqrt(score): 40220315.5 / 3075357 = 13.0783 = sqrt(171.0409)
    //
    // completely random 2:
    // avg score: 4860319828 / 3075357 = 1580.4
    // 2^(avg log(score)): 2^(22396702.0 / 3075357) = 2^7.2826 = 155.7010
    // (avg sqrt(score))^2: (40224473.6 / 3075357)^2 = 13.0796^2 = 171.0762
    // avg lg(score): 22396702.0 / 3075357 = 7.2826 = lg(155.7010)
    // avg sqrt(score): 40224473.6 / 3075357 = 13.0796 = sqrt(171.0762)
  4. digama0 revised this gist May 12, 2022. 1 changed file with 0 additions and 3 deletions.
    3 changes: 0 additions & 3 deletions key-dist.rs
    View file
    Original file line number Diff line number Diff line change
    @@ -9,9 +9,6 @@ use std::ops::Range;

    struct Pass<'a>(&'a HashMap<StatementAddress, u32>, &'a mut AccessSeq);

    /// The "null" proof builder, which creates no extra data. This
    /// is used for one-shot verification, where no extra data beyond the stack
    /// information is needed.
    impl ProofBuilder for Pass<'_> {
    type Item = ();
    type Accum = ();
  5. digama0 revised this gist May 12, 2022. 1 changed file with 40 additions and 18 deletions.
    58 changes: 40 additions & 18 deletions key-dist.rs
    View file
    Original file line number Diff line number Diff line change
    @@ -1,12 +1,11 @@
    // [dependencies]
    // metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife" }

    use std::{
    collections::{HashMap, HashSet},
    ops::Range,
    };
    // rand = "0.8"

    use metamath_knife::{statement::StatementAddress, verify::ProofBuilder, Database, StatementType};
    use rand::Rng;
    use std::collections::{hash_map::RandomState, HashMap, HashSet};
    use std::ops::Range;

    struct Pass<'a>(&'a HashMap<StatementAddress, u32>, &'a mut AccessSeq);

    @@ -80,23 +79,46 @@ fn main() {
    db.verify_one(&mut Pass(&map, &mut acc), stmt).unwrap();
    }
    }
    // replace the above for loop with this for a comparable completely random access sequence
    // let mut rand = rand::thread_rng();
    // for _ in 0..3075357 {
    // acc.push(rand.gen_range(0..map.len() as u32));
    // }
    let n = acc.seq.len();
    println!("avg score: {} / {n} = {:.1}", acc.sum_score, acc.sum_score / n as f64);
    println!("2^(avg lg(score)): 2^({:.1} / {n}) = {:.4}", acc.sum_log_score, (acc.sum_log_score / n as f64).exp2());
    println!("(avg sqrt(score))^2: ({:.1} / {n})^2 = {:.4}", acc.sum_sqrt_score, (acc.sum_sqrt_score / n as f64).powi(2));
    let AccessSeq { sum_score, sum_log_score, sum_sqrt_score, .. } = acc;
    let avg_score = sum_score / n as f64;
    let avg_log_score = sum_log_score / n as f64;
    let avg_sqrt_score = sum_sqrt_score / n as f64;
    println!("avg score: {sum_score} / {n} = {avg_score:.1}");
    println!("2^(avg log(score)): \
    2^({sum_log_score:.1} / {n}) = 2^{avg_log_score:.4} = {:.4}", avg_log_score.exp2());
    println!("(avg sqrt(score))^2: \
    ({sum_sqrt_score:.1} / {n})^2 = {avg_sqrt_score:.4}^2 = {:.4}", avg_sqrt_score.powi(2));
    }

    // Results on https://github.com/metamath/set.mm/blob/3de3ae5/set.mm
    // avg score: 4370145307 / 3075357 = 1421.0
    // 2^(avg lg(score)): 2^(10750033.8 / 3075357) = 11.2788
    // (avg sqrt(score))^2: (12705970.2 / 3075357)^2 = 17.0696
    // number of theorems: 42879
    //
    // avg score: 4370145307 / 3075357 = 1421.0
    // 2^(avg log(score)): 2^(10750033.8 / 3075357) = 2^3.4955 = 11.2788
    // (avg sqrt(score))^2: (12705970.2 / 3075357)^2 = 4.1315^2 = 17.0696
    //
    // shuffled 1:
    // avg score: 4451448463 / 3075357 = 1447.5
    // 2^(avg lg(score)): 2^(12843664.9 / 3075357) = 18.0799
    // (avg sqrt(score))^2: (17568628.9 / 3075357)^2 = 32.6351
    //
    // avg score: 4452015191 / 3075357 = 1447.6
    // 2^(avg log(score)): 2^(12857388.6 / 3075357) = 2^4.1808 = 18.1359
    // (avg sqrt(score))^2: (17604771.6 / 3075357)^2 = 5.7245^2 = 32.7695
    //
    // shuffled 2:
    // avg score: 4452744233 / 3075357 = 1447.9
    // 2^(avg lg(score)): 2^(12866794.4 / 3075357) = 18.1744
    // (avg sqrt(score))^2: (17636774.6 / 3075357)^2 = 32.8887
    // avg score: 4453096882 / 3075357 = 1448.0
    // 2^(avg log(score)): 2^(12873701.1 / 3075357) = 2^4.1861 = 18.2027
    // (avg sqrt(score))^2: (17659385.1 / 3075357)^2 = 5.7422^2 = 32.9731
    //
    // completely random 1:
    // avg score: 4860210535 / 3075357 = 1580.4
    // 2^(avg log(score)): 2^(22395391.0 / 3075357) = 2^7.2822 = 155.6550
    // (avg sqrt(score))^2: (40220315.5 / 3075357)^2 = 13.0783^2 = 171.0409
    //
    // completely random 2:
    // avg score: 4860319828 / 3075357 = 1580.4
    // 2^(avg log(score)): 2^(22396702.0 / 3075357) = 2^7.2826 = 155.7010
    // (avg sqrt(score))^2: (40224473.6 / 3075357)^2 = 13.0796^2 = 171.0762
  6. digama0 revised this gist May 12, 2022. 1 changed file with 22 additions and 5 deletions.
    27 changes: 22 additions & 5 deletions key-dist.rs
    View file
    Original file line number Diff line number Diff line change
    @@ -69,17 +69,34 @@ fn main() {
    .enumerate()
    {
    map.insert(stmt.address(), i as u32);
    }
    // uncomment to shuffle
    // for (k, (_, v)) in map.iter_mut().enumerate() {
    // *v = k as u32;
    // }
    let mut acc = AccessSeq::default();
    for stmt in db.statements().filter(|stmt| stmt.is_assertion()) {
    if stmt.statement_type() == StatementType::Provable {
    db.verify_one(&mut Pass(&map, &mut acc), stmt).unwrap();
    }
    }
    let n = acc.seq.len();
    println!("avg score: {} / {} = {:.1}", acc.sum_score, n, acc.sum_score / n as f64);
    println!("avg log(score): {:.1} / {} = {:.4}", acc.sum_log_score, n, acc.sum_log_score / n as f64);
    println!("avg sqrt(score): {:.1} / {} = {:.4}", acc.sum_sqrt_score, n, acc.sum_sqrt_score / n as f64);
    println!("avg score: {} / {n} = {:.1}", acc.sum_score, acc.sum_score / n as f64);
    println!("2^(avg lg(score)): 2^({:.1} / {n}) = {:.4}", acc.sum_log_score, (acc.sum_log_score / n as f64).exp2());
    println!("(avg sqrt(score))^2: ({:.1} / {n})^2 = {:.4}", acc.sum_sqrt_score, (acc.sum_sqrt_score / n as f64).powi(2));
    }

    // Results on https://github.com/metamath/set.mm/blob/3de3ae5/set.mm
    // avg score: 4370145307 / 3075357 = 1421.0
    // avg log(score): 10750033.8 / 3075357 = 3.4955
    // avg sqrt(score): 12705970.2 / 3075357 = 4.1315
    // 2^(avg lg(score)): 2^(10750033.8 / 3075357) = 11.2788
    // (avg sqrt(score))^2: (12705970.2 / 3075357)^2 = 17.0696
    //
    // shuffled 1:
    // avg score: 4451448463 / 3075357 = 1447.5
    // 2^(avg lg(score)): 2^(12843664.9 / 3075357) = 18.0799
    // (avg sqrt(score))^2: (17568628.9 / 3075357)^2 = 32.6351
    //
    // shuffled 2:
    // avg score: 4452744233 / 3075357 = 1447.9
    // 2^(avg lg(score)): 2^(12866794.4 / 3075357) = 18.1744
    // (avg sqrt(score))^2: (17636774.6 / 3075357)^2 = 32.8887
  7. digama0 revised this gist May 12, 2022. 1 changed file with 3 additions and 18 deletions.
    21 changes: 3 additions & 18 deletions key-dist.rs
    View file
    Original file line number Diff line number Diff line change
    @@ -74,24 +74,9 @@ fn main() {
    }
    }
    let n = acc.seq.len();
    println!(
    "avg score: {} / {} = {:.1}",
    acc.sum_score,
    n,
    acc.sum_score / n as f64
    );
    println!(
    "avg log(score): {:.1} / {} = {:.4}",
    acc.sum_log_score,
    n,
    acc.sum_log_score / n as f64
    );
    println!(
    "avg sqrt(score): {:.1} / {} = {:.4}",
    acc.sum_sqrt_score,
    n,
    acc.sum_sqrt_score / n as f64
    );
    println!("avg score: {} / {} = {:.1}", acc.sum_score, n, acc.sum_score / n as f64);
    println!("avg log(score): {:.1} / {} = {:.4}", acc.sum_log_score, n, acc.sum_log_score / n as f64);
    println!("avg sqrt(score): {:.1} / {} = {:.4}", acc.sum_sqrt_score, n, acc.sum_sqrt_score / n as f64);
    }

    // Results on https://github.com/metamath/set.mm/blob/3de3ae5/set.mm
  8. digama0 revised this gist May 12, 2022. 1 changed file with 53 additions and 13 deletions.
    66 changes: 53 additions & 13 deletions key-dist.rs
    View file
    Original file line number Diff line number Diff line change
    @@ -1,4 +1,10 @@
    use std::{collections::{HashMap, HashSet}, ops::Range};
    // [dependencies]
    // metamath-knife = { git = "https://github.com/david-a-wheeler/metamath-knife" }

    use std::{
    collections::{HashMap, HashSet},
    ops::Range,
    };

    use metamath_knife::{statement::StatementAddress, verify::ProofBuilder, Database, StatementType};

    @@ -21,22 +27,33 @@ impl ProofBuilder for Pass<'_> {
    }

    #[derive(Default)]
    struct AccessSeq(Vec<u32>, HashSet<u32>, f64);
    struct AccessSeq {
    seq: Vec<u32>,
    temp: HashSet<u32>,
    sum_score: f64,
    sum_log_score: f64,
    sum_sqrt_score: f64,
    }

    impl AccessSeq {
    fn score(&mut self, i: u32)-> u32 {
    fn score(&mut self, i: u32) -> u32 {
    let mut best = u32::MAX;
    for &j in self.0.iter().rev() {
    self.1.insert(j);
    if self.1.len() as u32 > best { break }
    best = best.min(self.1.len() as u32 + j.abs_diff(i));
    for &j in self.seq.iter().rev() {
    self.temp.insert(j);
    if self.temp.len() as u32 > best {
    break;
    }
    best = best.min(self.temp.len() as u32 + j.abs_diff(i));
    }
    self.1.clear();
    self.temp.clear();
    best
    }
    fn push(&mut self, i: u32) {
    self.2 += (self.score(i) as f64).log2();
    self.0.push(i)
    let score = self.score(i) as f64;
    self.sum_score += score;
    self.sum_log_score += score.log2();
    self.sum_sqrt_score += score.sqrt();
    self.seq.push(i)
    }
    }

    @@ -45,16 +62,39 @@ fn main() {
    db.parse("../mm/set.mm".into(), vec![]);
    db.scope_pass();
    let mut map = HashMap::new();
    let mut access = AccessSeq::default();
    let mut acc = AccessSeq::default();
    for (i, stmt) in db
    .statements()
    .filter(|stmt| stmt.is_assertion())
    .enumerate()
    {
    map.insert(stmt.address(), i as u32);
    if stmt.statement_type() == StatementType::Provable {
    db.verify_one(&mut Pass(&map, &mut access), stmt).unwrap();
    db.verify_one(&mut Pass(&map, &mut acc), stmt).unwrap();
    }
    }
    println!("{}", access.2 / access.0.len() as f64);
    let n = acc.seq.len();
    println!(
    "avg score: {} / {} = {:.1}",
    acc.sum_score,
    n,
    acc.sum_score / n as f64
    );
    println!(
    "avg log(score): {:.1} / {} = {:.4}",
    acc.sum_log_score,
    n,
    acc.sum_log_score / n as f64
    );
    println!(
    "avg sqrt(score): {:.1} / {} = {:.4}",
    acc.sum_sqrt_score,
    n,
    acc.sum_sqrt_score / n as f64
    );
    }

    // Results on https://github.com/metamath/set.mm/blob/3de3ae5/set.mm
    // avg score: 4370145307 / 3075357 = 1421.0
    // avg log(score): 10750033.8 / 3075357 = 3.4955
    // avg sqrt(score): 12705970.2 / 3075357 = 4.1315
  9. digama0 created this gist May 12, 2022.
    60 changes: 60 additions & 0 deletions key-dist.rs
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,60 @@
    use std::{collections::{HashMap, HashSet}, ops::Range};

    use metamath_knife::{statement::StatementAddress, verify::ProofBuilder, Database, StatementType};

    struct Pass<'a>(&'a HashMap<StatementAddress, u32>, &'a mut AccessSeq);

    /// The "null" proof builder, which creates no extra data. This
    /// is used for one-shot verification, where no extra data beyond the stack
    /// information is needed.
    impl ProofBuilder for Pass<'_> {
    type Item = ();
    type Accum = ();

    fn push(&mut self, _: &mut (), _: ()) {}

    fn build(&mut self, addr: StatementAddress, _: (), _: &[u8], _: Range<usize>) {
    if let Some(&i) = self.0.get(&addr) {
    self.1.push(i)
    }
    }
    }

    #[derive(Default)]
    struct AccessSeq(Vec<u32>, HashSet<u32>, f64);

    impl AccessSeq {
    fn score(&mut self, i: u32)-> u32 {
    let mut best = u32::MAX;
    for &j in self.0.iter().rev() {
    self.1.insert(j);
    if self.1.len() as u32 > best { break }
    best = best.min(self.1.len() as u32 + j.abs_diff(i));
    }
    self.1.clear();
    best
    }
    fn push(&mut self, i: u32) {
    self.2 += (self.score(i) as f64).log2();
    self.0.push(i)
    }
    }

    fn main() {
    let mut db = Database::default();
    db.parse("../mm/set.mm".into(), vec![]);
    db.scope_pass();
    let mut map = HashMap::new();
    let mut access = AccessSeq::default();
    for (i, stmt) in db
    .statements()
    .filter(|stmt| stmt.is_assertion())
    .enumerate()
    {
    map.insert(stmt.address(), i as u32);
    if stmt.statement_type() == StatementType::Provable {
    db.verify_one(&mut Pass(&map, &mut access), stmt).unwrap();
    }
    }
    println!("{}", access.2 / access.0.len() as f64);
    }