From 5ac1e27035f4b935ff6ee9856f911a55bb1c67b3 Mon Sep 17 00:00:00 2001
From: Andrew Dirksen <andrew@dirksen.com>
Date: Thu, 22 Apr 2021 11:41:32 -0700
Subject: [PATCH 1/5] add benches for prove() and infer()

---
 benches/.gitignore     |   5 ++
 benches/Cargo.toml     |   8 +++
 benches/rust-toolchain |   1 +
 benches/src/lib.rs     | 123 +++++++++++++++++++++++++++++++++++++++++
 justfile               |   6 ++
 5 files changed, 143 insertions(+)
 create mode 100644 benches/.gitignore
 create mode 100644 benches/Cargo.toml
 create mode 100644 benches/rust-toolchain
 create mode 100644 benches/src/lib.rs

diff --git a/benches/.gitignore b/benches/.gitignore
new file mode 100644
index 0000000..0363452
--- /dev/null
+++ b/benches/.gitignore
@@ -0,0 +1,5 @@
+/target
+/pkg
+/wasm-pack.log
+/tmp
+/Cargo.lock
diff --git a/benches/Cargo.toml b/benches/Cargo.toml
new file mode 100644
index 0000000..343742c
--- /dev/null
+++ b/benches/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "benches"
+version = "0.1.0"
+authors = ["Andrew Dirksen <andrew@dirksen.com>"]
+edition = "2018"
+
+[dependencies]
+rify = { path = ".." }
diff --git a/benches/rust-toolchain b/benches/rust-toolchain
new file mode 100644
index 0000000..bf867e0
--- /dev/null
+++ b/benches/rust-toolchain
@@ -0,0 +1 @@
+nightly
diff --git a/benches/src/lib.rs b/benches/src/lib.rs
new file mode 100644
index 0000000..c5fd2df
--- /dev/null
+++ b/benches/src/lib.rs
@@ -0,0 +1,123 @@
+#![cfg(test)]
+#![feature(test)]
+
+extern crate test;
+
+use core::fmt::Debug;
+use rify::Entity::{Bound as B, Unbound as U};
+use rify::*;
+use test::Bencher;
+
+const DG: &str = "default_graph";
+
+mod ancestry {
+    use super::*;
+    const PARENT: &str = "parent";
+    const ANCESTOR: &str = "ancestor";
+
+    fn rules() -> Vec<rify::Rule<&'static str, &'static str>> {
+        decl_rules(&[
+            [
+                &[[U("a"), B(PARENT), U("b"), B(DG)]],
+                &[[U("a"), B(ANCESTOR), U("b"), B(DG)]],
+            ],
+            [
+                &[
+                    [U("a"), B(ANCESTOR), U("b"), B(DG)],
+                    [U("b"), B(ANCESTOR), U("c"), B(DG)],
+                ],
+                &[[U("a"), B(ANCESTOR), U("c"), B(DG)]],
+            ],
+        ])
+    }
+
+    // Contains intentional leak; don't use outside of tests.
+    fn facts() -> Vec<[&'static str; 4]> {
+        let nodes: Vec<&str> = (0..20)
+            .map(|n| Box::leak(format!("node_{}", n).into_boxed_str()) as &str)
+            .collect();
+        let facts: Vec<[&str; 4]> = nodes
+            .iter()
+            .zip(nodes.iter().cycle().skip(1))
+            .map(|(a, b)| [a, PARENT, b, DG])
+            .collect();
+        facts
+    }
+
+    #[bench]
+    fn infer_(b: &mut Bencher) {
+        let facts = facts();
+        let rules = rules();
+        b.iter(|| infer(&facts, &rules));
+    }
+
+    #[bench]
+    fn prove_(b: &mut Bencher) {
+        let facts = facts();
+        let rules = rules();
+        b.iter(|| prove(&facts, &[[PARENT, PARENT, PARENT, PARENT]], &rules));
+    }
+}
+
+mod recursion_minimal {
+    use super::*;
+
+    const RULES: &[[&[[rify::Entity<&str, &str>; 4]]; 2]] = &[
+        [
+            &[
+                [B("andrew"), B("claims"), U("c"), B(DG)],
+                [U("c"), B("subject"), U("s"), B(DG)],
+                [U("c"), B("property"), U("p"), B(DG)],
+                [U("c"), B("object"), U("o"), B(DG)],
+            ],
+            &[[U("s"), U("p"), U("o"), B(DG)]],
+        ],
+        [
+            &[
+                [U("person_a"), B("is"), B("awesome"), B(DG)],
+                [U("person_a"), B("friendswith"), U("person_b"), B(DG)],
+            ],
+            &[[U("person_b"), B("is"), B("awesome"), B(DG)]],
+        ],
+        [
+            &[[U("person_a"), B("friendswith"), U("person_b"), B(DG)]],
+            &[[U("person_b"), B("friendswith"), U("person_a"), B(DG)]],
+        ],
+    ];
+
+    const FACTS: &[[&str; 4]] = &[
+        ["soyoung", "friendswith", "nick", DG],
+        ["nick", "friendswith", "elina", DG],
+        ["elina", "friendswith", "sam", DG],
+        ["sam", "friendswith", "fausto", DG],
+        ["fausto", "friendswith", "lovesh", DG],
+        ["andrew", "claims", "_:claim1", DG],
+        ["_:claim1", "subject", "lovesh", DG],
+        ["_:claim1", "property", "is", DG],
+        ["_:claim1", "object", "awesome", DG],
+    ];
+
+    #[bench]
+    fn infer_(b: &mut Bencher) {
+        let rules = decl_rules(RULES);
+        b.iter(|| infer(FACTS, &rules));
+    }
+
+    #[bench]
+    fn prove_(b: &mut Bencher) {
+        let rules = decl_rules(RULES);
+        let composite_claims: &[[&str; 4]] = &[
+            ["soyoung", "is", "awesome", "default_graph"],
+            ["nick", "is", "awesome", "default_graph"],
+        ];
+        b.iter(|| prove(FACTS, composite_claims, &rules));
+    }
+}
+
+pub fn decl_rules<Unbound: Ord + Debug + Clone, Bound: Ord + Clone>(
+    rs: &[[&[[rify::Entity<Unbound, Bound>; 4]]; 2]],
+) -> Vec<rify::Rule<Unbound, Bound>> {
+    rs.iter()
+        .map(|[ifa, then]| rify::Rule::create(ifa.to_vec(), then.to_vec()).unwrap())
+        .collect()
+}
diff --git a/justfile b/justfile
index 301281a..80bb7e6 100644
--- a/justfile
+++ b/justfile
@@ -30,6 +30,7 @@ js-test:
 # remove dist and node_modules from js bindings tests
 clean:
   cargo clean
