diff --git a/Cargo.toml b/Cargo.toml
index e25e8f4..c401174 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -18,5 +18,13 @@ pyo3 = { version = "0.18.0", features = ["extension-module"] }
criterion = "0.4.0"
[[bench]]
-name = "benches"
+name = "search_big"
+harness = false
+
+[[bench]]
+name = "search"
+harness = false
+
+[[bench]]
+name = "vm"
harness = false
diff --git a/Makefile b/Makefile
index e4974ad..d745702 100644
--- a/Makefile
+++ b/Makefile
@@ -7,5 +7,16 @@ flamegraph:
flamegraph-debug:
cargo flamegraph --dev -o debug_flamegraph.svg --bench search -- --bench
+asm:
+ cargo clean
+ cargo rustc --release --lib -- --emit asm=.vscode/asm_mangled
+ pwsh -Command 'Get-Content .vscode/asm_mangled | c++filt > .\src\lib.S'
+ pwsh -Command 'Remove-Item .vscode/asm_mangled'
+
+maturin:
+ pwsh -Command 'venv/Scripts/activate; maturin develop --release'
-.PHONY: criterion flamegraph flamegraph-debug
\ No newline at end of file
+hyperfine:
+ hyperfine --show-output --parameter-scan n 5 20 -S 'pwsh' -s 'venv/scripts/activate' --export-json hyperfine.json --export-csv hyperfine.csv 'python ./pytest/timing.py {n}'
+
+.PHONY: criterion flamegraph flamegraph-debug asm hyperfine maturin
\ No newline at end of file
diff --git a/benches/benches.rs b/benches/benches.rs
deleted file mode 100644
index faa2981..0000000
--- a/benches/benches.rs
+++ /dev/null
@@ -1,65 +0,0 @@
-#[macro_use]
-extern crate criterion;
-extern crate adversary;
-
-use criterion::{criterion_group, criterion_main, Criterion};
-
-fn vm(c: &mut Criterion) {
- let expression =
- adversary::vm::parsing::parse_relation("and (= (ham (^ x y)) (ham (+ 3 x))) (> (* x y) 5)");
- if let Err(e) = expression {
- println!("{}", e);
- panic!();
- }
- let code = adversary::vm::compile_boolean(expression.unwrap());
- let mut stack = adversary::vm::VmStack::from_code(&code);
- c.bench_function("vm", |b| {
- b.iter(|| {
- for x in 0..(1 << 6) {
- for y in 0..(1 << 6) {
- criterion::black_box(
- adversary::vm::Vm::load(
- &code,
- adversary::vm::Registers::load(x, y, 6, 0, 0),
- &mut stack,
- )
- .run(),
- );
- }
- }
- })
- });
-}
-
-fn search(c: &mut Criterion) {
- pyo3::prepare_freethreaded_python();
- pyo3::Python::with_gil(|_py| {
- let obj = adversary::Prover::py_new(
- "= (ham x) k".to_string(),
- "= (ham y) (+ k 1)".to_string(),
- "<= ham (^ x y) p".to_string(),
- )
- .unwrap();
- c.bench_function("search", |b| {
- b.iter(|| criterion::black_box(obj.find_bounds(10, 5, 3)));
- });
- })
-}
-
-fn search_big(c: &mut Criterion) {
- pyo3::prepare_freethreaded_python();
- pyo3::Python::with_gil(|_py| {
- let obj = adversary::Prover::py_new(
- "= (ham x) k".to_string(),
- "= (ham y) (+ k 1)".to_string(),
- "<= ham (^ x y) p".to_string(),
- )
- .unwrap();
- c.bench_function("search_big", |b| {
- b.iter(|| criterion::black_box(obj.find_bounds(12, 5, 8)));
- });
- })
-}
-
-criterion_group!(benches, vm, search, search_big);
-criterion_main!(benches);
diff --git a/benches/search.rs b/benches/search.rs
new file mode 100644
index 0000000..0a8ca4a
--- /dev/null
+++ b/benches/search.rs
@@ -0,0 +1,23 @@
+#[macro_use]
+extern crate criterion;
+extern crate adversary;
+
+use criterion::{criterion_group, criterion_main, Criterion};
+
+fn bench_search(c: &mut Criterion) {
+ pyo3::prepare_freethreaded_python();
+ pyo3::Python::with_gil(|_py| {
+ let obj = adversary::Prover::py_new(
+ "= (ham x) k".to_string(),
+ "= (ham y) (+ k 1)".to_string(),
+ "<= ham (^ x y) p".to_string(),
+ )
+ .unwrap();
+ c.bench_function("search", |b| {
+ b.iter(|| criterion::black_box(obj.find_bounds(10, 5, 3)));
+ });
+ })
+}
+
+criterion_group!(search, bench_search);
+criterion_main!(search);
\ No newline at end of file
diff --git a/benches/search_big.rs b/benches/search_big.rs
new file mode 100644
index 0000000..6f7bfb2
--- /dev/null
+++ b/benches/search_big.rs
@@ -0,0 +1,23 @@
+#[macro_use]
+extern crate criterion;
+extern crate adversary;
+
+use criterion::{criterion_group, criterion_main, Criterion};
+
+fn bench_search_big(c: &mut Criterion) {
+ pyo3::prepare_freethreaded_python();
+ pyo3::Python::with_gil(|_py| {
+ let obj = adversary::Prover::py_new(
+ "= (ham x) k".to_string(),
+ "= (ham y) (+ k 1)".to_string(),
+ "<= ham (^ x y) p".to_string(),
+ )
+ .unwrap();
+ c.bench_function("search_big", |b| {
+ b.iter(|| criterion::black_box(obj.find_bounds(12, 5, 8)));
+ });
+ })
+}
+
+criterion_group!(search_big, bench_search_big);
+criterion_main!(search_big);
diff --git a/benches/vm.rs b/benches/vm.rs
new file mode 100644
index 0000000..e761716
--- /dev/null
+++ b/benches/vm.rs
@@ -0,0 +1,35 @@
+#[macro_use]
+extern crate criterion;
+extern crate adversary;
+
+use criterion::{criterion_group, criterion_main, Criterion};
+
+fn bench_vm(c: &mut Criterion) {
+ let expression =
+ adversary::vm::parsing::parse_relation("and (= (ham (^ x y)) (ham (+ 3 x))) (> (* x y) 5)");
+ if let Err(e) = expression {
+ println!("{}", e);
+ panic!();
+ }
+ let code = adversary::vm::compile_boolean(expression.unwrap());
+ let mut stack = adversary::vm::VmStack::from_code(&code);
+ c.bench_function("vm", |b| {
+ b.iter(|| {
+ for x in 0..(1 << 6) {
+ for y in 0..(1 << 6) {
+ criterion::black_box(
+ adversary::vm::Vm::load(
+ &code,
+ adversary::vm::Registers::load(x, y, 6, 0, 0),
+ &mut stack,
+ )
+ .run(),
+ );
+ }
+ }
+ })
+ });
+}
+
+criterion_group!(vm, bench_vm);
+criterion_main!(vm);
\ No newline at end of file
diff --git a/hyperfine.csv b/hyperfine.csv
new file mode 100644
index 0000000..4b3fe2d
--- /dev/null
+++ b/hyperfine.csv
@@ -0,0 +1,17 @@
+#command,mean,stddev,median,user,system,min,max,parameter_n
+"python ./pytest/timing.py 5",0.04581394800000006,0.00816270671734837,0.04668517800000005,0.026718750000000003,0.019218749999999996,0.032075278000000096,0.05514677800000001,5
+"python ./pytest/timing.py 6",0.042371348000000066,0.007327761603207661,0.04315997800000004,0.009812500000000002,0.010281249999999997,0.03199467800000011,0.05567727800000011,6
+"python ./pytest/timing.py 7",0.04077101800000005,0.008782824810351926,0.040449628000000015,0.029562500000000002,0.016093749999999997,0.028448878000000066,0.05205177800000005,7
+"python ./pytest/timing.py 8",0.04834307800000006,0.008276160843853466,0.04665782800000007,0.041781250000000006,0.05874999999999999,0.03589267800000007,0.06276897800000003,8
+"python ./pytest/timing.py 9",0.04610321800000006,0.01221144375440967,0.04276542800000005,0.004125000000000001,0.005593749999999997,0.031109278000000073,0.06754577800000006,9
+"python ./pytest/timing.py 10",0.656881348,1.816322202089533,0.04675287800000005,0.02075,0.00915625,0.03219597800000007,5.8203265779999995,10
+"python ./pytest/timing.py 11",0.04503963800000007,0.005758636203747479,0.04366842800000009,0.018906250000000003,0.029718749999999995,0.03824637800000008,0.056746278000000094,11
+"python ./pytest/timing.py 12",0.06112314800000005,0.01715353160780924,0.05904557800000004,0.02146875,0.025031249999999994,0.03643177800000008,0.09102267800000008,12
+"python ./pytest/timing.py 13",0.07466937800000005,0.040038996149254304,0.060930978000000025,0.040781250000000005,0.017656249999999995,0.03599187800000003,0.15105747800000002,13
+"python ./pytest/timing.py 14",0.12913027800000004,0.16291293196519285,0.05922252800000005,0.10300000000000001,0.004249999999999999,0.035453378000000035,0.5145964780000001,14
+"python ./pytest/timing.py 15",0.5586950680000001,0.7332788059539814,0.17217967800000006,0.500875,0.005593749999999997,0.03280447800000008,2.137246578,15
+"python ./pytest/timing.py 16",2.576790488,2.687933192209969,1.668545078,2.5227499999999994,0.03284374999999999,0.041527578000000065,6.829759978,16
+"python ./pytest/timing.py 17",5.479623618,7.132625194222096,3.4482901779999997,5.43184375,0.015874999999999993,0.05124057800000004,21.924067778,17
+"python ./pytest/timing.py 18",34.976559767999994,45.33047970462983,1.2725040280000002,34.897749999999995,0.020562499999999994,0.03764907800000006,95.283775278,18
+"python ./pytest/timing.py 19",100.16646647799999,143.37612065560103,1.117140078,100.04775,0.022343749999999996,0.036464678000000084,385.89288487799996,19
+"python ./pytest/timing.py 20",253.70613178800005,435.7539383326962,75.73695792800001,253.42871875,0.047562499999999994,0.0477563780000001,1400.148915478,20
diff --git a/hyperfine.json b/hyperfine.json
new file mode 100644
index 0000000..beb844d
--- /dev/null
+++ b/hyperfine.json
@@ -0,0 +1,596 @@
+{
+ "results": [
+ {
+ "command": "python ./pytest/timing.py 5",
+ "mean": 0.04581394800000006,
+ "stddev": 0.00816270671734837,
+ "median": 0.04668517800000005,
+ "user": 0.026718750000000003,
+ "system": 0.019218749999999996,
+ "min": 0.032075278000000096,
+ "max": 0.05514677800000001,
+ "times": [
+ 0.05514677800000001,
+ 0.043960078000000014,
+ 0.047457178000000044,
+ 0.054621078000000045,
+ 0.045913178000000054,
+ 0.032075278000000096,
+ 0.05370557800000009,
+ 0.040872578000000104,
+ 0.05016877800000008,
+ 0.034218978000000067
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "5"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 6",
+ "mean": 0.042371348000000066,
+ "stddev": 0.007327761603207661,
+ "median": 0.04315997800000004,
+ "user": 0.009812500000000002,
+ "system": 0.010281249999999997,
+ "min": 0.03199467800000011,
+ "max": 0.05567727800000011,
+ "times": [
+ 0.04193087800000006,
+ 0.03199467800000011,
+ 0.033345078000000083,
+ 0.046498178,
+ 0.0482699780000001,
+ 0.04545117800000009,
+ 0.044389078000000026,
+ 0.04078387800000005,
+ 0.05567727800000011,
+ 0.03537327800000001
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "6"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 7",
+ "mean": 0.04077101800000005,
+ "stddev": 0.008782824810351926,
+ "median": 0.040449628000000015,
+ "user": 0.029562500000000002,
+ "system": 0.016093749999999997,
+ "min": 0.028448878000000066,
+ "max": 0.05205177800000005,
+ "times": [
+ 0.03829057800000002,
+ 0.03260187800000003,
+ 0.04944087800000008,
+ 0.05205177800000005,
+ 0.052009178000000045,
+ 0.04572607800000006,
+ 0.03360147800000002,
+ 0.028448878000000066,
+ 0.04260867800000001,
+ 0.032930778000000105
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "7"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 8",
+ "mean": 0.04834307800000006,
+ "stddev": 0.008276160843853466,
+ "median": 0.04665782800000007,
+ "user": 0.041781250000000006,
+ "system": 0.05874999999999999,
+ "min": 0.03589267800000007,
+ "max": 0.06276897800000003,
+ "times": [
+ 0.06276897800000003,
+ 0.051798178000000084,
+ 0.0451638780000001,
+ 0.04575477800000005,
+ 0.05026417800000005,
+ 0.03589267800000007,
+ 0.047560878000000084,
+ 0.040741878000000065,
+ 0.043394178000000005,
+ 0.06009117800000008
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "8"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 9",
+ "mean": 0.04610321800000006,
+ "stddev": 0.01221144375440967,
+ "median": 0.04276542800000005,
+ "user": 0.004125000000000001,
+ "system": 0.005593749999999997,
+ "min": 0.031109278000000073,
+ "max": 0.06754577800000006,
+ "times": [
+ 0.055943378000000044,
+ 0.031109278000000073,
+ 0.03689987800000005,
+ 0.03579857800000008,
+ 0.04079887800000004,
+ 0.03652607800000007,
+ 0.04473197800000006,
+ 0.06754577800000006,
+ 0.050433578000000034,
+ 0.061244778000000055
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "9"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 10",
+ "mean": 0.656881348,
+ "stddev": 1.816322202089533,
+ "median": 0.04675287800000005,
+ "user": 0.02075,
+ "system": 0.00915625,
+ "min": 0.03219597800000007,
+ "max": 5.8203265779999995,
+ "times": [
+ 5.8203265779999995,
+ 0.31030617800000004,
+ 0.14147657800000002,
+ 0.066758278,
+ 0.03356697800000008,
+ 0.05600177800000006,
+ 0.03219597800000007,
+ 0.03594707800000008,
+ 0.03473007800000005,
+ 0.03750397800000005
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "10"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 11",
+ "mean": 0.04503963800000007,
+ "stddev": 0.005758636203747479,
+ "median": 0.04366842800000009,
+ "user": 0.018906250000000003,
+ "system": 0.029718749999999995,
+ "min": 0.03824637800000008,
+ "max": 0.056746278000000094,
+ "times": [
+ 0.056746278000000094,
+ 0.04288307800000002,
+ 0.04308117800000011,
+ 0.03849437800000011,
+ 0.048631578000000064,
+ 0.042227278000000035,
+ 0.04431167800000002,
+ 0.0515188780000001,
+ 0.03824637800000008,
+ 0.044255678000000076
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "11"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 12",
+ "mean": 0.06112314800000005,
+ "stddev": 0.01715353160780924,
+ "median": 0.05904557800000004,
+ "user": 0.02146875,
+ "system": 0.025031249999999994,
+ "min": 0.03643177800000008,
+ "max": 0.09102267800000008,
+ "times": [
+ 0.06700417800000003,
+ 0.09102267800000008,
+ 0.07156757800000002,
+ 0.07994157800000001,
+ 0.06872617800000003,
+ 0.04994327800000009,
+ 0.046060578000000074,
+ 0.03643177800000008,
+ 0.05108697800000006,
+ 0.04944667800000002
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "12"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 13",
+ "mean": 0.07466937800000005,
+ "stddev": 0.040038996149254304,
+ "median": 0.060930978000000025,
+ "user": 0.040781250000000005,
+ "system": 0.017656249999999995,
+ "min": 0.03599187800000003,
+ "max": 0.15105747800000002,
+ "times": [
+ 0.07185757800000003,
+ 0.036325978000000037,
+ 0.0923784780000001,
+ 0.057389278000000044,
+ 0.1357676780000001,
+ 0.0541288780000001,
+ 0.03599187800000003,
+ 0.15105747800000002,
+ 0.064472678,
+ 0.04732387800000004
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "13"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 14",
+ "mean": 0.12913027800000004,
+ "stddev": 0.16291293196519285,
+ "median": 0.05922252800000005,
+ "user": 0.10300000000000001,
+ "system": 0.004249999999999999,
+ "min": 0.035453378000000035,
+ "max": 0.5145964780000001,
+ "times": [
+ 0.07471897800000005,
+ 0.035453378000000035,
+ 0.048438178000000054,
+ 0.05548507800000002,
+ 0.05164857800000011,
+ 0.04432947800000009,
+ 0.5145964780000001,
+ 0.06295997800000008,
+ 0.06315467800000008,
+ 0.34051797800000005
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "14"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 15",
+ "mean": 0.5586950680000001,
+ "stddev": 0.7332788059539814,
+ "median": 0.17217967800000006,
+ "user": 0.500875,
+ "system": 0.005593749999999997,
+ "min": 0.03280447800000008,
+ "max": 2.137246578,
+ "times": [
+ 0.7437489780000002,
+ 0.08189187800000008,
+ 0.0344190780000001,
+ 0.7140736780000001,
+ 0.03280447800000008,
+ 0.040056478000000006,
+ 0.26246747800000003,
+ 2.137246578,
+ 0.040682278000000016,
+ 1.499559778
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "15"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 16",
+ "mean": 2.576790488,
+ "stddev": 2.687933192209969,
+ "median": 1.668545078,
+ "user": 2.5227499999999994,
+ "system": 0.03284374999999999,
+ "min": 0.041527578000000065,
+ "max": 6.829759978,
+ "times": [
+ 6.602360178,
+ 0.39307727800000003,
+ 0.041527578000000065,
+ 0.057177678000000065,
+ 4.293663578,
+ 6.829759978,
+ 0.08836797800000007,
+ 1.690802878,
+ 4.124880478,
+ 1.646287278
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "16"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 17",
+ "mean": 5.479623618,
+ "stddev": 7.132625194222096,
+ "median": 3.4482901779999997,
+ "user": 5.43184375,
+ "system": 0.015874999999999993,
+ "min": 0.05124057800000004,
+ "max": 21.924067778,
+ "times": [
+ 3.617135778,
+ 11.049047278,
+ 3.4278150779999996,
+ 0.116646778,
+ 0.17526147800000003,
+ 3.468765278,
+ 10.884210377999999,
+ 21.924067778,
+ 0.05124057800000004,
+ 0.08204577800000001
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "17"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 18",
+ "mean": 34.976559767999994,
+ "stddev": 45.33047970462983,
+ "median": 1.2725040280000002,
+ "user": 34.897749999999995,
+ "system": 0.020562499999999994,
+ "min": 0.03764907800000006,
+ "max": 95.283775278,
+ "times": [
+ 65.275574278,
+ 93.015606878,
+ 93.44633337799999,
+ 1.253816878,
+ 1.291191178,
+ 0.03791617800000002,
+ 0.04903267800000011,
+ 0.03764907800000006,
+ 95.283775278,
+ 0.07470187800000005
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "18"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 19",
+ "mean": 100.16646647799999,
+ "stddev": 143.37612065560103,
+ "median": 1.117140078,
+ "user": 100.04775,
+ "system": 0.022343749999999996,
+ "min": 0.036464678000000084,
+ "max": 385.89288487799996,
+ "times": [
+ 385.89288487799996,
+ 290.359225178,
+ 0.036464678000000084,
+ 0.19590917800000007,
+ 0.046879778000000094,
+ 161.21907277800003,
+ 2.035711278,
+ 0.04454757800000009,
+ 161.635400578,
+ 0.19856887800000012
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "19"
+ }
+ },
+ {
+ "command": "python ./pytest/timing.py 20",
+ "mean": 253.70613178800005,
+ "stddev": 435.7539383326962,
+ "median": 75.73695792800001,
+ "user": 253.42871875,
+ "system": 0.047562499999999994,
+ "min": 0.0477563780000001,
+ "max": 1400.148915478,
+ "times": [
+ 420.37908587799996,
+ 0.07129847800000011,
+ 422.945836478,
+ 25.767745578000003,
+ 125.706170278,
+ 141.83330137800002,
+ 0.06695817800000003,
+ 1400.148915478,
+ 0.094249778,
+ 0.0477563780000001
+ ],
+ "exit_codes": [
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0,
+ 0
+ ],
+ "parameters": {
+ "n": "20"
+ }
+ }
+ ]
+}
diff --git a/linear_vm_flamegraph_debug.svg b/linear_vm_flamegraph_debug.svg
new file mode 100644
index 0000000..4acb1b6
--- /dev/null
+++ b/linear_vm_flamegraph_debug.svg
@@ -0,0 +1,491 @@
+
\ No newline at end of file
diff --git a/pytest/timing.py b/pytest/timing.py
index 026a507..4f8b33f 100644
--- a/pytest/timing.py
+++ b/pytest/timing.py
@@ -1,6 +1,10 @@
import adversary
+import random
import sys
+n = int(sys.argv[1])
prover = adversary.Prover(
"= (ham x) k", "= (ham y) (+ k 1)", "= ham (^ x y) p").hint_symmetric()
-bounds = prover.find_bounds(int(sys.argv[1]), 5, 8)
+k = random.randint(0, n)
+p = random.randint(0, n)
+bounds = prover.find_bounds(n, k, p)
diff --git a/time.ps1 b/time.ps1
deleted file mode 100644
index ed460fe..0000000
--- a/time.ps1
+++ /dev/null
@@ -1,2 +0,0 @@
-venv/Scripts/activate
-python test/bounds.py
diff --git a/timing_scaling.svg b/timing_scaling.svg
new file mode 100644
index 0000000..2a561b9
--- /dev/null
+++ b/timing_scaling.svg
@@ -0,0 +1,962 @@
+
+
+Qt SVG Document
+Generated with Qt
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 0
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 200
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 400
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 600
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 800
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 1000
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 1200
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 1400
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 15
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 16
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 17
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 18
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 19
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 20
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+