From a6b0ad123fa085cfb4ca7cb6f14eba3c8ac922f4 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Wed, 16 Oct 2024 14:38:40 +0100 Subject: [PATCH] Add model for `bit_decomposition` example --- .pre-commit-config.yaml | 2 +- cmd/testgen/main.go | 43 +++++ testdata/bit_decomposition.auto.accepts | 3 + testdata/bit_decomposition.auto.rejects | 240 ++++++++++++++++++++++++ 4 files changed, 287 insertions(+), 1 deletion(-) create mode 100644 testdata/bit_decomposition.auto.accepts create mode 100644 testdata/bit_decomposition.auto.rejects diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 064e2aa..3e6b8b3 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -11,7 +11,7 @@ repos: rev: v1.0.0-rc.1 hooks: - id: go-test-mod - args: [ --run=Test_ ] + args: [ --run=Test_Basic ] - repo: https://github.com/golangci/golangci-lint rev: v1.57.1 hooks: diff --git a/cmd/testgen/main.go b/cmd/testgen/main.go index 9b157de..a776f52 100644 --- a/cmd/testgen/main.go +++ b/cmd/testgen/main.go @@ -72,6 +72,7 @@ type Model struct { } var models []Model = []Model{ + {"bit_decomposition", bitDecompositionModel}, {"memory", memoryModel}, {"word_sorting", wordSortingModel}, } @@ -272,6 +273,48 @@ func wordSortingModel(schema sc.Schema, trace tr.Trace) bool { return true } +func bitDecompositionModel(schema sc.Schema, trace tr.Trace) bool { + TWO_1 := fr.NewElement(2) + TWO_2 := fr.NewElement(4) + TWO_3 := fr.NewElement(8) + TWO_4 := fr.NewElement(16) + // + NIBBLE := findColumn(0, "NIBBLE", schema, trace).Data() + BIT_0 := findColumn(0, "BIT_0", schema, trace).Data() + BIT_1 := findColumn(0, "BIT_1", schema, trace).Data() + BIT_2 := findColumn(0, "BIT_2", schema, trace).Data() + BIT_3 := findColumn(0, "BIT_3", schema, trace).Data() + // + for i := uint(0); i < NIBBLE.Len(); i++ { + NIBBLE_i := NIBBLE.Get(i) + BIT_0_i := BIT_0.Get(i) + BIT_1_i := BIT_1.Get(i) + BIT_2_i := BIT_2.Get(i) + BIT_3_i := BIT_3.Get(i) + // Check types + t_NIBBLE := NIBBLE_i.Cmp(&TWO_4) < 0 + t_BIT_0 := BIT_0_i.Cmp(&TWO_1) < 0 + t_BIT_1 := BIT_1_i.Cmp(&TWO_1) < 0 + t_BIT_2 := BIT_2_i.Cmp(&TWO_1) < 0 + t_BIT_3 := BIT_3_i.Cmp(&TWO_1) < 0 + // Check type constraints + if !(t_NIBBLE && t_BIT_0 && t_BIT_1 && t_BIT_2 && t_BIT_3) { + return false + } + // + b1 := mul(BIT_1_i, TWO_1) + b2 := mul(BIT_2_i, TWO_2) + b3 := mul(BIT_3_i, TWO_3) + sum := add(add(add(b3, b2), b1), BIT_0_i) + // Check decomposition matches + if NIBBLE_i.Cmp(&sum) != 0 { + return false + } + } + // Success + return true +} + // ============================================================================ // Helpers // ============================================================================ diff --git a/testdata/bit_decomposition.auto.accepts b/testdata/bit_decomposition.auto.accepts new file mode 100644 index 0000000..66ff12f --- /dev/null +++ b/testdata/bit_decomposition.auto.accepts @@ -0,0 +1,3 @@ +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 0]} diff --git a/testdata/bit_decomposition.auto.rejects b/testdata/bit_decomposition.auto.rejects new file mode 100644 index 0000000..df9f833 --- /dev/null +++ b/testdata/bit_decomposition.auto.rejects @@ -0,0 +1,240 @@ +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 0]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 1]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 0], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 1], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 0], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 1], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 0], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 1], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 0], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 1], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 2]} +{"NIBBLE": [0, 2], "BIT_0": [0, 2], "BIT_1": [0, 2], "BIT_2": [0, 2], "BIT_3": [0, 2]}