+  cd benches; cargo clean
   rm -r bindings/js_wasm/pkg || true
   just clean-js
 
@@ -37,3 +38,8 @@ clean:
 clean-js:
   rm -r bindings/js_wasm/binding_tests/dist || true
   rm -r bindings/js_wasm/binding_tests/node_modules || true
+
+bench:
+  #!/usr/bin/env bash
+  cd benches
+  cargo bench

From 7bf82a10568dfbf11458696463be8dd946e6cf17 Mon Sep 17 00:00:00 2001
From: Andrew Dirksen <andrew@dirksen.com>
Date: Thu, 22 Apr 2021 16:24:57 -0700
Subject: [PATCH 2/5] Optimize infer() and prove().

This implements differential rule applications as suggested in https://github.com/docknetwork/rify/issues/1

As a side effect of implementing that optimization I also reduced the cased where LowRule needed to be cloned within the hot path. The reduction in clones made a small difference but differential rule applications had the greated effect.

Before:
```
running 4 tests
test ancestry::infer_          ... bench:   2,339,370 ns/iter (+/- 36,027)
test ancestry::prove_          ... bench:   2,332,249 ns/iter (+/- 61,357)
test recursion_minimal::infer_ ... bench:      35,339 ns/iter (+/- 1,012)
test recursion_minimal::prove_ ... bench:      34,850 ns/iter (+/- 312)
```

After:
```
test ancestry::infer_          ... bench:   1,683,208 ns/iter (+/- 49,885)
test ancestry::prove_          ... bench:   1,792,665 ns/iter (+/- 22,206)
test recursion_minimal::infer_ ... bench:      17,601 ns/iter (+/- 457)
test recursion_minimal::prove_ ... bench:      23,608 ns/iter (+/- 677)
```

We see a ~24% improvment for the 20 node ancestry test case. The percentage improvement becomes larger as node count increases. The previous version was too slow to even include a benchmark with larger node count (I lost patience waiting.). The new version is fast enough to scale to larger node counts so I've added another couple larger benchmarks in this commit: `ancestry::infer_30` and `test ancestry::prove_30`
---
 benches/src/lib.rs | 24 +++++++++---
 src/infer.rs       | 70 ++++++++++++++++++++++------------
 src/prove.rs       | 95 ++++++++++++++++++++++++++++------------------
 src/reasoner.rs    | 91 +++++++++++++++++++++++++++++++++++++-------
 src/rule.rs        | 13 +++++++
 5 files changed, 215 insertions(+), 78 deletions(-)

diff --git a/benches/src/lib.rs b/benches/src/lib.rs
index c5fd2df..c5cef33 100644
--- a/benches/src/lib.rs
+++ b/benches/src/lib.rs
@@ -32,8 +32,8 @@ mod ancestry {
     }
 
     // Contains intentional leak; don't use outside of tests.
-    fn facts() -> Vec<[&'static str; 4]> {
-        let nodes: Vec<&str> = (0..20)
+    fn facts(numnodes: usize) -> Vec<[&'static str; 4]> {
+        let nodes: Vec<&str> = (0..numnodes)
             .map(|n| Box::leak(format!("node_{}", n).into_boxed_str()) as &str)
             .collect();
         let facts: Vec<[&str; 4]> = nodes
@@ -46,16 +46,30 @@ mod ancestry {
 
     #[bench]
     fn infer_(b: &mut Bencher) {
-        let facts = facts();
+        let facts = facts(20);
         let rules = rules();
         b.iter(|| infer(&facts, &rules));
     }
 
     #[bench]
     fn prove_(b: &mut Bencher) {
-        let facts = facts();
+        let facts = facts(20);
         let rules = rules();
-        b.iter(|| prove(&facts, &[[PARENT, PARENT, PARENT, PARENT]], &rules));
+        b.iter(|| prove(&facts, &[[PARENT, PARENT, PARENT, PARENT]], &rules).unwrap_err());
+    }
+
+    #[bench]
+    fn infer_30(b: &mut Bencher) {
+        let facts = facts(30);
+        let rules = rules();
+        b.iter(|| infer(&facts, &rules));
+    }
+
+    #[bench]
+    fn prove_30(b: &mut Bencher) {
+        let facts = facts(30);
+        let rules = rules();
+        b.iter(|| prove(&facts, &[[PARENT, PARENT, PARENT, PARENT]], &rules).unwrap_err());
     }
 }
 
diff --git a/src/infer.rs b/src/infer.rs
index a6ab38c..e4bc0ed 100644
--- a/src/infer.rs
+++ b/src/infer.rs
@@ -28,36 +28,58 @@ pub fn infer<Unbound: Ord + Clone, Bound: Ord + Clone>(
 /// A version of infer that operates on lowered input an returns output in lowered form.
 fn low_infer(premises: &[Quad], rules: &[LowRule]) -> Vec<Quad> {
     let mut rs = Reasoner::default();
-    for prem in premises {
-        rs.insert(prem.clone());
+
+    let mut to_add: BTreeSet<Quad> = premises.iter().cloned().collect();
+    let initial_len = to_add.len(); // number of premises after dedup
+    assert!(initial_len <= premises.len());
+
+    // apply_related is sufficient except for in the case of unconditional rules.
+    // in order to avoid calling apply() directly, rules with empty "if" clauses
+    // lists will get special treatment.
+    for rule in rules {
+        if rule.if_all.is_empty() {
+            for rule_part in &rule.then {
+                to_add.insert(rule_part.clone().local_to_global(&rule.inst).unwrap());
+            }
+        }
     }
-    let initial_len = rs.claims_ref().len(); // number of premises after dedup
-    debug_assert!(initial_len <= premises.len());
+    let mut rules: Vec<LowRule> = rules
+        .iter()
+        .filter(|r| !r.if_all.is_empty())
+        .cloned()
+        .collect();
 
+    // subsequent reasoning is done in a loop using apply_related
     loop {
-        let mut to_add = BTreeSet::<Quad>::new();
-        for rr in rules.iter() {
-            rs.apply(&mut rr.if_all.clone(), &mut rr.inst.clone(), &mut |inst| {
-                let ins = inst.as_ref();
-                for implied in &rr.then {
-                    let new_quad = [
-                        ins[&implied.s.0],
-                        ins[&implied.p.0],
-                        ins[&implied.o.0],
-                        ins[&implied.g.0],
-                    ]
-                    .into();
-                    if !rs.contains(&new_quad) {
-                        to_add.insert(new_quad);
-                    }
-                }
-            });
-        }
         if to_add.is_empty() {
             break;
         }
-        for new in to_add.into_iter() {
-            rs.insert(new);
+        let mut adding = BTreeSet::default();
+        core::mem::swap(&mut to_add, &mut adding);
+        for new in adding.iter().cloned() {
+            rs.insert(new.clone());
+            for LowRule {
+                ref mut if_all,
+                then,
+                ref mut inst,
+            } in rules.iter_mut()
+            {
+                rs.apply_related(new.clone(), if_all, inst, &mut |inst| {
+                    let ins = inst.as_ref();
+                    for implied in then.iter() {
+                        let new_quad = [
+                            ins[&implied.s.0],
+                            ins[&implied.p.0],
+                            ins[&implied.o.0],
+                            ins[&implied.g.0],
+                        ]
+                        .into();
+                        if !rs.contains(&new_quad) && !adding.contains(&new_quad) {
+                            to_add.insert(new_quad);
+                        }
+                    }
+                });
+            }
         }
     }
 
diff --git a/src/prove.rs b/src/prove.rs
index e377882..cf56a8d 100644
--- a/src/prove.rs
+++ b/src/prove.rs
@@ -7,7 +7,7 @@ use crate::translator::Translator;
 use alloc::collections::{BTreeMap, BTreeSet};
 use core::fmt::{Debug, Display};
 
-/// Locate a proof of some composite claims given the provied premises and rules.
+/// Locate a proof of some composite claims given the provided premises and rules.
 ///
 /// ```
 /// # fn main() -> Result<(), Box<dyn std::error::Error>> {
@@ -93,47 +93,70 @@ fn low_prove(
     rules: &[LowRule],
 ) -> Result<Vec<LowRuleApplication>, CantProve> {
     let mut rs = Reasoner::default();
-    for prem in premises {
-        rs.insert(prem.clone());
-    }
-
     // statement (Quad) is proved by applying rule (LowRuleApplication)
     let mut arguments: BTreeMap<Quad, LowRuleApplication> = BTreeMap::new();
+    let mut to_add: BTreeSet<Quad> = premises.iter().cloned().collect();
+
+    for (rule_index, rule) in rules.iter().enumerate() {
+        if rule.if_all.is_empty() {
+            for implied in &rule.then {
+                let new_quad = implied.clone().local_to_global(&rule.inst).unwrap();
+                if to_add.insert(new_quad.clone()) {
+                    arguments.insert(
+                        new_quad,
+                        LowRuleApplication {
+                            rule_index,
+                            instantiations: Default::default(),
+                        },
+                    );
+                }
+            }
+        }
+    }
+    let mut rules2: Vec<(usize, LowRule)> = rules
+        .iter()
+        .cloned()
+        .enumerate()
+        .filter(|(_index, rule)| !rule.if_all.is_empty())
+        .collect();
 
     // reason
-    loop {
-        if to_prove.iter().all(|tp| rs.contains(tp)) {
-            break;
-        }
-        let mut to_add = BTreeSet::<Quad>::new();
-        for (rule_index, rr) in rules.iter().enumerate() {
-            rs.apply(&mut rr.if_all.clone(), &mut rr.inst.clone(), &mut |inst| {
-                let ins = inst.as_ref();
-                for implied in &rr.then {
-                    let new_quad = [
-                        ins[&implied.s.0],
-                        ins[&implied.p.0],
-                        ins[&implied.o.0],
-                        ins[&implied.g.0],
-                    ]
-                    .into();
-                    if !rs.contains(&new_quad) {
-                        arguments
-                            .entry(new_quad.clone())
-                            .or_insert_with(|| LowRuleApplication {
-                                rule_index,
-                                instantiations: ins.clone(),
+    while !to_add.is_empty() && !to_prove.iter().all(|tp| rs.contains(tp)) {
+        let mut adding_now = BTreeSet::<Quad>::new();
+        core::mem::swap(&mut adding_now, &mut to_add);
+        for fact in &adding_now {
+            rs.insert(fact.clone());
+            for (
+                rule_index,
+                LowRule {
+                    ref mut if_all,
+                    then,
+                    ref mut inst,
+                },
+            ) in rules2.iter_mut()
+            {
+                rs.apply_related(fact.clone(), if_all, inst, &mut |inst| {
+                    let ins = inst.as_ref();
+                    for implied in then.iter() {
+                        let new_quad = [
+                            ins[&implied.s.0],
+                            ins[&implied.p.0],
+                            ins[&implied.o.0],
+                            ins[&implied.g.0],
+                        ]
+                        .into();
+                        if !rs.contains(&new_quad) && !adding_now.contains(&new_quad) {
+                            arguments.entry(new_quad.clone()).or_insert_with(|| {
+                                LowRuleApplication {
+                                    rule_index: *rule_index,
+                                    instantiations: ins.clone(),
+                                }
                             });
-                        to_add.insert(new_quad);
+                            to_add.insert(new_quad);
+                        }
                     }
-                }
-            });
-        }
-        if to_add.is_empty() {
-            break;
-        }
-        for new in to_add.into_iter() {
-            rs.insert(new);
+                });
+            }
         }
     }
 
diff --git a/src/reasoner.rs b/src/reasoner.rs
index 572feaf..6557328 100644
--- a/src/reasoner.rs
+++ b/src/reasoner.rs
@@ -10,6 +10,31 @@ pub struct Quad {
     pub g: Grap,
 }
 
+impl Quad {
+    fn zip(self, other: Quad) -> [(usize, usize); 4] {
+        [
+            (self.s.0, other.s.0),
+            (self.p.0, other.p.0),
+            (self.o.0, other.o.0),
+            (self.g.0, other.g.0),
+        ]
+    }
+
+    /// Attempt dereference all variable in self.
+    pub fn local_to_global(self, inst: &Instantiations) -> Option<Quad> {
+        let inst = inst.as_ref();
+        Some(
+            [
+                *inst.get(&self.s.0)?,
+                *inst.get(&self.p.0)?,
+                *inst.get(&self.o.0)?,
+                *inst.get(&self.g.0)?,
+            ]
+            .into(),
+        )
+    }
+}
+
 impl From<[usize; 4]> for Quad {
     fn from([s, p, o, g]: [usize; 4]) -> Self {
         Self {
@@ -102,6 +127,34 @@ impl Reasoner {
         .all(|wn| wn[0] == wn[1]));
     }
 
+    /// Granted a statement find in this store all possible valid instantiations of rule that
+    /// involve the statement. It is expexcted that the statement has already been [Self::insert]ed.
+    pub fn apply_related(
+        &self,
+        quad: Quad,
+        rule: &mut [Quad],
+        instantiations: &mut Instantiations,
+        cb: &mut impl FnMut(&Instantiations),
+    ) {
+        debug_assert!(self.contains(&quad));
+        debug_assert!(!rule.is_empty(), "potential confusing so disallowed");
+        // for each atom of rule, if the atom can match the quad, bind the unbound variables in the
+        // atom to the corresponding elements of quad, then call apply.
+        for i in 0..rule.len() {
+            let (rule_part, rule_rest) = evict(i, rule).unwrap();
+            if can_match(quad.clone(), rule_part.clone(), instantiations) {
+                let to_set = rule_part.clone().zip(quad.clone());
+                for (k, v) in &to_set {
+                    instantiations.write(*k, *v);
+                }
+                self.apply(rule_rest, instantiations, cb);
+                for _ in &to_set {
+                    instantiations.undo().unwrap();
+                }
+            }
+        }
+    }
+
     /// Find in this store all possible valid instantiations of rule. Report the
     /// instantiations through a callback.
     /// TODO: This function is recursive, but not tail recursive. Rules that are too long may
@@ -125,12 +178,7 @@ impl Reasoner {
         // in the requirement to the instantiation then recurse.
         for index in self.matches(strictest, instantiations) {
             let quad = &self.claims[*index];
-            let to_write = [
-                (strictest.s.0, quad.s.0),
-                (strictest.p.0, quad.p.0),
-                (strictest.o.0, quad.o.0),
-                (strictest.g.0, quad.g.0),
-            ];
+            let to_write = strictest.clone().zip(quad.clone());
             for (k, v) in &to_write {
                 debug_assert!(
                     if let Some(committed_v) = instantiations.as_ref().get(&k) {
@@ -193,9 +241,7 @@ impl Reasoner {
     ) -> Option<(&'rule Quad, &'rule mut [Quad])> {
         let index_strictest = (0..rule.len())
             .min_by_key(|index| self.matches(&rule[*index], instantiations).len())?;
-        rule.swap(0, index_strictest);
-        let (strictest, less_strict) = rule.split_first_mut().expect("rule to be non-empty");
-        Some((strictest, less_strict))
+        evict(index_strictest, rule)
     }
 
     /// Get the deduplicated history of all claims that were inserted into this reasoner.
@@ -203,14 +249,33 @@ impl Reasoner {
     pub fn claims(self) -> Vec<Quad> {
         self.claims
     }
+}
 
-    /// Get the deduplicated history of all claims that were inserted into this reasoner.
-    /// The returned list will be in insertion order.
-    pub fn claims_ref(&self) -> &[Quad] {
-        &self.claims
+fn evict<'a, T>(index: usize, unordered_list: &'a mut [T]) -> Option<(&'a T, &'a mut [T])> {
+    if index >= unordered_list.len() {
+        None
+    } else {
+        unordered_list.swap(0, index);
+        let (popped, rest) = unordered_list
+            .split_first_mut()
+            .expect("list to be non-empty");
+        Some((popped, rest))
     }
 }
 
+/// returns whether rule_part could validly be applied to quad assuming the already given
+/// instantiations
+fn can_match(quad: Quad, rule_part: Quad, instantiations: &Instantiations) -> bool {
+    let inst = instantiations.as_ref();
+    rule_part
+        .zip(quad)
+        .iter()
+        .all(|(rp, q)| match inst.get(&rp) {
+            Some(a) => a == q,
+            None => true,
+        })
+}
+
 trait Indexed {
     fn target(rs: &Reasoner) -> &VecSet<usize>;
     fn qcmp(&self, quad: &Quad) -> Ordering;
diff --git a/src/rule.rs b/src/rule.rs
index f512e11..ead7f4a 100644
--- a/src/rule.rs
+++ b/src/rule.rs
@@ -27,6 +27,19 @@ pub(crate) struct LowRule {
     pub inst: Instantiations, // partially maps the local scope to some global scope
 }
 
+// impl LowRule {
+//     /// List all implications as globaly scoped quads.
+//     ///
+//     /// # Panics
+//     ///
+//     /// Panics if rule is not sufficiently instantiated.
+//     pub fn instantiated(&self) -> impl Iterator<Item = Quad> {
+//         let inst = self.inst.as_ref();
+//         self.then.iter().map(|local| {
+//         })
+//     }
+// }
+
 #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Debug)]
 #[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
 pub enum Entity<Unbound, Bound> {

From 65766a9e0770fbe1249e47babdcc9d9d3e13a133 Mon Sep 17 00:00:00 2001
From: Andrew Dirksen <andrew@dirksen.com>
Date: Thu, 22 Apr 2021 17:52:32 -0700
Subject: [PATCH 3/5] MapStack Optimization

impl the optimization described in https://github.com/docknetwork/rify/issues/9

Results are good.
```
test ancestry::infer_          ... bench:   1,201,454 ns/iter (+/- 20,579)
test ancestry::infer_30        ... bench:   3,758,380 ns/iter (+/- 76,535)
test ancestry::prove_          ... bench:   1,342,813 ns/iter (+/- 31,824)
test ancestry::prove_30        ... bench:   4,210,072 ns/iter (+/- 46,268)
test recursion_minimal::infer_ ... bench:      12,014 ns/iter (+/- 232)
test recursion_minimal::prove_ ... bench:      16,378 ns/iter (+/- 357)
```
---
 src/common.rs   | 10 +++----
 src/infer.rs    | 11 ++------
 src/mapstack.rs | 47 +++++++++++++++++++--------------
 src/prove.rs    | 40 +++++++++++++---------------
 src/reasoner.rs | 69 +++++++++++++++++++------------------------------
 src/rule.rs     | 19 ++------------
 6 files changed, 81 insertions(+), 115 deletions(-)

diff --git a/src/common.rs b/src/common.rs
index 6ea7e23..7dc9f2b 100644
--- a/src/common.rs
+++ b/src/common.rs
@@ -33,9 +33,9 @@ where
 /// [crate::prove::prove] function does not immediately convert LowRuleApplication's to
 /// [RuleApplication]'s. Rather, it converts only the LowRuleApplication's it is going to return
 /// to the caller.
-pub struct LowRuleApplication {
+pub(crate) struct LowRuleApplication {
     pub rule_index: usize,
-    pub instantiations: BTreeMap<usize, usize>,
+    pub instantiations: Vec<Option<usize>>,
 }
 
 impl LowRuleApplication {
@@ -65,7 +65,7 @@ impl LowRuleApplication {
 
         for unbound_human in original_rule.cononical_unbound() {
             let unbound_local: usize = uhul[unbound_human];
-            let bound_global: usize = self.instantiations[&unbound_local];
+            let bound_global: usize = self.instantiations.get(unbound_local).unwrap().unwrap();
             let bound_human: &Bound = trans.back(bound_global).unwrap();
             instantiations.push(bound_human.clone());
         }
@@ -81,7 +81,7 @@ impl LowRuleApplication {
 /// This is a helper function. It translates all four element of a quad, calling
 /// [Translator::forward] for each element. If any element has no translation
 /// this function will return `None`.
-pub fn forward<T: Ord>(translator: &Translator<T>, key: &[T; 4]) -> Option<Quad> {
+pub(crate) fn forward<T: Ord>(translator: &Translator<T>, key: &[T; 4]) -> Option<Quad> {
     let [s, p, o, g] = key;
     Some(
         [
@@ -97,7 +97,7 @@ pub fn forward<T: Ord>(translator: &Translator<T>, key: &[T; 4]) -> Option<Quad>
 /// Reverse of [forward].
 /// [forward] translates each element from `T` to `usize`. This function translates each element
 /// from `usize` to `T`. If any element has no translation this function will return `None`.
-pub fn back<T: Ord>(translator: &Translator<T>, key: Quad) -> Option<[&T; 4]> {
+pub(crate) fn back<T: Ord>(translator: &Translator<T>, key: Quad) -> Option<[&T; 4]> {
     let Quad { s, p, o, g } = key;
     Some([
         translator.back(s.0)?,
diff --git a/src/infer.rs b/src/infer.rs
index e4bc0ed..b17c410 100644
--- a/src/infer.rs
+++ b/src/infer.rs
@@ -65,15 +65,8 @@ fn low_infer(premises: &[Quad], rules: &[LowRule]) -> Vec<Quad> {
             } in rules.iter_mut()
             {
                 rs.apply_related(new.clone(), if_all, inst, &mut |inst| {
-                    let ins = inst.as_ref();
-                    for implied in then.iter() {
-                        let new_quad = [
-                            ins[&implied.s.0],
-                            ins[&implied.p.0],
-                            ins[&implied.o.0],
-                            ins[&implied.g.0],
-                        ]
-                        .into();
+                    for implied in then.iter().cloned() {
+                        let new_quad = implied.local_to_global(inst).unwrap();
                         if !rs.contains(&new_quad) && !adding.contains(&new_quad) {
                             to_add.insert(new_quad);
                         }
diff --git a/src/mapstack.rs b/src/mapstack.rs
index a17ab67..08d9970 100644
--- a/src/mapstack.rs
+++ b/src/mapstack.rs
@@ -1,51 +1,58 @@
-use alloc::collections::BTreeMap;
 use core::fmt;
 use core::fmt::Debug;
 use core::iter::FromIterator;
 
 /// A mapping that keeps a history of writes. Writes to the map effect "pushes" to a stack. Those
 /// "pushes" can be undone with a "pop".
-#[derive(Clone, Debug, PartialEq, Eq)]
-pub struct MapStack<K, V> {
-    current: BTreeMap<K, V>,
-    history: Vec<(K, Option<V>)>,
+///
+/// Beware large keys when using this data structure. The memory used byt this structure scales
+/// with the size of the largest key!
+#[derive(Clone, Debug, PartialEq, Eq, Ord, PartialOrd, Default)]
+pub(crate) struct MapStack<V> {
+    current: Vec<Option<V>>,
+    history: Vec<(usize, Option<V>)>,
 }
 
-impl<K: Ord, V> MapStack<K, V> {
+impl<V> MapStack<V> {
     pub fn new() -> Self {
         Self {
-            current: BTreeMap::new(),
+            current: Vec::new(),
             history: Vec::new(),
         }
     }
 }
 
-impl<K: Ord + Clone, V> MapStack<K, V> {
+impl<V> MapStack<V> {
     /// Set a value appending to write history.
-    pub fn write(&mut self, key: K, val: V) {
-        let old_val = self.current.insert(key.clone(), val);
-        self.history.push((key, old_val));
+    pub fn write(&mut self, key: usize, val: V) {
+        debug_assert!(key < 30 ^ 2, "Thats a pretty large key. Are you sure?");
+        if self.current.len() <= key {
+            self.current.resize_with(key + 1, || None);
+        }
+        let mut val = Some(val);
+        core::mem::swap(&mut self.current[key], &mut val);
+        self.history.push((key, val));
     }
 
     /// Undo most recent write or return error if there is no history to undo.
     pub fn undo(&mut self) -> Result<(), NoMoreHistory> {
         let (key, old_val) = self.history.pop().ok_or(NoMoreHistory)?;
-        match old_val {
-            Some(val) => self.current.insert(key, val),
-            None => self.current.remove(&key),
-        };
+        self.current[key] = old_val;
         Ok(())
     }
-}
 
-impl<K, V> AsRef<BTreeMap<K, V>> for MapStack<K, V> {
-    fn as_ref(&self) -> &BTreeMap<K, V> {
+    /// Get the current value at key.
+    pub fn get(&self, key: usize) -> Option<&V> {
+        self.current.get(key).and_then(|o| o.as_ref())
+    }
+
+    pub fn inner(&self) -> &Vec<Option<V>> {
         &self.current
     }
 }
 
-impl<K: Ord + Clone, V> FromIterator<(K, V)> for MapStack<K, V> {
-    fn from_iter<T: IntoIterator<Item = (K, V)>>(kvs: T) -> Self {
+impl<V> FromIterator<(usize, V)> for MapStack<V> {
+    fn from_iter<T: IntoIterator<Item = (usize, V)>>(kvs: T) -> Self {
         let mut ret = Self::new();
         for (k, v) in kvs.into_iter() {
             ret.write(k, v);
diff --git a/src/prove.rs b/src/prove.rs
index cf56a8d..145d5db 100644
--- a/src/prove.rs
+++ b/src/prove.rs
@@ -136,20 +136,13 @@ fn low_prove(
             ) in rules2.iter_mut()
             {
                 rs.apply_related(fact.clone(), if_all, inst, &mut |inst| {
-                    let ins = inst.as_ref();
-                    for implied in then.iter() {
-                        let new_quad = [
-                            ins[&implied.s.0],
-                            ins[&implied.p.0],
-                            ins[&implied.o.0],
-                            ins[&implied.g.0],
-                        ]
-                        .into();
+                    for implied in then.iter().cloned() {
+                        let new_quad = implied.local_to_global(inst).unwrap();
                         if !rs.contains(&new_quad) && !adding_now.contains(&new_quad) {
                             arguments.entry(new_quad.clone()).or_insert_with(|| {
                                 LowRuleApplication {
                                     rule_index: *rule_index,
-                                    instantiations: ins.clone(),
+                                    instantiations: inst.inner().clone(),
                                 }
                             });
                             to_add.insert(new_quad);
@@ -183,8 +176,11 @@ fn recall_proof(
     outp: &mut Vec<LowRuleApplication>,
 ) {
     let to_global_scope = |rra: &LowRuleApplication, locally_scoped: usize| -> usize {
-        let concrete = rules[rra.rule_index].inst.as_ref().get(&locally_scoped);
-        let found = rra.instantiations.get(&locally_scoped);
+        let concrete = rules[rra.rule_index].inst.get(locally_scoped);
+        let found = rra
+            .instantiations
+            .get(locally_scoped)
+            .and_then(|o| o.as_ref());
         if let (Some(c), Some(f)) = (concrete, found) {
             debug_assert_eq!(c, f);
         }
@@ -237,7 +233,7 @@ impl std::error::Error for CantProve {}
 /// An element of a deductive proof. Proofs can be transmitted and later validatated as long as the
 /// validator assumes the same rule list as the prover.
 ///
-/// Unbound variables are bound to the values in `instanitations`. They are bound in order of
+/// Unbound variables are bound to the values in `instantiations`. They are bound in order of
 /// initial appearance.
 ///
 /// Given the rule:
@@ -311,31 +307,31 @@ impl<Bound: Clone> RuleApplication<Bound> {
 /// Panics
 ///
 /// panics if an unbound entity is not registered in map
-/// panics if the canonical index of unbound (according to map) is too large to index instanitations
+/// panics if the canonical index of unbound (according to map) is too large to index instantiations
 fn bind_claim<Unbound: Ord, Bound: Clone>(
     [s, p, o, g]: [Entity<Unbound, Bound>; 4],
     map: &BTreeMap<&Unbound, usize>,
-    instanitations: &[Bound],
+    instantiations: &[Bound],
 ) -> [Bound; 4] {
     [
-        bind_entity(s, map, instanitations),
-        bind_entity(p, map, instanitations),
-        bind_entity(o, map, instanitations),
-        bind_entity(g, map, instanitations),
+        bind_entity(s, map, instantiations),
+        bind_entity(p, map, instantiations),
+        bind_entity(o, map, instantiations),
+        bind_entity(g, map, instantiations),
     ]
 }
 
 /// Panics
 ///
 /// panics if an unbound entity is not registered in map
-/// panics if the canonical index of unbound (according to map) is too large to index instanitations
+/// panics if the canonical index of unbound (according to map) is too large to index instantiations
 fn bind_entity<Unbound: Ord, Bound: Clone>(
     e: Entity<Unbound, Bound>,
     map: &BTreeMap<&Unbound, usize>,
-    instanitations: &[Bound],
+    instantiations: &[Bound],
 ) -> Bound {
     match e {
-        Entity::Unbound(a) => instanitations[map[&a]].clone(),
+        Entity::Unbound(a) => instantiations[map[&a]].clone(),
         Entity::Bound(e) => e,
     }
 }
diff --git a/src/reasoner.rs b/src/reasoner.rs
index 6557328..bcd5c70 100644
--- a/src/reasoner.rs
+++ b/src/reasoner.rs
@@ -3,7 +3,7 @@ use crate::vecset::VecSet;
 use core::cmp::Ordering;
 
 #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
-pub struct Quad {
+pub(crate) struct Quad {
     pub s: Subj,
     pub p: Prop,
     pub o: Obje,
@@ -22,13 +22,12 @@ impl Quad {
 
     /// Attempt dereference all variable in self.
     pub fn local_to_global(self, inst: &Instantiations) -> Option<Quad> {
-        let inst = inst.as_ref();
         Some(
             [
-                *inst.get(&self.s.0)?,
-                *inst.get(&self.p.0)?,
-                *inst.get(&self.o.0)?,
-                *inst.get(&self.g.0)?,
+                *inst.get(self.s.0)?,
+                *inst.get(self.p.0)?,
+                *inst.get(self.o.0)?,
+                *inst.get(self.g.0)?,
             ]
             .into(),
         )
@@ -82,10 +81,10 @@ type O = (Obje,);
 type G = (Grap,);
 
 /// Bindings of slots within the context of a rule.
-pub type Instantiations = MapStack<usize, usize>;
+pub(crate) type Instantiations = MapStack<usize>;
 
 #[derive(Default)]
-pub struct Reasoner {
+pub(crate) struct Reasoner {
     claims: Vec<Quad>,
     spog: VecSet<usize>,
     posg: VecSet<usize>,
@@ -137,7 +136,7 @@ impl Reasoner {
         cb: &mut impl FnMut(&Instantiations),
     ) {
         debug_assert!(self.contains(&quad));
-        debug_assert!(!rule.is_empty(), "potential confusing so disallowed");
+        debug_assert!(!rule.is_empty(), "potentialy confusing so disallowed");
         // for each atom of rule, if the atom can match the quad, bind the unbound variables in the
         // atom to the corresponding elements of quad, then call apply.
         for i in 0..rule.len() {
@@ -181,7 +180,7 @@ impl Reasoner {
             let to_write = strictest.clone().zip(quad.clone());
             for (k, v) in &to_write {
                 debug_assert!(
-                    if let Some(committed_v) = instantiations.as_ref().get(&k) {
+                    if let Some(committed_v) = instantiations.get(*k) {
                         committed_v == v
                     } else {
                         true
@@ -200,13 +199,12 @@ impl Reasoner {
     /// Return a slice representing all possible matches to the pattern provided.
     /// pattern is in a local scope. instantiations is a partial translation of that
     /// local scope to the global scope represented by self.claims
-    fn matches(&self, pattern: &Quad, instantiations: &Instantiations) -> &[usize] {
-        let inst = instantiations.as_ref();
+    fn matches(&self, pattern: &Quad, inst: &Instantiations) -> &[usize] {
         let pattern: (Option<Subj>, Option<Prop>, Option<Obje>, Option<Grap>) = (
-            inst.get(&pattern.s.0).cloned().map(Subj),
-            inst.get(&pattern.p.0).cloned().map(Prop),
-            inst.get(&pattern.o.0).cloned().map(Obje),
-            inst.get(&pattern.g.0).cloned().map(Grap),
+            inst.get(pattern.s.0).cloned().map(Subj),
+            inst.get(pattern.p.0).cloned().map(Prop),
+            inst.get(pattern.o.0).cloned().map(Obje),
+            inst.get(pattern.g.0).cloned().map(Grap),
         );
         match pattern {
             (Some(s), Some(p), Some(o), Some(g)) => (s, p, o, g).search(self),
@@ -251,7 +249,7 @@ impl Reasoner {
     }
 }
 
-fn evict<'a, T>(index: usize, unordered_list: &'a mut [T]) -> Option<(&'a T, &'a mut [T])> {
+fn evict<T>(index: usize, unordered_list: &mut [T]) -> Option<(&T, &mut [T])> {
     if index >= unordered_list.len() {
         None
     } else {
@@ -265,12 +263,11 @@ fn evict<'a, T>(index: usize, unordered_list: &'a mut [T]) -> Option<(&'a T, &'a
 
 /// returns whether rule_part could validly be applied to quad assuming the already given
 /// instantiations
-fn can_match(quad: Quad, rule_part: Quad, instantiations: &Instantiations) -> bool {
-    let inst = instantiations.as_ref();
+fn can_match(quad: Quad, rule_part: Quad, inst: &Instantiations) -> bool {
     rule_part
         .zip(quad)
         .iter()
-        .all(|(rp, q)| match inst.get(&rp) {
+        .all(|(rp, q)| match inst.get(*rp) {
             Some(a) => a == q,
             None => true,
         })
@@ -352,7 +349,7 @@ mod tests {
         LowRule, Rule,
     };
     use crate::translator::Translator;
-    use alloc::collections::{BTreeMap, BTreeSet};
+    use alloc::collections::BTreeSet;
 
     #[test]
     fn ancestry_raw() {
@@ -408,7 +405,7 @@ mod tests {
 
         // This test only does one round of reasoning, no forward chaining. We will need a forward
         // chaining test eventually.
-        let mut results = Vec::<BTreeMap<usize, usize>>::new();
+        let mut results = Vec::<Vec<Option<usize>>>::new();
         for rule in rules {
             let Rule {
                 mut if_all,
@@ -416,7 +413,7 @@ mod tests {
                 mut inst,
             } = rule.clone();
             ts.apply(&mut if_all, &mut inst, &mut |inst| {
-                results.push(inst.as_ref().clone())
+                results.push(inst.inner().clone())
             });
         }
 
@@ -425,20 +422,15 @@ mod tests {
         // The second rule, (?a ancestor ?b ?g) and (?b ancestor ?c ?g) -> (?a ancestor ?c ?g),
         // should not activate because results from application of first rule have not been added
         // to the rdf store so there are there are are not yet any ancestry relations present.
-        let mut expected_intantiations: Vec<BTreeMap<usize, usize>> = nodes
+        let mut expected_intantiations: Vec<Vec<Option<usize>>> = nodes
             .iter()
             .zip(nodes.iter().cycle().skip(1))
             .map(|(a, b)| {
-                [
-                    (0, *a),
-                    (1, parent.0),
-                    (2, *b),
-                    (3, ancestor.0),
-                    (4, default_graph.0),
-                ]
-                .iter()
-                .cloned()
-                .collect()
+                [*a, parent.0, *b, ancestor.0, default_graph.0]
+                    .iter()
+                    .cloned()
+                    .map(Some)
+                    .collect()
             })
             .collect();
         results.sort();
@@ -517,14 +509,7 @@ mod tests {
                 let then = &rule.then;
                 ts.apply(&mut if_all, &mut inst, &mut |inst| {
                     for implied in then {
-                        let inst = inst.as_ref();
-                        let new: Quad = [
-                            inst[&implied.s.0],
-                            inst[&implied.p.0],
-                            inst[&implied.o.0],
-                            inst[&implied.g.0],
-                        ]
-                        .into();
+                        let new: Quad = implied.clone().local_to_global(inst).unwrap();
                         if !ts.contains(&new) {
                             to_add.insert(new);
                         }
diff --git a/src/rule.rs b/src/rule.rs
index ead7f4a..605e566 100644
--- a/src/rule.rs
+++ b/src/rule.rs
@@ -27,19 +27,6 @@ pub(crate) struct LowRule {
     pub inst: Instantiations, // partially maps the local scope to some global scope
 }
 
-// impl LowRule {
-//     /// List all implications as globaly scoped quads.
-//     ///
-//     /// # Panics
-//     ///
-//     /// Panics if rule is not sufficiently instantiated.
-//     pub fn instantiated(&self) -> impl Iterator<Item = Quad> {
-//         let inst = self.inst.as_ref();
-//         self.then.iter().map(|local| {
-//         })
-//     }
-// }
-
 #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Debug)]
 #[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
 pub enum Entity<Unbound, Bound> {
@@ -298,8 +285,7 @@ mod test {
                 .map(|local_name| {
                     re_rulea
                         .inst
-                        .as_ref()
-                        .get(&local_name)
+                        .get(*local_name)
                         .map(|global_name| trans.back(*global_name).unwrap().clone())
                 })
                 .collect();
@@ -353,8 +339,7 @@ mod test {
                 .map(|local_name| {
                     re_ruleb
                         .inst
-                        .as_ref()
-                        .get(&local_name)
+                        .get(*local_name)
                         .map(|global_name| trans.back(*global_name).unwrap().clone())
                 })
                 .collect();

From cfb572eaf3358eb268ea3bec586ef3a8f15a645b Mon Sep 17 00:00:00 2001
From: Andrew Dirksen <andrew@dirksen.com>
Date: Fri, 23 Apr 2021 09:32:42 -0700
Subject: [PATCH 4/5] bump versions to prepare for publish

---
 Cargo.toml                    | 2 +-
 bindings/js_wasm/package.json | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index 25c9555..5ac6149 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "rify"
-version = "0.7.0"
+version = "0.7.1"
 authors = [
   "Andrew Dirksen <andrew@dirksen.com>",
   "Sam Hellawell <sshellawell@gmail.com>"
diff --git a/bindings/js_wasm/package.json b/bindings/js_wasm/package.json
index 64d3e2a..b60401d 100644
--- a/bindings/js_wasm/package.json
+++ b/bindings/js_wasm/package.json
@@ -5,7 +5,7 @@
     "Sam Hellawell <sshellawell@gmail.com>"
   ],
   "description": "RDF reasoner that operates on RIF-like conjunctive rules. Outputs a machine\nreadable proof of some claim which can be cheaply verified.\n",
-  "version": "0.7.0",
+  "version": "0.7.1",
   "license": "MIT OR Apache-2.0",
   "repository": {
     "type": "git",

From e23a00f8d932cf6a029098085d178d3ad32516bc Mon Sep 17 00:00:00 2001
From: Andrew Dirksen <andrew@dirksen.com>
Date: Fri, 23 Apr 2021 10:31:10 -0700
Subject: [PATCH 5/5] scripts for publish

---
 justfile | 26 +++++++++++++++++++++++---
 1 file changed, 23 insertions(+), 3 deletions(-)

diff --git a/justfile b/justfile
index 80bb7e6..72b8abf 100644
--- a/justfile
+++ b/justfile
@@ -31,15 +31,35 @@ js-test:
 clean:
   cargo clean
   cd benches; cargo clean
-  rm -r bindings/js_wasm/pkg || true
+  rm -rf bindings/js_wasm/pkg
   just clean-js
 
 # remove artifacts from js bindings tests
 clean-js:
-  rm -r bindings/js_wasm/binding_tests/dist || true
-  rm -r bindings/js_wasm/binding_tests/node_modules || true
+  rm -rf bindings/js_wasm/binding_tests/dist
+  rm -rf bindings/js_wasm/binding_tests/node_modules
 
 bench:
   #!/usr/bin/env bash
   cd benches
   cargo bench
+
+checkall-buildall:
+  just clean
+  cargo test
+  cargo clippy -- -D warnings
+  just bench
+  just js-test
+
+assert-clean-workdir:
+  ! test -n "$(git status --porcelain)" # please commit before publish
+
+publish-js:
+  just checkall-buildall
+  just assert-clean-workdir
+  cd bindings/js_wasm/pkg && npm publish
+
+publish-rs:
+  just checkall-buildall
+  just assert-clean-workdir
+  cargo publish