diff --git a/dev/bend2/DIFFERENTIAL_TESTING.md b/dev/bend2/DIFFERENTIAL_TESTING.md new file mode 100644 index 0000000000..212ac0cba7 --- /dev/null +++ b/dev/bend2/DIFFERENTIAL_TESTING.md @@ -0,0 +1,245 @@ + + +# Validating Java against a proven Bend 2 model: differential testing + +This document explains how the Bend 2 model of the Flight SQL +prepared-statement lifecycle in `prepared_statement/` is used to +validate the Java servers in `flight-sql`, what that validation does +and does not establish, and how to extend it. + +## 1. The problem it solves + +A Bend 2 model with proven laws says nothing about Java code by itself. +The laws are theorems about the Bend program `main.bend`; the checker +never sees `FlightSqlExample` or `FlightSqlClient`. To validate the +Java implementation, the model has to be connected to it. The +connection used here is differential testing: the model is the oracle +that says what a conforming server answers to every request in a +trace, and a JUnit test replays the same traces against a real server +and compares. + +The chain of trust is: + +1. **Spec sentences become laws.** `LAWS.bend` states, for every + server state and every handle, what the spec's "must" and "should" + sentences require (a closed handle never executes, a stale handle is + rejected, a created handle does execute, and so on). +2. **The model is proven to obey the laws.** `bend PROOF.bend` checks + `PROOF.bend` against `LAWS.bend` and the model. If the model + violated a law, there would be no proof and the check would fail. + This is what makes the model trustworthy as an oracle: its answers + are not hand-written expectations, they are the output of a program + that is proven to respect the spec. +3. **The model generates expectations.** `traces.bend` enumerates + request sequences, runs each through the model, and writes the + response to every request into a text file. +4. **A JUnit test replays the traces against Java.** For each trace and + each request, the test issues the real RPC and compares the + success-or-error outcome with the model's. +5. **Deviations are classified, not hidden.** Every mismatch is + bucketed by request kind and expected versus observed outcome. Each + server has a documented set of known deviations, and the test fails + if a category appears or disappears. + +## 2. The pieces + +| File | Role | +| --- | --- | +| `dev/bend2/prepared_statement/main.bend` | The model: server state, four requests, transitions, trace replay. | +| `dev/bend2/prepared_statement/LAWS.bend` | Six laws, each tied to a spec sentence or a sanity requirement. | +| `dev/bend2/prepared_statement/PROOF.bend` | Proofs of the six laws. `bend PROOF.bend` is the gate. | +| `dev/bend2/prepared_statement/traces.bend` | The trace generator. Prints the trace file. | +| `flight/flight-sql/src/test/resources/bend2/prepared_statement_traces.txt` | Generated expectations, checked in. | +| `flight/flight-sql/src/test/java/.../test/TestFlightSqlBendConformance.java` | The replayer and the known-deviation lists. | + +### 2.1 The model and its two policies + +The Flight SQL spec says a server "may return an updated handle" when +parameters are bound with `DoPut`, and that if it does, the client must +use the new handle and the server "should return an error" if the old +one is used. Both example servers in this repository are valid under +that sentence but behave differently: `FlightSqlExample` keeps the +handle, `FlightSqlStatelessExample` returns a new one that encodes the +bound parameters. + +The model therefore takes a policy flag, `rot`. Under `rot = True` a +bind retires the old handle and issues a fresh one; under `rot = False` +the handle is kept. The laws are stated for both policies where they +apply to both (close, create, freshness), for the rotating policy +where the spec sentence is about rotation (`stale_handle_rejected`), +and a sixth law, `kept_handle_executes`, pins down the keeping policy: +after a bind, the same handle still executes. + +### 2.2 The trace file + +`traces.bend` builds every sequence of one to three requests over the +alphabet `C` (create), `B0`/`B1` (bind handle 0 or 1), `E0`/`E1` +(execute), `X0`/`X1` (close), then every length-four sequence starting +with a create and every length-five sequence starting with create and +bind. That is 1085 traces and 4221 request steps. Each line holds the +actions and the expected responses under both policies: + +``` +C B0 E0 | ok0 ok1 err | ok0 ok0 ok0 +``` + +Read: create returns handle 0; bind handle 0 returns handle 1 under +rotation or 0 under keeping; execute handle 0 is then an error under +rotation (stale) and a success under keeping. The `okN` form carries +the model's handle id, which the Java side needs (next section). + +Handle ids are small naturals in the model and opaque bytes on the +wire, so the alphabet uses ids 0 and 1 and lets the traces reach ids up +to 4 through creates and rotations. Requests on ids the trace never +issued exercise the "unknown handle" paths. + +### 2.3 The replayer + +`TestFlightSqlBendConformance` starts a `FlightServer` with one of the +two example producers over Derby, opens a raw `FlightClient`, and for +each trace: + +- keeps a map from model handle id to the `ByteString` the server + actually issued; +- for `C`, calls the `CreatePreparedStatement` action with a query that + differs per create (`... AND 1 = 1`, `... AND 2 = 2`), because both + example servers use the query text as the handle and two creates of + the same text would alias; +- for `B`, runs a `DoPut` with a one-row parameter batch and reads the + `DoPutPreparedStatementResult` metadata for an updated handle; +- for `E`, calls `GetFlightInfo` with `CommandPreparedStatementQuery`; +- for `X`, calls the `ClosePreparedStatement` action; +- maps unknown ids to bytes no server has seen + (`bend2-unknown-handle-N`); +- after every successful request whose expectation is `okN`, records + the returned bytes as the real handle for id `N`, so the model's + handle bookkeeping and the server's stay aligned even when the server + rotates; +- compares only the kind of outcome, success or error, per request, + and closes every handle it created before the next trace. + +Expectations are read from the column matching the server's policy: +the stateful example is compared against the keep column, the +stateless one against the rotate column. + +### 2.4 Known deviations + +A conformance test that fails on day one is not mergeable, and a test +that silently ignores mismatches is worthless. The middle ground used +here: deviations are bucketed by category, each server carries an +explicit, commented set of known categories, and the assertion is +equality of category sets. Fixing the server makes a category +disappear and the test fail, which is the prompt to delete the entry. +A regression adds a category and fails the test. + +## 3. Results + +Run with: + +```sh +mvn -pl flight/flight-sql test -Dtest=TestFlightSqlBendConformance +``` + +| Server | Policy column | Steps compared | Deviation categories | +| --- | --- | ---: | --- | +| `FlightSqlExample` (stateful) | keep | 4221 | none | +| `FlightSqlStatelessExample` | rotate | 4221 | three, below | + +The stateless example deviates from the model in three ways, all +consequences of the same design: the handle is the query text, or a +serialised (query, parameters) pair, and the server validates nothing +against its own state. + +| Category | Count | Example | Spec sentence at stake | +| --- | ---: | --- | --- | +| `E expected err observed ok` | 229 | `C B0 E0`, step 3 | Executing the pre-bind handle succeeds; the spec says the server "should return an error". Executing a closed handle also succeeds. | +| `B expected err observed ok` | 189 | `C B0 B0`, step 3 | Binding a stale or closed handle succeeds. | +| `B expected ok observed err` | 126 | `C B0 B1`, step 3 | Binding the rotated handle fails, because the server parses the rotated bytes as SQL. The spec allows chaining a `DoPut` handle into another `DoPut`. | + +The third row is a real limitation of the example rather than a +laxness: a client that binds parameters twice against the stateless +example gets a lexical error. The first two are the example choosing +statelessness over validation, which the spec's "should" permits but +the model, taking the sentence at face value, does not. + +The stateful example's server threads log `AssertionError` during the +run. That is its `assert statementContext != null` firing on requests +with unknown handles, which is exactly the error path the model +expects; the assertion is converted into an error status for the +client. + +## 4. What this validates and what it does not + +It validates that, for every enumerated trace, each Java server answers +each request with the same success-or-error verdict as a model that is +proven to satisfy the spec's lifecycle laws, except for the documented +deviations. + +It does not validate: + +- **Traces beyond the enumeration.** The model's proofs cover all + states; the replay covers 1085 traces. Longer or differently shaped + sequences are untested unless the generator is extended. +- **Anything but the verdict.** Result schemas, row contents, error + codes and messages are not compared. The model has no notion of them. +- **Servers other than the two examples.** Running the same replayer + against another Flight SQL server is a matter of pointing the test at + it; it is not done here. +- **The client wrapper.** `FlightSqlClient.PreparedStatement` is + bypassed on purpose so that server behaviour is observed directly; + its own client-side checks (for example refusing to execute a closed + statement locally) are not under test. +- **The model's fidelity.** If the model misreads the spec, the oracle + is wrong and the proofs faithfully guarantee the wrong thing. The + laws in `LAWS.bend` quote the sentence each one encodes so that a + reviewer can check the reading. + +## 5. Extending it + +- **New laws or a changed model.** Edit `main.bend` and `LAWS.bend`, + make `bend PROOF.bend` pass again, regenerate the trace file with + `bend traces.bend > flight/flight-sql/src/test/resources/bend2/prepared_statement_traces.txt`, + and rerun the test. If the model's behaviour changed, the deviation + sets may change with it. +- **Wider traces.** Change `alphabet` or `all_traces` in `traces.bend`. + Replay time is roughly linear in steps; 4221 steps against Derby take + about eight seconds per server here. +- **Another server.** Add a test method that constructs the producer + and calls `replayAll` with the right policy column and its own known + deviations. +- **Other protocols.** The same shape works for any lifecycle the model + can express: a model with a `responses` function, a generator that + prints one line per trace, and a replayer that maps model ids to wire + values. The transactions and savepoints, IPC ordering, buffer + reference counting and PollFlightInfo proofs of concept are the + natural next candidates. + +## 6. Running Bend here + +The installer host may be unreachable; the checker runs from a clone +of the Bend repository with bun: + +```sh +git clone --depth 1 https://github.com/bendlang/bend.git /tmp/bend +cd dev/bend2/prepared_statement +bun /tmp/bend/bend2/main.ts PROOF.bend # All terms check. +bun /tmp/bend/bend2/main.ts main.bend # prints Err, then Ok(0) +bun /tmp/bend/bend2/main.ts traces.bend > ../../../flight/flight-sql/src/test/resources/bend2/prepared_statement_traces.txt +``` diff --git a/dev/bend2/README.md b/dev/bend2/README.md new file mode 100644 index 0000000000..6c0b420c45 --- /dev/null +++ b/dev/bend2/README.md @@ -0,0 +1,514 @@ + + +# Bend 2 and Apache Arrow: research notes + +Research notes on the Bend 2 programming language (released 2026-09-17) +and where it could be used around Arrow, Arrow Flight and Flight SQL. +Written against Bend 2.0.21, commit `c15a75f8` of +[bendlang/bend](https://github.com/bendlang/bend), on 2026-09-20. + +The `prepared_statement/` directory next to this file holds a small, +checked Bend 2 model of the Flight SQL prepared-statement lifecycle that +was built while writing these notes. It is the concrete evidence behind +the assessment in section 4. `DIFFERENTIAL_TESTING.md` explains how +that model is used as a test oracle for the Java servers in +`flight-sql`, which is the bridge from "the model is proven" to "the +Java is checked against it". + +## 1. Summary + +Bend 2 is a dependently typed, affine, pure functional language whose +type checker doubles as a proof checker. Its headline feature is +`LAWS.bend`: a file of properties the program must satisfy, which the +compiler re-checks against a `PROOF.bend` on every build and refuses +to compile while any law is unproven or false. It compiles one C file +per program that runs on CPU threads and on GPUs (CUDA, Metal), and it +also emits single-threaded JavaScript. + +For Arrow the realistic fit today is **executable, machine-checked +specification** of protocol semantics: the lifecycles and invariants +that the Flight and Flight SQL specs express in prose ("the server +should return an error if the client does not use the updated +handle"). The prototype in this directory states six such laws about +prepared statements, proves them, checks in 0.2 seconds, and rejects +three injected bugs. A generator turns the proven model into 1085 +request traces, and a JUnit test replays them against both example +Flight SQL servers: the stateful one matches the model on all 4221 +steps, the stateless one deviates in three documented ways. Bend has +no Java target, no stable foreign ABI, no 64-bit integers and no +float64, so it is not a candidate for production code inside +`arrow-java`, and its `LAWS.bend` mechanism cannot constrain Java code, +only Bend code; the differential test is what connects the two. + +Recommendation: treat Bend 2 as a modelling and specification tool in +the same family as TLA+ or Alloy, with the differences that its models +are proven rather than model-checked and can be compiled and run as +test oracles. Do not plan any runtime integration. Revisit if the +promised Python target or a stable FFI lands. Details in section 5. + +## 2. What Bend 2 is + +### 2.1 Origin and positioning + +Bend 2 was released on 2026-09-17 by Higher Order Company (Victor +Taelin), under Apache-2.0. It is a new language and does not accept +Bend 1 programs or the HVM runtime. The README states the goal +plainly: "an ambiguity-free language to communicate our intents to the +AIs building the world around us", where laws make intents precise and +proofs let humans verify AI output mechanically. The tagline is +"`LAWS.bend` is `AGENTS.md` backed by proof". + +The project also describes NeoGen, a program and proof synthesiser +that can fill holes in programs; it is announced material rather than a +documented, shipped command in the 2.0.21 checkout, and these notes do +not rely on it. + +### 2.2 The language in one page + +Syntax is Python-like with mandatory type annotations. Nothing is +inferred. + +```python +import Base + +type Shape is Data: + Circle{r: U32} + Square{s: U32} + +def area(s: Shape) -> U32: + match s: + case Circle{+r}: + (3 * r * r : U32) + case Square{+s}: + (s * s : U32) +``` + +The pieces that matter for specification work: + +- **Quantities.** Every variable is affine by default (used at most + once). `+x` marks a reusable value, allowed only for `Data` kinds + (constructors, numbers, lists of Data). `-x` marks an erased value + that exists only for the checker. Functions, arrays and IO handles + are `Type`-kinded and can never be copied. +- **Dependent types.** A `def` may return a `Type`, so predicates are + ordinary functions: `def Sorted(xs: List) -> Type`. Datatypes + can be indexed, which allows intrinsically typed ASTs (the + `proof_typed_eval` demo). +- **Propositions as types.** `{a == b : T}` is an equality type, + `{==}` proves it when both sides normalise to the same term, and + `%e : P` rewrites the goal with an equation. A `match` refines the + goal per case and a recursive call is the induction hypothesis. + There are no tactics and no proof search. +- **Laws.** `law name:` states a claim with `for` binders and an + optional `exs` witness; `def Laws.name(...)` in another file proves + it. `bend PROOF.bend` fails while any law is open or false and prints + `All terms check.` otherwise. Base itself uses laws for axioms such + as the handle types and the F32 operations. +- **Termination is mandatory.** Recursion must structurally decrease + on an argument, read left to right, and mutual recursion is + forbidden. A `match` may only scrutinise a parameter or a + pattern-bound variable, never a computed value; the idiom is a helper + `def` that takes the computed value as a parameter. `@unsafe` opts a + def out of the termination check and out of the proof guarantees. +- **Parallelism.** `a b = f(x) g(y)` forks two calls; `f!(x)` runs a + call on the GPU. The programmer promises the two halves are + independent and balanced. +- **Effects.** `IO(R)` with `do` blocks. Built-in effects are print, + env, time, sleep, spawn, channels, files, TCP and UDP. There is no + TLS, HTTP, JSON or regex. New effects are "foreigns": a `def` with an + `IO` return type that imports a `.c` and a `.js` implementation. + +### 2.3 Type theory and trust model + +The core, BendTT, is described in `paper/BendTT.pdf` and its abstract: +one sort with `Type : Type`, no universe hierarchy, datatypes without +a positivity restriction, and consistency recovered by the affine +usage discipline plus a wall between "live" code (runs, must +terminate) and "dead" code (types, erased arguments, equations, may +diverge but never counts as live evidence). The theory is mechanised +in `bend2/bend.lean`, but the README says the Lean formalisation and +the checker "mismatch" and "early consistency bugs may occur". The +checker (`bend2/bend.ts`) is human-written; the compiler and runtimes +(`bend2/comp.ts`) are, per the README, "99% AI-written and not fully +audited yet". The changelog shows the pace: three releases on +2026-09-19 and 2026-09-20, one of them closing a way to inhabit +`Empty` through templates (#902). + +Foreign effects are trusted invisibly: the checker accepts whatever +type the `.c`/`.js` side claims to return (bendlang/bend#874 tracks +this). Proofs therefore say nothing about code behind an FFI boundary. + +### 2.4 Runtime and targets + +BendRT emits one C file per program. A term is a 64-bit word, small +values inline and everything else a pointer into one heap shared by +every core and the GPU; there is no garbage collector, a `match` frees +the node it consumes, and only `+` values carry a reference count. +There is no C call stack: each def is a segment of a flat state +machine. Targets are C (clang only, 14+; 19+ for GPU calls), CUDA 12, +Metal and JavaScript (single core). Lua, Luau and Python are listed as +planned. No Windows, no separate compilation, and native compilation is +slow; the guide recommends the JS target for development. + +### 2.5 Tooling + +One binary: `bend file.bend` checks and runs, `-o out` builds a +native binary, `-o out.c` and `-o out.js` emit sources, `bend guide` +and `bend base` print the docs and the prelude, `--publish` pushes to +a hub whose packages are content hashes with no names, versions or +search. The LSP formats only. There is no debugger, profiler, REPL, +test framework or diagnostics. + +### 2.6 Reception in the first days + +Hacker News threads tested the `LAWS.bend` mechanic and found that it +does what it claims, and also surfaced the central weakness: an +under-specified law is satisfied by implementations that violate its +intent (the example reported was a movement scheme that preserved a +stated game law while breaking the game). Taelin agreed that writing +complete, well-scoped laws for a non-trivial system is hard. The +prototype here runs into the same issue and handles it with an +explicit anti-vacuity law (section 4.3). + +### 2.7 Stated limitations that matter here + +From the README's own list, the ones that shape the Arrow assessment: +numbers are `Nat`, `U32` and `F32` only (no U64, I64 or F64; F32 is +axiomatic and nothing about floats can be proven); strings are linked +lists of characters; Base is small and ships almost no arithmetic +lemmas (`Nat.ge_refl`, `Nat.max_ge_*`, `U32.add_comm` and the `Equal` +combinators); no type classes or macros; parallelism requires balanced +calls; one GPU and one event loop per program; the compiler has known +blind spots. + +## 3. How to use it + +### 3.1 Installing and running + +The official installer is `curl -fsSL https://bend-lang.com/install.sh | sh`. +In this sandbox that host was blocked, so the checker was run from a +clone of the repository with bun, which is exactly what the installed +binary wraps: + +```sh +git clone --depth 1 https://github.com/bendlang/bend.git +bun bend/bend2/main.ts path/to/PROOF.bend # check laws and proofs +bun bend/bend2/main.ts path/to/main.bend # check and run main +bun bend/bend2/main.ts main.bend -o out.js # JavaScript +bun bend/bend2/main.ts main.bend -o out # native, needs clang 14+ +``` + +All four were exercised on the prototype in this directory; the JS +and native builds both run and print the expected result. + +### 3.2 The intended workflow with coding agents + +The README's recipe, verbatim in spirit: add to `AGENTS.md` that the +agent must run `bend guide` to learn the language, keep the important +rules in `LAWS.bend`, and run `bend PROOF.bend` before committing. The +human writes and owns `LAWS.bend`; the agent writes `main.bend` and +`PROOF.bend`; the checker is the gate. `bend` refuses a `PROOF.bend` +that sits beside a `LAWS.bend` without importing it. + +### 3.3 What proving costs in practice + +Writing the prototype gave a feel for the effort: + +| Item | Lines | +| --- | ---: | +| Model (`main.bend`) | 181 | +| Laws (`LAWS.bend`, 6 laws) | 94 | +| Proofs (`PROOF.bend`) | 298 | +| Trace generator (`traces.bend`) | 212 | + +Roughly two lines of proof per line of model, for a model whose +invariant is a simple list bound. Most of the proof file is generic +plumbing that Base does not provide: splitting and joining `T(a && b)`, +`n < n + 1`, monotonicity of `<`, soundness of `Nat.is_eq`, and the +"inspect" idiom of passing a computed Boolean plus an equation about +it into a helper so that it can be matched. The checker ran the whole +thing in 0.2 seconds wall time, which does match the project's claim +that checking is fast. + +Two frictions recur. Constructor names are global, so `Close{}` and +`Ok{}` collide with Base and everything needs a prefix. And proofs are +brittle: changing an implementation detail that does not affect a +law's truth (the exact shape of a state) still breaks proofs that +mention that shape, and the failure is reported at the proof, not as +"law is false". An agent would then have to re-prove rather than fix +code, and it needs to tell those two situations apart. + +## 4. Prototype: a Flight SQL prepared-statement model + +### 4.1 What is modelled + +The Flight SQL spec describes prepared statements as: create a handle +with `CreatePreparedStatement`; bind parameters with `DoPut`, after +which the server "may return an updated handle" that the client must +use from then on; execute with `GetFlightInfo`; close with +`ClosePreparedStatement`. On the handle-rotation rule the spec says: +"The server is responsible for detecting the case where the client +does not use the updated handle and should return an error." The Java +client implements the client side of this in +`FlightSqlClient.PreparedStatement.execute`, which adopts the handle +returned in `DoPutPreparedStatementResult` when it is non-empty, and +`FlightSqlStatelessExample` implements a server that encodes the query +and bound parameters into the rotated handle. + +`main.bend` models the server as a list of live handles plus a +counter, with four requests (`ACreate`, `ABind`, `AExec`, `AClose`) +and two responses (`ROk{h}`, `RErr`). The spec says a server "may +return an updated handle" on bind, so the model takes a policy flag: +under the rotating policy `ABind` on a live handle retires it and +issues the counter as the new handle, under the keeping policy the +handle stays. `replay` runs a trace and `responses` lists every answer. + +### 4.2 The laws + +`LAWS.bend` states six laws over arbitrary server states: + +1. `closed_never_executes`: after `AClose{h}`, `AExec{h}` answers + `RErr`, under either policy. +2. `created_handle_executes`: the handle returned by `ACreate` executes + with `ROk`. This is the anti-vacuity law; without it a server that + rejects every request satisfies law 1. +3. `stale_handle_rejected`: under the rotating policy, after `ABind{h}` + rotates the handle, `AExec{h}` on the old handle answers `RErr`. + This is the spec sentence quoted above. +4. `kept_handle_executes`: under the keeping policy, after `ABind{h}` + on a live handle, `AExec{h}` still answers `ROk{h}`. +5. `fresh_start` and 6. `fresh_kept`: the initial state is fresh (all + live handles are below the counter) and every request preserves + freshness under either policy. Law 3 is stated for fresh states, and + laws 5 and 6 show every reachable state is fresh, so together they + cover every trace. + +### 4.3 Results + +`bend PROOF.bend` prints `All terms check.` in 0.22 seconds. Three +mutations of `main.bend` were then tried, each restored afterwards: + +| Mutation | Spec bug it corresponds to | Result | +| --- | --- | --- | +| `ABind` keeps the old handle live | Server accepts a stale handle | Rejected at `fresh_kept`'s bind case | +| `AClose` does not remove the handle | Closed statement still executes | Rejected at `closed_never_executes` | +| `ACreate` does not advance the counter | Handles reissued | Rejected at `created_handle_executes` | + +The third row illustrates the brittleness noted in 3.3: the mutation +genuinely breaks `fresh_kept` (the new handle is not below an +unchanged counter), but the first failure the checker reports is in a +proof whose rewrite spelled out `1n+next`. Both readings lead to "the +build is blocked", which is the property `LAWS.bend` promises; the +diagnosis of why is left to the human or agent. + +The model compiles to a 16 KB JavaScript file and a 1.1 MB native +binary, both of which run the sample trace (create, bind, execute the +pre-bind handle) and print `Err` for the rotating policy and `Ok(0)` +for the keeping one. + +### 4.4 From model to Java: the differential test + +`traces.bend` enumerates 1085 request sequences, runs each through the +proven model under both policies, and prints the expected response to +every request. The file is checked in under +`flight/flight-sql/src/test/resources/bend2/` and +`TestFlightSqlBendConformance` replays every trace against the two +example servers through the raw Flight client: + +| Server | Steps compared | Deviations from the model | +| --- | ---: | --- | +| `FlightSqlExample` (keeps handles) | 4221 | none | +| `FlightSqlStatelessExample` (rotates handles) | 4221 | executes and binds stale or closed handles; cannot bind a rotated handle again | + +The stateless deviations are the example encoding the query into the +handle and validating nothing server-side. They are recorded as a +known-deviation set in the test, so the test passes today and fails +the day the example is fixed or regresses further. `DIFFERENTIAL_TESTING.md` +documents the design, the chain of trust and the limits. + +## 5. Where Bend 2 could fit around Arrow + +### 5.1 Executable protocol specifications (good fit) + +Flight and Flight SQL carry a lot of lifecycle semantics in prose: +prepared-statement handle rotation, transactions and savepoints +(`ActionBeginTransaction`, `ActionEndSavepoint` with release or +rollback, statements that may or may not carry a `transaction_id`), +`PollFlightInfo` (reuse the returned descriptor, `progress` in +`[0, 1]`, expiration, cancel via `CancelFlightInfo`), endpoint +expiration and `RenewFlightEndpoint`, session options +(`SetSessionOptions` "may require these options be set exactly once +and prior to any other activity"), and the `ordered` flag on +`FlightInfo`. Each of these is a small state machine with a handful of +"must" and "should" sentences, which is exactly what the prototype +shows Bend can state as laws and prove in minutes of checker time. + +Value for Arrow: a machine-checked reference of what a conforming +server does, next to the `.proto` and `.rst` files. It would settle +questions such as the one in apache/arrow#37720 (stateless prepared +statements with parameters) by making the intended state transitions +explicit and checked. This is comparable to writing a TLA+ spec, with +two practical differences: the proof is total rather than bounded by a +model checker, and the model compiles to JS or C so it can be run. + +Cost: the proofs are hand-written, and the first model of each area +pays for its own lemma library. Expect the proof to be two to three +times the size of the model, as in section 3.3. + +### 5.2 Test oracles for the Java implementation (done for prepared statements) + +A differential test generates request traces, runs them through the +proven model to get the expected responses, and replays them against a +real server, comparing the success-or-error outcome per step. This is +implemented for the prepared-statement model (section 4.4 and +`DIFFERENTIAL_TESTING.md`): the generator is written in Bend and its +output is committed as a text resource, so the Java build needs no +Bend or node toolchain. The oracle is only as good as the model, which +is why every law quotes the spec sentence it encodes, but it turns the +prose rules into a regression test and it found three ways the +stateless example departs from them. + +### 5.3 Columnar and IPC structural invariants (feasible, expensive) + +The columnar spec has invariants that are natural laws: offsets have +`length + 1` entries and are monotonically non-decreasing; run-end +arrays have strictly increasing positive run ends; `null_count` +matches the validity bitmap; every buffer is padded to 8 bytes; an +encapsulated IPC message is `0xFFFFFFFF`, an int32 metadata length, +the flatbuffer, padding to 8 bytes and a body whose total is a multiple +of 8 (`MessageSerializer` enforces this with `checkArgument` calls); +streams put the schema first and define a dictionary before a batch +uses it. + +These can be modelled, but the arithmetic ones are costly today: Base +ships no lemmas about `Nat.mod`, `Nat.div` or multiplication, so a +proof that a padded length is a multiple of 8 means building that +theory first, and there is no 64-bit integer type, so `int64` lengths +and offsets become `Nat`. A round-trip law for the message prefix +(`decode(encode(m)) == m`) needs little-endian byte splitting and the +same divmod lemmas. The list-shaped invariants (offsets monotonic, +dictionaries defined before use, schema first) are cheap and look like +the prototype. Value is moderate: these invariants are already checked +at runtime by every implementation, and the spec prose is precise. + +### 5.4 Verified reference implementations (not now) + +Compiling a verified Bend routine and calling it from `arrow-java` is +not practical. There is no Java or JVM target. The C output is one +whole program with its own heap and flat state machine, not a library +with a stable ABI: the effects guide says outright there is "no ABI +promise" and effects must be rebuilt with every compiler release. +Values live as 64-bit words in Bend's heap, so Arrow buffers would be +copied and re-encoded on the way in and out, and strings are linked +lists. A Panama or JNI bridge would be fighting the runtime. + +### 5.5 GPU kernels over Arrow data (not a fit) + +Bend's parallelism is real but shaped for divide-and-conquer over its +own data structures, with arrays limited to power-of-two sizes and +balanced forks. Arrow's columnar buffers would have to be marshalled +into that heap, and `arrow-java` has no GPU story to plug into. Where +GPU work on Arrow data is wanted, existing Arrow-native engines are the +comparison, and Bend does not offer zero-copy against the C Data +Interface. + +### 5.6 Governing AI-written Java (not applicable) + +`LAWS.bend` constrains Bend code only. It cannot state or enforce +anything about `FlightSqlProducer` implementations written in Java. +The useful transfer is indirect: a Bend model pins down what the Java +code should do, and section 5.2 turns that into tests. + +## 6. Risks and open questions + +- **Maturity.** Three days old at time of writing, releases daily, + a consistency fix in the newest one, the compiler unaudited, the + Lean model behind the checker. Fine for specification work whose + output is understanding and tests; not fine for anything that ships. +- **Trusted computing base.** Proofs are checked by `bend.ts`, which + is not the formalised kernel. Anything behind a foreign effect is + trusted on its declared type. +- **Under-specified laws.** A law can be true of the wrong program. + Every law set needs positive (liveness-style) laws next to the + negative ones, as the prototype's `created_handle_executes` shows. +- **No 64-bit integers or float64.** Arrow is full of both. Models + must abstract them to `Nat`, which is fine for semantics and wrong + for overflow behaviour. +- **Proof brittleness without tactics.** Refactoring a model breaks + proofs even when laws still hold. Budget for re-proving. +- **Network egress.** The docs site (`bend-lang.com`, `bend2.dev`) was + unreachable from this environment; the GitHub repository carried + everything needed, including the guide (`bend guide` prints it). + +## 7. Suggested next steps + +1. Extend the prototype with transactions and savepoints + (`ActionBeginTransaction`, `ActionBeginSavepoint`, + `ActionEndTransaction`, `ActionEndSavepoint`) and with statements + that carry a `transaction_id`, and state the legality of each + action per state as laws. +2. Model `PollFlightInfo` (descriptor reuse, monotone progress, + expiration, cancel) the same way. +3. Give each new model a `responses` function and a trace generator, + and add a replayer test as in `DIFFERENTIAL_TESTING.md`, so every + model validates the Java servers rather than only itself. +4. Decide whether the stateless example should be fixed to reject + stale and closed handles and to accept a rotated handle on a second + bind; the conformance test's known-deviation set is the checklist. +5. Revisit runtime integration only if a Python or JVM target or a + stable FFI appears in the Bend changelog. + +## 8. Sources + +Primary, read directly: + +- Bend repository, README, `guide/GUIDE.md`, `guide/EFFECTS.md`, + `WONTFIX.txt`, `AGENTS.md`, `CHANGELOG.md`, `bend2/base.bend`, + paper abstracts in `bend2/docs/BendTT` and `bend2/docs/BendRT`, + demos `proof_insertion_sort`, `proof_typed_eval`, + `app_win_is_bug_2d`, `io_tcp_echos`, `io_http_server`: + https://github.com/bendlang/bend (commit c15a75f8, 2026-09-20) +- Foreign effects trusted on declared type: https://github.com/bendlang/bend/issues/874 +- Apache Arrow format docs, Flight, Flight SQL and Columnar: + https://github.com/apache/arrow/tree/main/docs/source/format +- Stateless prepared statements with parameters: https://github.com/apache/arrow/issues/37720 +- This repository: `arrow-format/Flight.proto`, `arrow-format/FlightSql.proto`, + `flight/flight-sql/.../FlightSqlClient.java`, + `flight/flight-sql/.../FlightSqlProducer.java`, + `flight/flight-sql/src/test/.../FlightSqlStatelessExample.java`, + `vector/.../ipc/message/MessageSerializer.java` + +Secondary, via search results (the sites themselves were not reachable +from this environment, so figures quoted from them are vendor claims): + +- Bend 2 launch coverage and Hacker News discussion of under-specified + laws: https://news.ycombinator.com/item?id=49746163 and + https://news.ycombinator.com/item?id=49753179 +- bend2.dev notes ("What is Bend2?", "Bend2 vs Lean", reporting a + checker benchmark of 0.295 s for Bend against 36.177 s for Lean on a + 12,800-definition fixture): https://bend2.dev/notes/what-is-bend2/ + and https://bend2.dev/notes/bend2-vs-lean/ +- Taelin's launch and NeoGen posts: https://x.com/VictorTaelin/status/2100681226143092875 + and https://x.com/VictorTaelin/status/1957775213053022614 +- Higher Order Company fundraising page (older material; lists + Python, JavaScript and Go export, which the release does not): + https://wefunder.com/higherorderco/ +- Vow language issue proposing an audit of Bend 2's verification model: + https://github.com/vow-lang/vow/issues/1298 diff --git a/dev/bend2/prepared_statement/LAWS.bend b/dev/bend2/prepared_statement/LAWS.bend new file mode 100644 index 0000000000..0dca14da6a --- /dev/null +++ b/dev/bend2/prepared_statement/LAWS.bend @@ -0,0 +1,94 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# The laws of the prepared-statement model. The human states them; +# PROOF.bend must prove them. Each law is a sentence from the Flight +# SQL spec, or a sanity check that keeps the others from being +# satisfied vacuously. + +import Base +import ./main.bend as PS + +# the truth of a Bool as a type: Unit when True, Empty when False +def T(b: Bool) -> Data: + match b: + case True{}: + Unit + case False{}: + Empty + +# every live handle is below the counter, so no handle is ever reissued +def Fresh(live: List<&2, Nat>, +next: Nat) -> Data: + T(PS.all_lt(live, next)) + +def Fresh_s(s: PS.Server) -> Data: + PS.Server{live, next} = s + Fresh(live, next) + +# LAW: "Closes server resources associated with the prepared statement +# handle." Once a handle is closed, executing it is an error, from any +# server state and under either bind policy. +law closed_never_executes: + for +h : Nat + for +live : List<&2, Nat> + for +next : Nat + for rot : Bool + {PS.resp(PS.step_s(PS.AExec{h}, PS.state(PS.step(PS.AClose{h}, live, next, rot)), rot)) == PS.RErr{} : PS.Resp} + +# LAW (anti-vacuity): a server that rejects everything satisfies the law +# above. This one rules that out: the handle a Create returns executes. +law created_handle_executes: + for +live : List<&2, Nat> + for +next : Nat + for rot : Bool + {PS.resp(PS.step_s(PS.AExec{next}, PS.state(PS.step(PS.ACreate{}, live, next, rot)), rot)) == PS.ROk{next} : PS.Resp} + +# LAW: "The server is responsible for detecting the case where the +# client does not use the updated handle and should return an error." +# Under the rotating policy, after a bind rotates h, executing the +# stale h is an error. This needs the freshness invariant, so it is +# stated for fresh states only, and the two laws below show every +# reachable state is fresh. +law stale_handle_rejected: + for +h : Nat + for +live : List<&2, Nat> + for +next : Nat + for w : Fresh(live, next) + {PS.resp(PS.step_s(PS.AExec{h}, PS.state(PS.step(PS.ABind{h}, live, next, True{})), True{})) == PS.RErr{} : PS.Resp} + +# LAW: a server that does not return an updated handle keeps the bound +# handle valid: under the keeping policy, after a bind of a live h, +# executing h succeeds. +law kept_handle_executes: + for +h : Nat + for +live : List<&2, Nat> + for +next : Nat + for hw : T(PS.has(h, live)) + {PS.resp(PS.step_s(PS.AExec{h}, PS.state(PS.step(PS.ABind{h}, live, next, False{})), False{})) == PS.ROk{h} : PS.Resp} + +# LAW: the initial state is fresh +law fresh_start: + Fresh_s(PS.start()) + +# LAW: every request keeps the state fresh, under either policy +law fresh_kept: + for a : PS.Act + for +live : List<&2, Nat> + for +next : Nat + for rot : Bool + for w : Fresh(live, next) + Fresh_s(PS.state(PS.step(a, live, next, rot))) diff --git a/dev/bend2/prepared_statement/PROOF.bend b/dev/bend2/prepared_statement/PROOF.bend new file mode 100644 index 0000000000..d7147476e9 --- /dev/null +++ b/dev/bend2/prepared_statement/PROOF.bend @@ -0,0 +1,298 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# The proofs. Imports the model (as PS) and the claims (as Laws) and +# fills every law they state; `bend PROOF.bend` is the whole check. + +import Base +import ./main.bend as PS +import ./LAWS.bend as Laws + +# Lemmas on has and remove +# ------------------------ + +# removing h leaves no h: the step case, with the verdict c of +# Nat.is_eq(x, h) as a parameter, since a computed value cannot be +# matched in place +def has_remove.fin(+h: Nat, +x: Nat, -t: List<&2, Nat>, + rec: {False{} == PS.has(h, PS.remove(h, t)) : Bool}, + c: Bool, e: {c == Nat.is_eq(x, h) : Bool}) + -> {False{} == PS.has(h, PS.put(x, PS.remove(h, t), c)) : Bool}: + match c: + case True{}: + rec + case False{}: + %e : {False{} == (_ || PS.has(h, PS.remove(h, t))) : Bool} + rec + +def has_remove(+h: Nat, xs: List<&2, Nat>) -> {False{} == PS.has(h, PS.remove(h, xs)) : Bool}: + match xs: + case Nil{}: + {==} + case Con{+x, t}: + has_remove.fin(h, x, t, has_remove(h, t), Nat.is_eq(x, h), {==}) + +# a nat equals itself +def eq_refl(n: Nat) -> {True{} == Nat.is_eq(n, n) : Bool}: + match n: + case 0n: + {==} + case 1n+p: + eq_refl(p) + +# Laws +# ---- + +def Laws.closed_never_executes(h, live, next, rot): + %has_remove(h, live) : {PS.resp(PS.exec(h, PS.remove(h, live), next, _)) == PS.RErr{} : PS.Resp} + {==} + +def Laws.created_handle_executes(live, next, rot): + %eq_refl(next) : {PS.resp(PS.exec(next, next <> live, 1n+next, (_ || PS.has(next, live)))) == PS.ROk{next} : PS.Resp} + {==} + +# Proof kit +# --------- + +# T(True{}) from an equation +def true_T(b: Bool, e: {True{} == b : Bool}) -> Laws.T(b): + %e : Laws.T(_) + Unit{} + +def disc(b: Bool) -> Type: + match b: + case True{}: + Unit + case False{}: + Empty + +# True and False clash +def true_ne_false(e: {True{} == False{} : Bool}) -> Empty: + %e : disc(_) + Unit{} + +def ndisc(b: Bool) -> Type: + match b: + case True{}: + Empty + case False{}: + Unit + +# T(b) with b known False is Empty +def false_T(b: Bool, e: {False{} == b : Bool}, w: Laws.T(b)) -> Empty: + match b: + case True{}: + %e : ndisc(_) + Unit{} + case False{}: + w + +# T(c && b) splits into T(c) and T(b); c is a parameter so it can be matched +def split.fin(c: Bool, -b: Bool, w: Laws.T(c && b), -P: Type, k: Laws.T(c) -> Laws.T(b) -> P) -> P: + match c: + case True{}: + k(Unit{}, w) + case False{}: + Empty.absurd(P, w) + +# T(c) and T(b) join into T(c && b) +def join.fin(c: Bool, -b: Bool, wc: Laws.T(c), wb: Laws.T(b)) -> Laws.T(c && b): + match c: + case True{}: + wb + case False{}: + Empty.absurd(Laws.T(False{} && b), wc) + +# Lemmas on Nat +# ------------- + +# n < n + 1 +def lt_succ(n: Nat) -> Laws.T(Nat.is_lt(n, 1n+n)): + match n: + case 0n: + Unit{} + case 1n+p: + lt_succ(p) + +# x < n implies x < n + 1 +def lt_mono(x: Nat, n: Nat, w: Laws.T(Nat.is_lt(x, n))) -> Laws.T(Nat.is_lt(x, 1n+n)): + match x n: + case 0n 0n: + Empty.absurd(Laws.T(Nat.is_lt(0n, 1n)), w) + case 0n 1n+q: + Unit{} + case 1n+p 0n: + Empty.absurd(Laws.T(Nat.is_lt(1n+p, 1n)), w) + case 1n+p 1n+q: + lt_mono(p, q, w) + +# a true Nat.is_eq is an equality +def eq_sound(x: Nat, h: Nat, e: {True{} == Nat.is_eq(x, h) : Bool}) -> {x == h : Nat}: + match x h: + case 0n 0n: + {==} + case 0n 1n+q: + Empty.absurd({0n == 1n+q : Nat}, true_ne_false(e)) + case 1n+p 0n: + Empty.absurd({1n+p == 0n : Nat}, true_ne_false(e)) + case 1n+p 1n+q: + %eq_sound(p, q, e) : {1n+p == 1n+_ : Nat} + {==} + +# h < n implies n != h +def lt_ne(h: Nat, n: Nat, w: Laws.T(Nat.is_lt(h, n))) -> {False{} == Nat.is_eq(n, h) : Bool}: + match h n: + case 0n 0n: + Empty.absurd({False{} == Nat.is_eq(0n, 0n) : Bool}, w) + case 0n 1n+q: + {==} + case 1n+p 0n: + Empty.absurd({False{} == Nat.is_eq(0n, 1n+p) : Bool}, w) + case 1n+p 1n+q: + lt_ne(p, q, w) + +# Lemmas on all_lt +# ---------------- + +# a bound below n is a bound below n + 1 +def mono(xs: List<&2, Nat>, +n: Nat, w: Laws.T(PS.all_lt(xs, n))) -> Laws.T(PS.all_lt(xs, 1n+n)): + match xs: + case Nil{}: + Unit{} + case Con{+x, +t}: + split.fin(Nat.is_lt(x, n), PS.all_lt(t, n), w, Laws.T(PS.all_lt(x <> t, 1n+n)), + wx => wt => join.fin(Nat.is_lt(x, 1n+n), PS.all_lt(t, 1n+n), lt_mono(x, n, wx), mono(t, n, wt))) + +# removing keeps a bound: the step case, over the verdict c of the removal +def remove_lt.fin(c: Bool, +x: Nat, -r: List<&2, Nat>, +n: Nat, wx: Laws.T(Nat.is_lt(x, n)), wr: Laws.T(PS.all_lt(r, n))) + -> Laws.T(PS.all_lt(PS.put(x, r, c), n)): + match c: + case True{}: + wr + case False{}: + join.fin(Nat.is_lt(x, n), PS.all_lt(r, n), wx, wr) + +def remove_lt(+h: Nat, xs: List<&2, Nat>, +n: Nat, w: Laws.T(PS.all_lt(xs, n))) -> Laws.T(PS.all_lt(PS.remove(h, xs), n)): + match xs: + case Nil{}: + Unit{} + case Con{+x, +t}: + split.fin(Nat.is_lt(x, n), PS.all_lt(t, n), w, Laws.T(PS.all_lt(PS.remove(h, x <> t), n)), + wx => wt => remove_lt.fin(Nat.is_eq(x, h), x, PS.remove(h, t), n, wx, remove_lt(h, t, n, wt))) + +# a live handle is below the bound: the step case, over the verdict c +# of Nat.is_eq(x, h); rec is the induction hypothesis on the tail +def has_lt.fin(+h: Nat, +x: Nat, -t: List<&2, Nat>, +n: Nat, + rec: Laws.T(PS.has(h, t)) -> Laws.T(PS.all_lt(t, n)) -> Laws.T(Nat.is_lt(h, n)), + c: Bool, e: {c == Nat.is_eq(x, h) : Bool}, hw: Laws.T(c || PS.has(h, t)), w: Laws.T(PS.all_lt(x <> t, n))) + -> Laws.T(Nat.is_lt(h, n)): + match c: + case True{}: + split.fin(Nat.is_lt(x, n), PS.all_lt(t, n), w, Laws.T(Nat.is_lt(h, n)), + wx => wt => + %eq_sound(x, h, e) : Laws.T(Nat.is_lt(_, n)) + wx) + case False{}: + split.fin(Nat.is_lt(x, n), PS.all_lt(t, n), w, Laws.T(Nat.is_lt(h, n)), + wx => wt => rec(hw, wt)) + +def has_lt(+h: Nat, xs: List<&2, Nat>, +n: Nat) -> Laws.T(PS.has(h, xs)) -> Laws.T(PS.all_lt(xs, n)) -> Laws.T(Nat.is_lt(h, n)): + match xs: + case Nil{}: + hw => w => Empty.absurd(Laws.T(Nat.is_lt(h, n)), hw) + case Con{+x, +t}: + hw => w => has_lt.fin(h, x, t, n, has_lt(h, t, n), Nat.is_eq(x, h), {==}, hw, w) + +# Invariant laws +# -------------- + +def Laws.fresh_start(): + Unit{} + +# the Bind arm on a live handle, over the policy rot +def kept_bind.ok(rot: Bool, +h: Nat, +live: List<&2, Nat>, +next: Nat, w: Laws.Fresh(live, next)) + -> Laws.Fresh_s(PS.state(PS.bind.ok(h, live, next, rot))): + match rot: + case True{}: + join.fin(Nat.is_lt(next, 1n+next), PS.all_lt(PS.remove(h, live), 1n+next), + lt_succ(next), mono(PS.remove(h, live), next, remove_lt(h, live, next, w))) + case False{}: + w + +# the Bind arm, over the verdict c of has(h, live) +def kept_bind.fin(c: Bool, rot: Bool, +h: Nat, +live: List<&2, Nat>, +next: Nat, w: Laws.Fresh(live, next)) + -> Laws.Fresh_s(PS.state(PS.bind(h, live, next, rot, c))): + match c: + case True{}: + kept_bind.ok(rot, h, live, next, w) + case False{}: + w + +# the Exec arm: the state is unchanged either way +def kept_exec.fin(c: Bool, +h: Nat, +live: List<&2, Nat>, +next: Nat, w: Laws.Fresh(live, next)) + -> Laws.Fresh_s(PS.state(PS.exec(h, live, next, c))): + match c: + case True{}: + w + case False{}: + w + +def Laws.fresh_kept(a, live, next, rot, w): + match a: + case PS.ACreate{}: + join.fin(Nat.is_lt(next, 1n+next), PS.all_lt(live, 1n+next), lt_succ(next), mono(live, next, w)) + case PS.ABind{+h}: + kept_bind.fin(PS.has(h, live), rot, h, live, next, w) + case PS.AExec{+h}: + kept_exec.fin(PS.has(h, live), h, live, next, w) + case PS.AClose{+h}: + remove_lt(h, live, next, w) + +# Stale handles +# ------------- + +# over the verdict c of has(h, live), with its equation +def stale.fin(+h: Nat, +live: List<&2, Nat>, +next: Nat, c: Bool, e: {c == PS.has(h, live) : Bool}, w: Laws.Fresh(live, next)) + -> {PS.resp(PS.step_s(PS.AExec{h}, PS.state(PS.bind(h, live, next, True{}, c)), True{})) == PS.RErr{} : PS.Resp}: + match c: + case True{}: + ne = lt_ne(h, next, has_lt(h, live, next)(true_T(PS.has(h, live), e), w)) + %has_remove(h, live) : {PS.resp(PS.exec(h, next <> PS.remove(h, live), 1n+next, (Nat.is_eq(next, h) || _))) == PS.RErr{} : PS.Resp} + %ne : {PS.resp(PS.exec(h, next <> PS.remove(h, live), 1n+next, (_ || False{}))) == PS.RErr{} : PS.Resp} + {==} + case False{}: + %e : {PS.resp(PS.exec(h, live, next, _)) == PS.RErr{} : PS.Resp} + {==} + +def Laws.stale_handle_rejected(h, live, next, w): + stale.fin(h, live, next, PS.has(h, live), {==}, w) + +# Kept handles +# ------------ + +# over the verdict c of has(h, live), with its equation +def kept.fin(+h: Nat, +live: List<&2, Nat>, +next: Nat, c: Bool, e: {c == PS.has(h, live) : Bool}, hw: Laws.T(PS.has(h, live))) + -> {PS.resp(PS.step_s(PS.AExec{h}, PS.state(PS.bind(h, live, next, False{}, c)), False{})) == PS.ROk{h} : PS.Resp}: + match c: + case True{}: + %e : {PS.resp(PS.exec(h, live, next, _)) == PS.ROk{h} : PS.Resp} + {==} + case False{}: + Empty.absurd({PS.resp(PS.exec(h, live, next, PS.has(h, live))) == PS.ROk{h} : PS.Resp}, false_T(PS.has(h, live), e, hw)) + +def Laws.kept_handle_executes(h, live, next, hw): + kept.fin(h, live, next, PS.has(h, live), {==}, hw) diff --git a/dev/bend2/prepared_statement/main.bend b/dev/bend2/prepared_statement/main.bend new file mode 100644 index 0000000000..3f94ad2978 --- /dev/null +++ b/dev/bend2/prepared_statement/main.bend @@ -0,0 +1,181 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# A model of the Arrow Flight SQL prepared-statement lifecycle, written +# in Bend 2 to see what its laws and proofs cost on a protocol shaped +# like Flight SQL. Handles are Nats issued by a counter; the server +# keeps the list of live handles. The spec says a server "may return an +# updated handle" when parameters are bound (DoPut), and the client must +# use it afterwards; the policy flag `rot` picks that stateless style +# (True) or the stateful one that keeps the handle (False). +# +# bend main.bend # checks the model and runs the sample trace in main +# bend PROOF.bend # checks LAWS.bend against this model + +import Base + +# Protocol +# -------- + +# one client request, by Flight SQL RPC +type Act is Data: + ACreate{} # DoAction CreatePreparedStatement + ABind{h: Nat} # DoPut CommandPreparedStatementQuery (bind parameters) + AExec{h: Nat} # GetFlightInfo CommandPreparedStatementQuery (execute) + AClose{h: Nat} # DoAction ClosePreparedStatement + +# the server's answer: the handle to use next, or an error status +type Resp is Data: + ROk{h: Nat} + RErr{} + +# server state: the live handles, and the next handle to issue +type Server is Data: + Server{live: List<&2, Nat>, next: Nat} + +# List helpers +# ------------ + +# keep x unless drop +def put(x: Nat, r: List<&2, Nat>, drop: Bool) -> List<&2, Nat>: + match drop: + case True{}: + r + case False{}: + x <> r + +# xs without every occurrence of h +def remove(+h: Nat, xs: List<&2, Nat>) -> List<&2, Nat>: + match xs: + case Nil{}: + Nil{} + case Con{+x, t}: + put(x, remove(h, t), Nat.is_eq(x, h)) + +# whether h occurs in xs +def has(+h: Nat, xs: List<&2, Nat>) -> Bool: + match xs: + case Nil{}: + False{} + case x <> t: + Nat.is_eq(x, h) || has(h, t) + +# whether every handle in xs is below n +def all_lt(xs: List<&2, Nat>, +n: Nat) -> Bool: + match xs: + case Nil{}: + True{} + case Con{x, t}: + Nat.is_lt(x, n) && all_lt(t, n) + +# Transitions +# ----------- + +# Exec: answer Ok on a live handle, Err otherwise; the state is unchanged +def exec(+h: Nat, live: List<&2, Nat>, +next: Nat, ok: Bool) -> Server & Resp: + match ok: + case True{}: + (Server{live, next}, ROk{h}) + case False{}: + (Server{live, next}, RErr{}) + +# Bind on a live handle: rotate it (retire h, issue next) or keep it +def bind.ok(+h: Nat, +live: List<&2, Nat>, +next: Nat, rot: Bool) -> Server & Resp: + match rot: + case True{}: + (Server{next <> remove(h, live), 1n+next}, ROk{next}) + case False{}: + (Server{live, next}, ROk{h}) + +# Bind: on a live handle follow the policy; else Err +def bind(+h: Nat, +live: List<&2, Nat>, +next: Nat, rot: Bool, ok: Bool) -> Server & Resp: + match ok: + case True{}: + bind.ok(h, live, next, rot) + case False{}: + (Server{live, next}, RErr{}) + +# one request against one state, under the bind policy rot +def step(a: Act, +live: List<&2, Nat>, +next: Nat, rot: Bool) -> Server & Resp: + match a: + case ACreate{}: + (Server{next <> live, 1n+next}, ROk{next}) + case ABind{+h}: + bind(h, live, next, rot, has(h, live)) + case AExec{+h}: + exec(h, live, next, has(h, live)) + case AClose{+h}: + (Server{remove(h, live), next}, ROk{h}) + +# projections of a step +def state(sr: Server & Resp) -> Server: + (s, r) = sr + s + +def resp(sr: Server & Resp) -> Resp: + (s, r) = sr + r + +# a request against a whole server +def step_s(a: Act, s: Server, rot: Bool) -> Server & Resp: + Server{live, next} = s + step(a, live, next, rot) + +def start() -> Server: + Server{Nil{}, 0n} + +# a whole trace, threading the state and the last response +def run(acts: List, sr: Server & Resp, +rot: Bool) -> Server & Resp: + match acts: + case Nil{}: + sr + case a <> rest: + (s, last) = sr + run(rest, step_s(a, s, rot), rot) + +def replay(acts: List, +rot: Bool) -> Server & Resp: + run(acts, (start(), RErr{}), rot) + +# the response of one step, followed by the rest of the trace +def emit(sr: Server & Resp, rec: Server -> List<&2, Resp>) -> List<&2, Resp>: + (s, r) = sr + r <> rec(s) + +# every response of a trace, in order, as a function of the start state +def responses(acts: List<&2, Act>, +rot: Bool) -> Server -> List<&2, Resp>: + match acts: + case Nil{}: + s => Nil{} + case a <> rest: + s => emit(step_s(a, s, rot), responses(rest, rot)) + +# Show +# ---- + +def Resp.show(r: Resp) -> String: + match r: + case ROk{h}: + "Ok(" ++ Nat.show(h) ++ ")" + case RErr{}: + "Err" + +# create, bind, execute the pre-bind handle 0: Err when the bind +# rotated the handle (stateless server), Ok(0) when it kept it +def main() -> IO(Unit): + do IO: + IO.print(Resp.show(resp(replay([ACreate{}, ABind{0n}, AExec{0n}], True{})))) + IO.print(Resp.show(resp(replay([ACreate{}, ABind{0n}, AExec{0n}], False{})))) diff --git a/dev/bend2/prepared_statement/traces.bend b/dev/bend2/prepared_statement/traces.bend new file mode 100644 index 0000000000..da3b51f38e --- /dev/null +++ b/dev/bend2/prepared_statement/traces.bend @@ -0,0 +1,212 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. + +# The trace generator: enumerates client request sequences over two +# handle ids, runs each through the proven model under both bind +# policies, and prints one line per trace: +# +# C B0 E0 | ok0 ok1 err | ok0 ok0 ok0 +# +# actions, then the expected responses under the rotating policy, then +# under the keeping policy. `okN` carries the handle id the model +# returned, which the Java test uses to map model ids to real handles. +# +# bend traces.bend > ../../../flight/flight-sql/src/test/resources/bend2/prepared_statement_traces.txt + +import Base +import ./main.bend as PS + +# Alphabet +# -------- + +# the actions a trace is built from +def alphabet() -> List<&2, PS.Act>: + [PS.ACreate{}, PS.ABind{0n}, PS.ABind{1n}, PS.AExec{0n}, PS.AExec{1n}, PS.AClose{0n}, PS.AClose{1n}] + +def is_create(a: PS.Act) -> Bool: + match a: + case PS.ACreate{}: + True{} + case PS.ABind{h}: + False{} + case PS.AExec{h}: + False{} + case PS.AClose{h}: + False{} + +def is_bind0(a: PS.Act) -> Bool: + match a: + case PS.ACreate{}: + False{} + case PS.ABind{h}: + Nat.is_eq(h, 0n) + case PS.AExec{h}: + False{} + case PS.AClose{h}: + False{} + +# Enumeration +# ----------- + +# t followed by each action of as +def extend_one(+t: List<&2, PS.Act>, as: List<&2, PS.Act>) -> List<&2, List<&2, PS.Act>>: + match as: + case Nil{}: + Nil{} + case Con{+a, rest}: + List.append(&2, PS.Act, t, [a]) <> extend_one(t, rest) + +# every trace of ts, extended by one action +def extend(ts: List<&2, List<&2, PS.Act>>) -> List<&2, List<&2, PS.Act>>: + match ts: + case Nil{}: + Nil{} + case Con{+t, rest}: + List.append(&2, List<&2, PS.Act>, extend_one(t, alphabet()), extend(rest)) + +# whether a trace starts with a Create +def starts_create(t: List<&2, PS.Act>) -> Bool: + match t: + case Nil{}: + False{} + case Con{a, rest}: + is_create(a) + +# whether a trace starts with Create, Bind 0 +def starts_create_bind(t: List<&2, PS.Act>) -> Bool: + match t: + case Nil{}: + False{} + case Con{a, rest}: + match rest: + case Nil{}: + False{} + case Con{b, rest2}: + is_create(a) && is_bind0(b) + +def keep(t: List<&2, PS.Act>, r: List<&2, List<&2, PS.Act>>, hit: Bool) -> List<&2, List<&2, PS.Act>>: + match hit: + case True{}: + t <> r + case False{}: + r + +def only_create(ts: List<&2, List<&2, PS.Act>>) -> List<&2, List<&2, PS.Act>>: + match ts: + case Nil{}: + Nil{} + case Con{+t, rest}: + keep(t, only_create(rest), starts_create(t)) + +def only_create_bind(ts: List<&2, List<&2, PS.Act>>) -> List<&2, List<&2, PS.Act>>: + match ts: + case Nil{}: + Nil{} + case Con{+t, rest}: + keep(t, only_create_bind(rest), starts_create_bind(t)) + +# all traces of length 1 to 3, the length-4 ones that start with a +# Create, and the length-5 ones that start with Create, Bind 0 +def all_traces() -> List<&2, List<&2, PS.Act>>: + +l1 = extend([Nil{}]) + +l2 = extend(l1) + +l3 = extend(l2) + +l4 = extend(only_create(l3)) + +l5 = extend(only_create_bind(l4)) + List.concat(&2, List<&2, PS.Act>, [l1, l2, l3, l4, l5]) + +# Show +# ---- + +def act_show(a: PS.Act) -> String: + match a: + case PS.ACreate{}: + "C" + case PS.ABind{h}: + "B" ++ Nat.show(h) + case PS.AExec{h}: + "E" ++ Nat.show(h) + case PS.AClose{h}: + "X" ++ Nat.show(h) + +def resp_show(r: PS.Resp) -> String: + match r: + case PS.ROk{h}: + "ok" ++ Nat.show(h) + case PS.RErr{}: + "err" + +def acts_show(t: List<&2, PS.Act>) -> String: + match t: + case Nil{}: + "" + case Con{a, rest}: + match rest: + case Nil{}: + act_show(a) + case Con{b, rest2}: + act_show(a) ++ " " ++ acts_show(b <> rest2) + +def resps_show(rs: List<&2, PS.Resp>) -> String: + match rs: + case Nil{}: + "" + case Con{r, rest}: + match rest: + case Nil{}: + resp_show(r) + case Con{r2, rest2}: + resp_show(r) ++ " " ++ resps_show(r2 <> rest2) + +# one line: the actions, then the responses under rotate, then under keep +def line(+t: List<&2, PS.Act>) -> String: + acts_show(t) ++ " | " ++ resps_show(PS.responses(t, True{})(PS.start())) ++ " | " ++ resps_show(PS.responses(t, False{})(PS.start())) + +def lines(ts: List<&2, List<&2, PS.Act>>) -> String: + match ts: + case Nil{}: + "" + case Con{t, rest}: + line(t) ++ "\n" ++ lines(rest) + +def header() -> String: + "# Licensed to the Apache Software Foundation (ASF) under one\n" + ++ "# or more contributor license agreements. See the NOTICE file\n" + ++ "# distributed with this work for additional information\n" + ++ "# regarding copyright ownership. The ASF licenses this file\n" + ++ "# to you under the Apache License, Version 2.0 (the\n" + ++ "# \"License\"); you may not use this file except in compliance\n" + ++ "# with the License. You may obtain a copy of the License at\n" + ++ "#\n" + ++ "# http://www.apache.org/licenses/LICENSE-2.0\n" + ++ "#\n" + ++ "# Unless required by applicable law or agreed to in writing,\n" + ++ "# software distributed under the License is distributed on an\n" + ++ "# \"AS IS\" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY\n" + ++ "# KIND, either express or implied. See the License for the\n" + ++ "# specific language governing permissions and limitations\n" + ++ "# under the License.\n" + ++ "#\n" + ++ "# GENERATED by dev/bend2/prepared_statement/traces.bend from the proven\n" + ++ "# Flight SQL prepared-statement model. Do not edit by hand.\n" + ++ "# Format: actions | expected responses (rotating bind) | expected responses (keeping bind)\n" + ++ "# Actions: C = CreatePreparedStatement, Bh = DoPut bind on handle h,\n" + ++ "# Eh = GetFlightInfo execute on handle h, Xh = ClosePreparedStatement on h.\n" + ++ "# Responses: okN = success returning handle id N, err = error status.\n" + +def main() -> IO(Unit): + IO.print(header() ++ lines(all_traces())) diff --git a/flight/flight-sql/src/test/java/org/apache/arrow/flight/sql/test/TestFlightSqlBendConformance.java b/flight/flight-sql/src/test/java/org/apache/arrow/flight/sql/test/TestFlightSqlBendConformance.java new file mode 100644 index 0000000000..0619c833db --- /dev/null +++ b/flight/flight-sql/src/test/java/org/apache/arrow/flight/sql/test/TestFlightSqlBendConformance.java @@ -0,0 +1,404 @@ +/* + * Licensed to the Apache Software Foundation (ASF) under one or more + * contributor license agreements. See the NOTICE file distributed with + * this work for additional information regarding copyright ownership. + * The ASF licenses this file to You under the Apache License, Version 2.0 + * (the "License"); you may not use this file except in compliance with + * the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package org.apache.arrow.flight.sql.test; + +import static org.assertj.core.api.Assertions.assertThat; + +import com.google.protobuf.Any; +import com.google.protobuf.ByteString; +import java.io.BufferedReader; +import java.io.IOException; +import java.io.InputStream; +import java.io.InputStreamReader; +import java.nio.charset.StandardCharsets; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.TreeMap; +import java.util.TreeSet; +import java.util.stream.Collectors; +import org.apache.arrow.flight.Action; +import org.apache.arrow.flight.FlightClient; +import org.apache.arrow.flight.FlightDescriptor; +import org.apache.arrow.flight.FlightServer; +import org.apache.arrow.flight.Location; +import org.apache.arrow.flight.PutResult; +import org.apache.arrow.flight.Result; +import org.apache.arrow.flight.SyncPutListener; +import org.apache.arrow.flight.sql.FlightSqlProducer; +import org.apache.arrow.flight.sql.FlightSqlUtils; +import org.apache.arrow.flight.sql.example.FlightSqlExample; +import org.apache.arrow.flight.sql.example.FlightSqlStatelessExample; +import org.apache.arrow.flight.sql.impl.FlightSql.ActionClosePreparedStatementRequest; +import org.apache.arrow.flight.sql.impl.FlightSql.ActionCreatePreparedStatementRequest; +import org.apache.arrow.flight.sql.impl.FlightSql.ActionCreatePreparedStatementResult; +import org.apache.arrow.flight.sql.impl.FlightSql.CommandPreparedStatementQuery; +import org.apache.arrow.flight.sql.impl.FlightSql.DoPutPreparedStatementResult; +import org.apache.arrow.memory.ArrowBuf; +import org.apache.arrow.memory.BufferAllocator; +import org.apache.arrow.memory.RootAllocator; +import org.apache.arrow.util.AutoCloseables; +import org.apache.arrow.vector.IntVector; +import org.apache.arrow.vector.VectorSchemaRoot; +import org.apache.arrow.vector.types.pojo.ArrowType; +import org.apache.arrow.vector.types.pojo.Field; +import org.apache.arrow.vector.types.pojo.Schema; +import org.junit.jupiter.api.Test; + +/** + * Differential conformance test for the Flight SQL prepared-statement lifecycle. + * + *

The expected behaviour comes from a Bend 2 model of the protocol whose laws are + * machine-checked ({@code dev/bend2/prepared_statement/}). The model's trace generator enumerates + * request sequences and records the response the spec-conforming server gives to each request, + * under both bind policies the spec allows: a server that returns an updated handle when parameters + * are bound ("rotate") and one that keeps the handle ("keep"). This test replays every trace + * against a real server through the raw Flight client and compares the success-or-error outcome of + * each request with the model's. + * + *

Deviations are grouped by category (request kind, expected outcome, observed outcome). Each + * server has a set of known, documented deviations; the test fails if a new category appears or a + * known one disappears, so a fix to the example server shows up as a test change. + * + *

See {@code dev/bend2/DIFFERENTIAL_TESTING.md} for the design. + */ +public class TestFlightSqlBendConformance { + + private static final String TRACES = "/bend2/prepared_statement_traces.txt"; + private static final String LOCALHOST = "localhost"; + + /** The stateful example keeps the handle on bind; the model's keep column applies. */ + @Test + public void statefulExampleConformsUnderKeepPolicy() throws Exception { + final Report report = replayAll("derbyBendKeepDB", false); + assertThat(report.stepsCompared).isGreaterThan(1000); + assertThat(report.categories()).isEqualTo(Collections.emptySet()); + } + + /** + * The stateless example rotates the handle on bind; the model's rotate column applies. Its known + * deviations from the model are listed in {@link #KNOWN_STATELESS_DEVIATIONS}. + */ + @Test + public void statelessExampleConformsUnderRotatePolicyExceptKnownDeviations() throws Exception { + final Report report = replayAll("derbyBendRotateDB", true); + assertThat(report.stepsCompared).isGreaterThan(1000); + assertThat(report.categories()).isEqualTo(KNOWN_STATELESS_DEVIATIONS); + } + + /** + * Deviations of {@link FlightSqlStatelessExample} from the model, by category. The stateless + * example encodes the query text (and, after a bind, the bound parameters) into the handle and + * validates nothing on the server, so: + * + *

    + *
  • {@code E expected err observed ok}: executing a closed handle or a stale (pre-bind) + * handle succeeds, because the handle still carries a valid query. The spec says the server + * "should return an error" for a stale handle and that close "closes server resources". + *
  • {@code B expected err observed ok}: binding a closed or stale handle succeeds for the + * same reason. + *
  • {@code B expected ok observed err}: binding the rotated handle a second time fails, + * because the server reads the rotated handle as query text. The spec allows chaining a + * DoPut handle into another DoPut. + *
+ */ + private static final Set KNOWN_STATELESS_DEVIATIONS = + new TreeSet<>( + List.of( + "E expected err observed ok", + "B expected err observed ok", + "B expected ok observed err")); + + // Trace file + // ---------- + + /** One generated trace: the actions and the expected responses under each policy. */ + static final class Trace { + final String[] actions; + final String[] expectRotate; + final String[] expectKeep; + + Trace(String line) { + final String[] parts = line.split("\\|"); + actions = parts[0].trim().split(" "); + expectRotate = parts[1].trim().split(" "); + expectKeep = parts[2].trim().split(" "); + } + + String[] expected(boolean rotate) { + return rotate ? expectRotate : expectKeep; + } + } + + static List loadTraces() throws IOException { + final List traces = new ArrayList<>(); + try (InputStream in = TestFlightSqlBendConformance.class.getResourceAsStream(TRACES); + BufferedReader reader = + new BufferedReader(new InputStreamReader(in, StandardCharsets.UTF_8))) { + String line; + while ((line = reader.readLine()) != null) { + if (line.isEmpty() || line.startsWith("#")) { + continue; + } + traces.add(new Trace(line)); + } + } + return traces; + } + + // Replay + // ------ + + /** What the replay found: the number of steps compared and every deviation. */ + static final class Report { + int stepsCompared; + final Map deviationCounts = new TreeMap<>(); + final Map firstExample = new TreeMap<>(); + + void deviation(String category, String example) { + deviationCounts.merge(category, 1, Integer::sum); + firstExample.putIfAbsent(category, example); + } + + Set categories() { + return new TreeSet<>(deviationCounts.keySet()); + } + + @Override + public String toString() { + return deviationCounts.entrySet().stream() + .map(e -> e.getKey() + " x" + e.getValue() + " e.g. " + firstExample.get(e.getKey())) + .collect(Collectors.joining("\n")); + } + } + + private static Report replayAll(String dbName, boolean rotate) throws Exception { + final List traces = loadTraces(); + final Report report = new Report(); + final Location serverLocation = Location.forGrpcInsecure(LOCALHOST, 0); + final FlightSqlProducer producer = + rotate + ? new FlightSqlStatelessExample(serverLocation, dbName) + : new FlightSqlExample(serverLocation, dbName); + try (BufferAllocator allocator = new RootAllocator(Integer.MAX_VALUE); + FlightServer server = + FlightServer.builder(allocator, serverLocation, producer).build().start(); + FlightClient client = + FlightClient.builder(allocator, Location.forGrpcInsecure(LOCALHOST, server.getPort())) + .build(); + VectorSchemaRoot parameters = VectorSchemaRoot.create(PARAMETER_SCHEMA, allocator)) { + final Replayer replayer = new Replayer(client, parameters, rotate, report); + for (Trace trace : traces) { + replayer.replay(trace); + } + } finally { + AutoCloseables.close(producer); + FlightSqlExample.removeDerbyDatabaseIfExists(dbName); + } + System.out.println( + "Bend conformance (" + + (rotate ? "rotate" : "keep") + + "): " + + report.stepsCompared + + " steps compared, deviations:\n" + + report); + return report; + } + + private static final Schema PARAMETER_SCHEMA = + new Schema(List.of(Field.nullable("p0", new ArrowType.Int(32, true)))); + + /** Replays traces against one server, mapping the model's handle ids to real handles. */ + static final class Replayer { + private final FlightClient client; + private final VectorSchemaRoot parameters; + private final boolean rotate; + private final Report report; + + Replayer(FlightClient client, VectorSchemaRoot parameters, boolean rotate, Report report) { + this.client = client; + this.parameters = parameters; + this.rotate = rotate; + this.report = report; + } + + void replay(Trace trace) { + // model handle id -> the bytes the server actually issued for it + final Map handles = new HashMap<>(); + final String[] expected = trace.expected(rotate); + int created = 0; + for (int i = 0; i < trace.actions.length; i++) { + final String action = trace.actions[i]; + final String want = expected[i]; + final Outcome got; + switch (action.charAt(0)) { + case 'C': + // a distinct query per Create: the example servers use the query text as the handle + created++; + got = create("SELECT * FROM intTable WHERE id = ? AND " + created + " = " + created); + break; + case 'B': + got = bind(handleFor(handles, action)); + break; + case 'E': + got = execute(handleFor(handles, action)); + break; + case 'X': + got = close(handleFor(handles, action)); + break; + default: + throw new IllegalArgumentException("unknown action " + action); + } + // the model told us which id the server's Ok carries: remember its real bytes + if (got.ok && want.startsWith("ok") && got.handle != null) { + handles.put(Integer.parseInt(want.substring(2)), got.handle); + } + report.stepsCompared++; + final String wantKind = want.startsWith("ok") ? "ok" : "err"; + final String gotKind = got.ok ? "ok" : "err"; + if (!wantKind.equals(gotKind)) { + report.deviation( + action.charAt(0) + " expected " + wantKind + " observed " + gotKind, + String.join(" ", trace.actions) + " @" + (i + 1) + " (" + got.detail + ")"); + } + } + // leave no statement behind between traces + for (ByteString handle : handles.values()) { + close(handle); + } + } + + private static ByteString handleFor(Map handles, String action) { + final int id = Integer.parseInt(action.substring(1)); + // a handle the model never issued in this trace: bytes no server has seen + return handles.getOrDefault(id, ByteString.copyFromUtf8("bend2-unknown-handle-" + id)); + } + + private Outcome create(String query) { + try { + final Action action = + new Action( + FlightSqlUtils.FLIGHT_SQL_CREATE_PREPARED_STATEMENT.getType(), + Any.pack(ActionCreatePreparedStatementRequest.newBuilder().setQuery(query).build()) + .toByteArray()); + final Result result = client.doAction(action).next(); + final ActionCreatePreparedStatementResult parsed = + FlightSqlUtils.unpackAndParseOrThrow( + result.getBody(), ActionCreatePreparedStatementResult.class); + return Outcome.ok(parsed.getPreparedStatementHandle()); + } catch (RuntimeException e) { + return Outcome.err(e); + } + } + + private Outcome bind(ByteString handle) { + try (SyncPutListener listener = new SyncPutListener()) { + parameters.allocateNew(); + ((IntVector) parameters.getVector(0)).setSafe(0, 1); + parameters.setRowCount(1); + final FlightClient.ClientStreamListener writer = + client.startPut(descriptor(handle), parameters, listener); + writer.putNext(); + writer.completed(); + writer.getResult(); + ByteString updated = null; + final PutResult putResult = listener.read(); + if (putResult != null) { + try (ArrowBuf metadata = putResult.getApplicationMetadata()) { + if (metadata != null) { + final DoPutPreparedStatementResult parsed = + DoPutPreparedStatementResult.parseFrom(metadata.nioBuffer()); + if (!parsed.getPreparedStatementHandle().isEmpty()) { + updated = parsed.getPreparedStatementHandle(); + } + } + } + } + // no updated handle: the server kept the one we sent + return Outcome.ok(updated != null ? updated : handle); + } catch (RuntimeException + | InterruptedException + | java.util.concurrent.ExecutionException + | com.google.protobuf.InvalidProtocolBufferException e) { + return Outcome.err(e); + } + } + + private Outcome execute(ByteString handle) { + try { + client.getInfo(descriptor(handle)); + return Outcome.ok(handle); + } catch (RuntimeException e) { + return Outcome.err(e); + } + } + + private Outcome close(ByteString handle) { + try { + final Action action = + new Action( + FlightSqlUtils.FLIGHT_SQL_CLOSE_PREPARED_STATEMENT.getType(), + Any.pack( + ActionClosePreparedStatementRequest.newBuilder() + .setPreparedStatementHandle(handle) + .build()) + .toByteArray()); + client.doAction(action).forEachRemaining(result -> {}); + return Outcome.ok(handle); + } catch (RuntimeException e) { + return Outcome.err(e); + } + } + + private static FlightDescriptor descriptor(ByteString handle) { + return FlightDescriptor.command( + Any.pack( + CommandPreparedStatementQuery.newBuilder() + .setPreparedStatementHandle(handle) + .build()) + .toByteArray()); + } + } + + /** The outcome of one request: success with the handle to use next, or an error. */ + static final class Outcome { + final boolean ok; + final ByteString handle; + final String detail; + + private Outcome(boolean ok, ByteString handle, String detail) { + this.ok = ok; + this.handle = handle; + this.detail = detail; + } + + static Outcome ok(ByteString handle) { + return new Outcome(true, handle, "ok"); + } + + static Outcome err(Exception e) { + final String message = e.getMessage() == null ? "" : e.getMessage(); + return new Outcome( + false, + null, + e.getClass().getSimpleName() + ": " + message.lines().findFirst().orElse("")); + } + } +} diff --git a/flight/flight-sql/src/test/resources/bend2/prepared_statement_traces.txt b/flight/flight-sql/src/test/resources/bend2/prepared_statement_traces.txt new file mode 100644 index 0000000000..b83364c787 --- /dev/null +++ b/flight/flight-sql/src/test/resources/bend2/prepared_statement_traces.txt @@ -0,0 +1,1109 @@ +# Licensed to the Apache Software Foundation (ASF) under one +# or more contributor license agreements. See the NOTICE file +# distributed with this work for additional information +# regarding copyright ownership. The ASF licenses this file +# to you under the Apache License, Version 2.0 (the +# "License"); you may not use this file except in compliance +# with the License. You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, +# software distributed under the License is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY +# KIND, either express or implied. See the License for the +# specific language governing permissions and limitations +# under the License. +# +# GENERATED by dev/bend2/prepared_statement/traces.bend from the proven +# Flight SQL prepared-statement model. Do not edit by hand. +# Format: actions | expected responses (rotating bind) | expected responses (keeping bind) +# Actions: C = CreatePreparedStatement, Bh = DoPut bind on handle h, +# Eh = GetFlightInfo execute on handle h, Xh = ClosePreparedStatement on h. +# Responses: okN = success returning handle id N, err = error status. +C | ok0 | ok0 +B0 | err | err +B1 | err | err +E0 | err | err +E1 | err | err +X0 | ok0 | ok0 +X1 | ok1 | ok1 +C C | ok0 ok1 | ok0 ok1 +C B0 | ok0 ok1 | ok0 ok0 +C B1 | ok0 err | ok0 err +C E0 | ok0 ok0 | ok0 ok0 +C E1 | ok0 err | ok0 err +C X0 | ok0 ok0 | ok0 ok0 +C X1 | ok0 ok1 | ok0 ok1 +B0 C | err ok0 | err ok0 +B0 B0 | err err | err err +B0 B1 | err err | err err +B0 E0 | err err | err err +B0 E1 | err err | err err +B0 X0 | err ok0 | err ok0 +B0 X1 | err ok1 | err ok1 +B1 C | err ok0 | err ok0 +B1 B0 | err err | err err +B1 B1 | err err | err err +B1 E0 | err err | err err +B1 E1 | err err | err err +B1 X0 | err ok0 | err ok0 +B1 X1 | err ok1 | err ok1 +E0 C | err ok0 | err ok0 +E0 B0 | err err | err err +E0 B1 | err err | err err +E0 E0 | err err | err err +E0 E1 | err err | err err +E0 X0 | err ok0 | err ok0 +E0 X1 | err ok1 | err ok1 +E1 C | err ok0 | err ok0 +E1 B0 | err err | err err +E1 B1 | err err | err err +E1 E0 | err err | err err +E1 E1 | err err | err err +E1 X0 | err ok0 | err ok0 +E1 X1 | err ok1 | err ok1 +X0 C | ok0 ok0 | ok0 ok0 +X0 B0 | ok0 err | ok0 err +X0 B1 | ok0 err | ok0 err +X0 E0 | ok0 err | ok0 err +X0 E1 | ok0 err | ok0 err +X0 X0 | ok0 ok0 | ok0 ok0 +X0 X1 | ok0 ok1 | ok0 ok1 +X1 C | ok1 ok0 | ok1 ok0 +X1 B0 | ok1 err | ok1 err +X1 B1 | ok1 err | ok1 err +X1 E0 | ok1 err | ok1 err +X1 E1 | ok1 err | ok1 err +X1 X0 | ok1 ok0 | ok1 ok0 +X1 X1 | ok1 ok1 | ok1 ok1 +C C C | ok0 ok1 ok2 | ok0 ok1 ok2 +C C B0 | ok0 ok1 ok2 | ok0 ok1 ok0 +C C B1 | ok0 ok1 ok2 | ok0 ok1 ok1 +C C E0 | ok0 ok1 ok0 | ok0 ok1 ok0 +C C E1 | ok0 ok1 ok1 | ok0 ok1 ok1 +C C X0 | ok0 ok1 ok0 | ok0 ok1 ok0 +C C X1 | ok0 ok1 ok1 | ok0 ok1 ok1 +C B0 C | ok0 ok1 ok2 | ok0 ok0 ok1 +C B0 B0 | ok0 ok1 err | ok0 ok0 ok0 +C B0 B1 | ok0 ok1 ok2 | ok0 ok0 err +C B0 E0 | ok0 ok1 err | ok0 ok0 ok0 +C B0 E1 | ok0 ok1 ok1 | ok0 ok0 err +C B0 X0 | ok0 ok1 ok0 | ok0 ok0 ok0 +C B0 X1 | ok0 ok1 ok1 | ok0 ok0 ok1 +C B1 C | ok0 err ok1 | ok0 err ok1 +C B1 B0 | ok0 err ok1 | ok0 err ok0 +C B1 B1 | ok0 err err | ok0 err err +C B1 E0 | ok0 err ok0 | ok0 err ok0 +C B1 E1 | ok0 err err | ok0 err err +C B1 X0 | ok0 err ok0 | ok0 err ok0 +C B1 X1 | ok0 err ok1 | ok0 err ok1 +C E0 C | ok0 ok0 ok1 | ok0 ok0 ok1 +C E0 B0 | ok0 ok0 ok1 | ok0 ok0 ok0 +C E0 B1 | ok0 ok0 err | ok0 ok0 err +C E0 E0 | ok0 ok0 ok0 | ok0 ok0 ok0 +C E0 E1 | ok0 ok0 err | ok0 ok0 err +C E0 X0 | ok0 ok0 ok0 | ok0 ok0 ok0 +C E0 X1 | ok0 ok0 ok1 | ok0 ok0 ok1 +C E1 C | ok0 err ok1 | ok0 err ok1 +C E1 B0 | ok0 err ok1 | ok0 err ok0 +C E1 B1 | ok0 err err | ok0 err err +C E1 E0 | ok0 err ok0 | ok0 err ok0 +C E1 E1 | ok0 err err | ok0 err err +C E1 X0 | ok0 err ok0 | ok0 err ok0 +C E1 X1 | ok0 err ok1 | ok0 err ok1 +C X0 C | ok0 ok0 ok1 | ok0 ok0 ok1 +C X0 B0 | ok0 ok0 err | ok0 ok0 err +C X0 B1 | ok0 ok0 err | ok0 ok0 err +C X0 E0 | ok0 ok0 err | ok0 ok0 err +C X0 E1 | ok0 ok0 err | ok0 ok0 err +C X0 X0 | ok0 ok0 ok0 | ok0 ok0 ok0 +C X0 X1 | ok0 ok0 ok1 | ok0 ok0 ok1 +C X1 C | ok0 ok1 ok1 | ok0 ok1 ok1 +C X1 B0 | ok0 ok1 ok1 | ok0 ok1 ok0 +C X1 B1 | ok0 ok1 err | ok0 ok1 err +C X1 E0 | ok0 ok1 ok0 | ok0 ok1 ok0 +C X1 E1 | ok0 ok1 err | ok0 ok1 err +C X1 X0 | ok0 ok1 ok0 | ok0 ok1 ok0 +C X1 X1 | ok0 ok1 ok1 | ok0 ok1 ok1 +B0 C C | err ok0 ok1 | err ok0 ok1 +B0 C B0 | err ok0 ok1 | err ok0 ok0 +B0 C B1 | err ok0 err | err ok0 err +B0 C E0 | err ok0 ok0 | err ok0 ok0 +B0 C E1 | err ok0 err | err ok0 err +B0 C X0 | err ok0 ok0 | err ok0 ok0 +B0 C X1 | err ok0 ok1 | err ok0 ok1 +B0 B0 C | err err ok0 | err err ok0 +B0 B0 B0 | err err err | err err err +B0 B0 B1 | err err err | err err err +B0 B0 E0 | err err err | err err err +B0 B0 E1 | err err err | err err err +B0 B0 X0 | err err ok0 | err err ok0 +B0 B0 X1 | err err ok1 | err err ok1 +B0 B1 C | err err ok0 | err err ok0 +B0 B1 B0 | err err err | err err err +B0 B1 B1 | err err err | err err err +B0 B1 E0 | err err err | err err err +B0 B1 E1 | err err err | err err err +B0 B1 X0 | err err ok0 | err err ok0 +B0 B1 X1 | err err ok1 | err err ok1 +B0 E0 C | err err ok0 | err err ok0 +B0 E0 B0 | err err err | err err err +B0 E0 B1 | err err err | err err err +B0 E0 E0 | err err err | err err err +B0 E0 E1 | err err err | err err err +B0 E0 X0 | err err ok0 | err err ok0 +B0 E0 X1 | err err ok1 | err err ok1 +B0 E1 C | err err ok0 | err err ok0 +B0 E1 B0 | err err err | err err err +B0 E1 B1 | err err err | err err err +B0 E1 E0 | err err err | err err err +B0 E1 E1 | err err err | err err err +B0 E1 X0 | err err ok0 | err err ok0 +B0 E1 X1 | err err ok1 | err err ok1 +B0 X0 C | err ok0 ok0 | err ok0 ok0 +B0 X0 B0 | err ok0 err | err ok0 err +B0 X0 B1 | err ok0 err | err ok0 err +B0 X0 E0 | err ok0 err | err ok0 err +B0 X0 E1 | err ok0 err | err ok0 err +B0 X0 X0 | err ok0 ok0 | err ok0 ok0 +B0 X0 X1 | err ok0 ok1 | err ok0 ok1 +B0 X1 C | err ok1 ok0 | err ok1 ok0 +B0 X1 B0 | err ok1 err | err ok1 err +B0 X1 B1 | err ok1 err | err ok1 err +B0 X1 E0 | err ok1 err | err ok1 err +B0 X1 E1 | err ok1 err | err ok1 err +B0 X1 X0 | err ok1 ok0 | err ok1 ok0 +B0 X1 X1 | err ok1 ok1 | err ok1 ok1 +B1 C C | err ok0 ok1 | err ok0 ok1 +B1 C B0 | err ok0 ok1 | err ok0 ok0 +B1 C B1 | err ok0 err | err ok0 err +B1 C E0 | err ok0 ok0 | err ok0 ok0 +B1 C E1 | err ok0 err | err ok0 err +B1 C X0 | err ok0 ok0 | err ok0 ok0 +B1 C X1 | err ok0 ok1 | err ok0 ok1 +B1 B0 C | err err ok0 | err err ok0 +B1 B0 B0 | err err err | err err err +B1 B0 B1 | err err err | err err err +B1 B0 E0 | err err err | err err err +B1 B0 E1 | err err err | err err err +B1 B0 X0 | err err ok0 | err err ok0 +B1 B0 X1 | err err ok1 | err err ok1 +B1 B1 C | err err ok0 | err err ok0 +B1 B1 B0 | err err err | err err err +B1 B1 B1 | err err err | err err err +B1 B1 E0 | err err err | err err err +B1 B1 E1 | err err err | err err err +B1 B1 X0 | err err ok0 | err err ok0 +B1 B1 X1 | err err ok1 | err err ok1 +B1 E0 C | err err ok0 | err err ok0 +B1 E0 B0 | err err err | err err err +B1 E0 B1 | err err err | err err err +B1 E0 E0 | err err err | err err err +B1 E0 E1 | err err err | err err err +B1 E0 X0 | err err ok0 | err err ok0 +B1 E0 X1 | err err ok1 | err err ok1 +B1 E1 C | err err ok0 | err err ok0 +B1 E1 B0 | err err err | err err err +B1 E1 B1 | err err err | err err err +B1 E1 E0 | err err err | err err err +B1 E1 E1 | err err err | err err err +B1 E1 X0 | err err ok0 | err err ok0 +B1 E1 X1 | err err ok1 | err err ok1 +B1 X0 C | err ok0 ok0 | err ok0 ok0 +B1 X0 B0 | err ok0 err | err ok0 err +B1 X0 B1 | err ok0 err | err ok0 err +B1 X0 E0 | err ok0 err | err ok0 err +B1 X0 E1 | err ok0 err | err ok0 err +B1 X0 X0 | err ok0 ok0 | err ok0 ok0 +B1 X0 X1 | err ok0 ok1 | err ok0 ok1 +B1 X1 C | err ok1 ok0 | err ok1 ok0 +B1 X1 B0 | err ok1 err | err ok1 err +B1 X1 B1 | err ok1 err | err ok1 err +B1 X1 E0 | err ok1 err | err ok1 err +B1 X1 E1 | err ok1 err | err ok1 err +B1 X1 X0 | err ok1 ok0 | err ok1 ok0 +B1 X1 X1 | err ok1 ok1 | err ok1 ok1 +E0 C C | err ok0 ok1 | err ok0 ok1 +E0 C B0 | err ok0 ok1 | err ok0 ok0 +E0 C B1 | err ok0 err | err ok0 err +E0 C E0 | err ok0 ok0 | err ok0 ok0 +E0 C E1 | err ok0 err | err ok0 err +E0 C X0 | err ok0 ok0 | err ok0 ok0 +E0 C X1 | err ok0 ok1 | err ok0 ok1 +E0 B0 C | err err ok0 | err err ok0 +E0 B0 B0 | err err err | err err err +E0 B0 B1 | err err err | err err err +E0 B0 E0 | err err err | err err err +E0 B0 E1 | err err err | err err err +E0 B0 X0 | err err ok0 | err err ok0 +E0 B0 X1 | err err ok1 | err err ok1 +E0 B1 C | err err ok0 | err err ok0 +E0 B1 B0 | err err err | err err err +E0 B1 B1 | err err err | err err err +E0 B1 E0 | err err err | err err err +E0 B1 E1 | err err err | err err err +E0 B1 X0 | err err ok0 | err err ok0 +E0 B1 X1 | err err ok1 | err err ok1 +E0 E0 C | err err ok0 | err err ok0 +E0 E0 B0 | err err err | err err err +E0 E0 B1 | err err err | err err err +E0 E0 E0 | err err err | err err err +E0 E0 E1 | err err err | err err err +E0 E0 X0 | err err ok0 | err err ok0 +E0 E0 X1 | err err ok1 | err err ok1 +E0 E1 C | err err ok0 | err err ok0 +E0 E1 B0 | err err err | err err err +E0 E1 B1 | err err err | err err err +E0 E1 E0 | err err err | err err err +E0 E1 E1 | err err err | err err err +E0 E1 X0 | err err ok0 | err err ok0 +E0 E1 X1 | err err ok1 | err err ok1 +E0 X0 C | err ok0 ok0 | err ok0 ok0 +E0 X0 B0 | err ok0 err | err ok0 err +E0 X0 B1 | err ok0 err | err ok0 err +E0 X0 E0 | err ok0 err | err ok0 err +E0 X0 E1 | err ok0 err | err ok0 err +E0 X0 X0 | err ok0 ok0 | err ok0 ok0 +E0 X0 X1 | err ok0 ok1 | err ok0 ok1 +E0 X1 C | err ok1 ok0 | err ok1 ok0 +E0 X1 B0 | err ok1 err | err ok1 err +E0 X1 B1 | err ok1 err | err ok1 err +E0 X1 E0 | err ok1 err | err ok1 err +E0 X1 E1 | err ok1 err | err ok1 err +E0 X1 X0 | err ok1 ok0 | err ok1 ok0 +E0 X1 X1 | err ok1 ok1 | err ok1 ok1 +E1 C C | err ok0 ok1 | err ok0 ok1 +E1 C B0 | err ok0 ok1 | err ok0 ok0 +E1 C B1 | err ok0 err | err ok0 err +E1 C E0 | err ok0 ok0 | err ok0 ok0 +E1 C E1 | err ok0 err | err ok0 err +E1 C X0 | err ok0 ok0 | err ok0 ok0 +E1 C X1 | err ok0 ok1 | err ok0 ok1 +E1 B0 C | err err ok0 | err err ok0 +E1 B0 B0 | err err err | err err err +E1 B0 B1 | err err err | err err err +E1 B0 E0 | err err err | err err err +E1 B0 E1 | err err err | err err err +E1 B0 X0 | err err ok0 | err err ok0 +E1 B0 X1 | err err ok1 | err err ok1 +E1 B1 C | err err ok0 | err err ok0 +E1 B1 B0 | err err err | err err err +E1 B1 B1 | err err err | err err err +E1 B1 E0 | err err err | err err err +E1 B1 E1 | err err err | err err err +E1 B1 X0 | err err ok0 | err err ok0 +E1 B1 X1 | err err ok1 | err err ok1 +E1 E0 C | err err ok0 | err err ok0 +E1 E0 B0 | err err err | err err err +E1 E0 B1 | err err err | err err err +E1 E0 E0 | err err err | err err err +E1 E0 E1 | err err err | err err err +E1 E0 X0 | err err ok0 | err err ok0 +E1 E0 X1 | err err ok1 | err err ok1 +E1 E1 C | err err ok0 | err err ok0 +E1 E1 B0 | err err err | err err err +E1 E1 B1 | err err err | err err err +E1 E1 E0 | err err err | err err err +E1 E1 E1 | err err err | err err err +E1 E1 X0 | err err ok0 | err err ok0 +E1 E1 X1 | err err ok1 | err err ok1 +E1 X0 C | err ok0 ok0 | err ok0 ok0 +E1 X0 B0 | err ok0 err | err ok0 err +E1 X0 B1 | err ok0 err | err ok0 err +E1 X0 E0 | err ok0 err | err ok0 err +E1 X0 E1 | err ok0 err | err ok0 err +E1 X0 X0 | err ok0 ok0 | err ok0 ok0 +E1 X0 X1 | err ok0 ok1 | err ok0 ok1 +E1 X1 C | err ok1 ok0 | err ok1 ok0 +E1 X1 B0 | err ok1 err | err ok1 err +E1 X1 B1 | err ok1 err | err ok1 err +E1 X1 E0 | err ok1 err | err ok1 err +E1 X1 E1 | err ok1 err | err ok1 err +E1 X1 X0 | err ok1 ok0 | err ok1 ok0 +E1 X1 X1 | err ok1 ok1 | err ok1 ok1 +X0 C C | ok0 ok0 ok1 | ok0 ok0 ok1 +X0 C B0 | ok0 ok0 ok1 | ok0 ok0 ok0 +X0 C B1 | ok0 ok0 err | ok0 ok0 err +X0 C E0 | ok0 ok0 ok0 | ok0 ok0 ok0 +X0 C E1 | ok0 ok0 err | ok0 ok0 err +X0 C X0 | ok0 ok0 ok0 | ok0 ok0 ok0 +X0 C X1 | ok0 ok0 ok1 | ok0 ok0 ok1 +X0 B0 C | ok0 err ok0 | ok0 err ok0 +X0 B0 B0 | ok0 err err | ok0 err err +X0 B0 B1 | ok0 err err | ok0 err err +X0 B0 E0 | ok0 err err | ok0 err err +X0 B0 E1 | ok0 err err | ok0 err err +X0 B0 X0 | ok0 err ok0 | ok0 err ok0 +X0 B0 X1 | ok0 err ok1 | ok0 err ok1 +X0 B1 C | ok0 err ok0 | ok0 err ok0 +X0 B1 B0 | ok0 err err | ok0 err err +X0 B1 B1 | ok0 err err | ok0 err err +X0 B1 E0 | ok0 err err | ok0 err err +X0 B1 E1 | ok0 err err | ok0 err err +X0 B1 X0 | ok0 err ok0 | ok0 err ok0 +X0 B1 X1 | ok0 err ok1 | ok0 err ok1 +X0 E0 C | ok0 err ok0 | ok0 err ok0 +X0 E0 B0 | ok0 err err | ok0 err err +X0 E0 B1 | ok0 err err | ok0 err err +X0 E0 E0 | ok0 err err | ok0 err err +X0 E0 E1 | ok0 err err | ok0 err err +X0 E0 X0 | ok0 err ok0 | ok0 err ok0 +X0 E0 X1 | ok0 err ok1 | ok0 err ok1 +X0 E1 C | ok0 err ok0 | ok0 err ok0 +X0 E1 B0 | ok0 err err | ok0 err err +X0 E1 B1 | ok0 err err | ok0 err err +X0 E1 E0 | ok0 err err | ok0 err err +X0 E1 E1 | ok0 err err | ok0 err err +X0 E1 X0 | ok0 err ok0 | ok0 err ok0 +X0 E1 X1 | ok0 err ok1 | ok0 err ok1 +X0 X0 C | ok0 ok0 ok0 | ok0 ok0 ok0 +X0 X0 B0 | ok0 ok0 err | ok0 ok0 err +X0 X0 B1 | ok0 ok0 err | ok0 ok0 err +X0 X0 E0 | ok0 ok0 err | ok0 ok0 err +X0 X0 E1 | ok0 ok0 err | ok0 ok0 err +X0 X0 X0 | ok0 ok0 ok0 | ok0 ok0 ok0 +X0 X0 X1 | ok0 ok0 ok1 | ok0 ok0 ok1 +X0 X1 C | ok0 ok1 ok0 | ok0 ok1 ok0 +X0 X1 B0 | ok0 ok1 err | ok0 ok1 err +X0 X1 B1 | ok0 ok1 err | ok0 ok1 err +X0 X1 E0 | ok0 ok1 err | ok0 ok1 err +X0 X1 E1 | ok0 ok1 err | ok0 ok1 err +X0 X1 X0 | ok0 ok1 ok0 | ok0 ok1 ok0 +X0 X1 X1 | ok0 ok1 ok1 | ok0 ok1 ok1 +X1 C C | ok1 ok0 ok1 | ok1 ok0 ok1 +X1 C B0 | ok1 ok0 ok1 | ok1 ok0 ok0 +X1 C B1 | ok1 ok0 err | ok1 ok0 err +X1 C E0 | ok1 ok0 ok0 | ok1 ok0 ok0 +X1 C E1 | ok1 ok0 err | ok1 ok0 err +X1 C X0 | ok1 ok0 ok0 | ok1 ok0 ok0 +X1 C X1 | ok1 ok0 ok1 | ok1 ok0 ok1 +X1 B0 C | ok1 err ok0 | ok1 err ok0 +X1 B0 B0 | ok1 err err | ok1 err err +X1 B0 B1 | ok1 err err | ok1 err err +X1 B0 E0 | ok1 err err | ok1 err err +X1 B0 E1 | ok1 err err | ok1 err err +X1 B0 X0 | ok1 err ok0 | ok1 err ok0 +X1 B0 X1 | ok1 err ok1 | ok1 err ok1 +X1 B1 C | ok1 err ok0 | ok1 err ok0 +X1 B1 B0 | ok1 err err | ok1 err err +X1 B1 B1 | ok1 err err | ok1 err err +X1 B1 E0 | ok1 err err | ok1 err err +X1 B1 E1 | ok1 err err | ok1 err err +X1 B1 X0 | ok1 err ok0 | ok1 err ok0 +X1 B1 X1 | ok1 err ok1 | ok1 err ok1 +X1 E0 C | ok1 err ok0 | ok1 err ok0 +X1 E0 B0 | ok1 err err | ok1 err err +X1 E0 B1 | ok1 err err | ok1 err err +X1 E0 E0 | ok1 err err | ok1 err err +X1 E0 E1 | ok1 err err | ok1 err err +X1 E0 X0 | ok1 err ok0 | ok1 err ok0 +X1 E0 X1 | ok1 err ok1 | ok1 err ok1 +X1 E1 C | ok1 err ok0 | ok1 err ok0 +X1 E1 B0 | ok1 err err | ok1 err err +X1 E1 B1 | ok1 err err | ok1 err err +X1 E1 E0 | ok1 err err | ok1 err err +X1 E1 E1 | ok1 err err | ok1 err err +X1 E1 X0 | ok1 err ok0 | ok1 err ok0 +X1 E1 X1 | ok1 err ok1 | ok1 err ok1 +X1 X0 C | ok1 ok0 ok0 | ok1 ok0 ok0 +X1 X0 B0 | ok1 ok0 err | ok1 ok0 err +X1 X0 B1 | ok1 ok0 err | ok1 ok0 err +X1 X0 E0 | ok1 ok0 err | ok1 ok0 err +X1 X0 E1 | ok1 ok0 err | ok1 ok0 err +X1 X0 X0 | ok1 ok0 ok0 | ok1 ok0 ok0 +X1 X0 X1 | ok1 ok0 ok1 | ok1 ok0 ok1 +X1 X1 C | ok1 ok1 ok0 | ok1 ok1 ok0 +X1 X1 B0 | ok1 ok1 err | ok1 ok1 err +X1 X1 B1 | ok1 ok1 err | ok1 ok1 err +X1 X1 E0 | ok1 ok1 err | ok1 ok1 err +X1 X1 E1 | ok1 ok1 err | ok1 ok1 err +X1 X1 X0 | ok1 ok1 ok0 | ok1 ok1 ok0 +X1 X1 X1 | ok1 ok1 ok1 | ok1 ok1 ok1 +C C C C | ok0 ok1 ok2 ok3 | ok0 ok1 ok2 ok3 +C C C B0 | ok0 ok1 ok2 ok3 | ok0 ok1 ok2 ok0 +C C C B1 | ok0 ok1 ok2 ok3 | ok0 ok1 ok2 ok1 +C C C E0 | ok0 ok1 ok2 ok0 | ok0 ok1 ok2 ok0 +C C C E1 | ok0 ok1 ok2 ok1 | ok0 ok1 ok2 ok1 +C C C X0 | ok0 ok1 ok2 ok0 | ok0 ok1 ok2 ok0 +C C C X1 | ok0 ok1 ok2 ok1 | ok0 ok1 ok2 ok1 +C C B0 C | ok0 ok1 ok2 ok3 | ok0 ok1 ok0 ok2 +C C B0 B0 | ok0 ok1 ok2 err | ok0 ok1 ok0 ok0 +C C B0 B1 | ok0 ok1 ok2 ok3 | ok0 ok1 ok0 ok1 +C C B0 E0 | ok0 ok1 ok2 err | ok0 ok1 ok0 ok0 +C C B0 E1 | ok0 ok1 ok2 ok1 | ok0 ok1 ok0 ok1 +C C B0 X0 | ok0 ok1 ok2 ok0 | ok0 ok1 ok0 ok0 +C C B0 X1 | ok0 ok1 ok2 ok1 | ok0 ok1 ok0 ok1 +C C B1 C | ok0 ok1 ok2 ok3 | ok0 ok1 ok1 ok2 +C C B1 B0 | ok0 ok1 ok2 ok3 | ok0 ok1 ok1 ok0 +C C B1 B1 | ok0 ok1 ok2 err | ok0 ok1 ok1 ok1 +C C B1 E0 | ok0 ok1 ok2 ok0 | ok0 ok1 ok1 ok0 +C C B1 E1 | ok0 ok1 ok2 err | ok0 ok1 ok1 ok1 +C C B1 X0 | ok0 ok1 ok2 ok0 | ok0 ok1 ok1 ok0 +C C B1 X1 | ok0 ok1 ok2 ok1 | ok0 ok1 ok1 ok1 +C C E0 C | ok0 ok1 ok0 ok2 | ok0 ok1 ok0 ok2 +C C E0 B0 | ok0 ok1 ok0 ok2 | ok0 ok1 ok0 ok0 +C C E0 B1 | ok0 ok1 ok0 ok2 | ok0 ok1 ok0 ok1 +C C E0 E0 | ok0 ok1 ok0 ok0 | ok0 ok1 ok0 ok0 +C C E0 E1 | ok0 ok1 ok0 ok1 | ok0 ok1 ok0 ok1 +C C E0 X0 | ok0 ok1 ok0 ok0 | ok0 ok1 ok0 ok0 +C C E0 X1 | ok0 ok1 ok0 ok1 | ok0 ok1 ok0 ok1 +C C E1 C | ok0 ok1 ok1 ok2 | ok0 ok1 ok1 ok2 +C C E1 B0 | ok0 ok1 ok1 ok2 | ok0 ok1 ok1 ok0 +C C E1 B1 | ok0 ok1 ok1 ok2 | ok0 ok1 ok1 ok1 +C C E1 E0 | ok0 ok1 ok1 ok0 | ok0 ok1 ok1 ok0 +C C E1 E1 | ok0 ok1 ok1 ok1 | ok0 ok1 ok1 ok1 +C C E1 X0 | ok0 ok1 ok1 ok0 | ok0 ok1 ok1 ok0 +C C E1 X1 | ok0 ok1 ok1 ok1 | ok0 ok1 ok1 ok1 +C C X0 C | ok0 ok1 ok0 ok2 | ok0 ok1 ok0 ok2 +C C X0 B0 | ok0 ok1 ok0 err | ok0 ok1 ok0 err +C C X0 B1 | ok0 ok1 ok0 ok2 | ok0 ok1 ok0 ok1 +C C X0 E0 | ok0 ok1 ok0 err | ok0 ok1 ok0 err +C C X0 E1 | ok0 ok1 ok0 ok1 | ok0 ok1 ok0 ok1 +C C X0 X0 | ok0 ok1 ok0 ok0 | ok0 ok1 ok0 ok0 +C C X0 X1 | ok0 ok1 ok0 ok1 | ok0 ok1 ok0 ok1 +C C X1 C | ok0 ok1 ok1 ok2 | ok0 ok1 ok1 ok2 +C C X1 B0 | ok0 ok1 ok1 ok2 | ok0 ok1 ok1 ok0 +C C X1 B1 | ok0 ok1 ok1 err | ok0 ok1 ok1 err +C C X1 E0 | ok0 ok1 ok1 ok0 | ok0 ok1 ok1 ok0 +C C X1 E1 | ok0 ok1 ok1 err | ok0 ok1 ok1 err +C C X1 X0 | ok0 ok1 ok1 ok0 | ok0 ok1 ok1 ok0 +C C X1 X1 | ok0 ok1 ok1 ok1 | ok0 ok1 ok1 ok1 +C B0 C C | ok0 ok1 ok2 ok3 | ok0 ok0 ok1 ok2 +C B0 C B0 | ok0 ok1 ok2 err | ok0 ok0 ok1 ok0 +C B0 C B1 | ok0 ok1 ok2 ok3 | ok0 ok0 ok1 ok1 +C B0 C E0 | ok0 ok1 ok2 err | ok0 ok0 ok1 ok0 +C B0 C E1 | ok0 ok1 ok2 ok1 | ok0 ok0 ok1 ok1 +C B0 C X0 | ok0 ok1 ok2 ok0 | ok0 ok0 ok1 ok0 +C B0 C X1 | ok0 ok1 ok2 ok1 | ok0 ok0 ok1 ok1 +C B0 B0 C | ok0 ok1 err ok2 | ok0 ok0 ok0 ok1 +C B0 B0 B0 | ok0 ok1 err err | ok0 ok0 ok0 ok0 +C B0 B0 B1 | ok0 ok1 err ok2 | ok0 ok0 ok0 err +C B0 B0 E0 | ok0 ok1 err err | ok0 ok0 ok0 ok0 +C B0 B0 E1 | ok0 ok1 err ok1 | ok0 ok0 ok0 err +C B0 B0 X0 | ok0 ok1 err ok0 | ok0 ok0 ok0 ok0 +C B0 B0 X1 | ok0 ok1 err ok1 | ok0 ok0 ok0 ok1 +C B0 B1 C | ok0 ok1 ok2 ok3 | ok0 ok0 err ok1 +C B0 B1 B0 | ok0 ok1 ok2 err | ok0 ok0 err ok0 +C B0 B1 B1 | ok0 ok1 ok2 err | ok0 ok0 err err +C B0 B1 E0 | ok0 ok1 ok2 err | ok0 ok0 err ok0 +C B0 B1 E1 | ok0 ok1 ok2 err | ok0 ok0 err err +C B0 B1 X0 | ok0 ok1 ok2 ok0 | ok0 ok0 err ok0 +C B0 B1 X1 | ok0 ok1 ok2 ok1 | ok0 ok0 err ok1 +C B0 E0 C | ok0 ok1 err ok2 | ok0 ok0 ok0 ok1 +C B0 E0 B0 | ok0 ok1 err err | ok0 ok0 ok0 ok0 +C B0 E0 B1 | ok0 ok1 err ok2 | ok0 ok0 ok0 err +C B0 E0 E0 | ok0 ok1 err err | ok0 ok0 ok0 ok0 +C B0 E0 E1 | ok0 ok1 err ok1 | ok0 ok0 ok0 err +C B0 E0 X0 | ok0 ok1 err ok0 | ok0 ok0 ok0 ok0 +C B0 E0 X1 | ok0 ok1 err ok1 | ok0 ok0 ok0 ok1 +C B0 E1 C | ok0 ok1 ok1 ok2 | ok0 ok0 err ok1 +C B0 E1 B0 | ok0 ok1 ok1 err | ok0 ok0 err ok0 +C B0 E1 B1 | ok0 ok1 ok1 ok2 | ok0 ok0 err err +C B0 E1 E0 | ok0 ok1 ok1 err | ok0 ok0 err ok0 +C B0 E1 E1 | ok0 ok1 ok1 ok1 | ok0 ok0 err err +C B0 E1 X0 | ok0 ok1 ok1 ok0 | ok0 ok0 err ok0 +C B0 E1 X1 | ok0 ok1 ok1 ok1 | ok0 ok0 err ok1 +C B0 X0 C | ok0 ok1 ok0 ok2 | ok0 ok0 ok0 ok1 +C B0 X0 B0 | ok0 ok1 ok0 err | ok0 ok0 ok0 err +C B0 X0 B1 | ok0 ok1 ok0 ok2 | ok0 ok0 ok0 err +C B0 X0 E0 | ok0 ok1 ok0 err | ok0 ok0 ok0 err +C B0 X0 E1 | ok0 ok1 ok0 ok1 | ok0 ok0 ok0 err +C B0 X0 X0 | ok0 ok1 ok0 ok0 | ok0 ok0 ok0 ok0 +C B0 X0 X1 | ok0 ok1 ok0 ok1 | ok0 ok0 ok0 ok1 +C B0 X1 C | ok0 ok1 ok1 ok2 | ok0 ok0 ok1 ok1 +C B0 X1 B0 | ok0 ok1 ok1 err | ok0 ok0 ok1 ok0 +C B0 X1 B1 | ok0 ok1 ok1 err | ok0 ok0 ok1 err +C B0 X1 E0 | ok0 ok1 ok1 err | ok0 ok0 ok1 ok0 +C B0 X1 E1 | ok0 ok1 ok1 err | ok0 ok0 ok1 err +C B0 X1 X0 | ok0 ok1 ok1 ok0 | ok0 ok0 ok1 ok0 +C B0 X1 X1 | ok0 ok1 ok1 ok1 | ok0 ok0 ok1 ok1 +C B1 C C | ok0 err ok1 ok2 | ok0 err ok1 ok2 +C B1 C B0 | ok0 err ok1 ok2 | ok0 err ok1 ok0 +C B1 C B1 | ok0 err ok1 ok2 | ok0 err ok1 ok1 +C B1 C E0 | ok0 err ok1 ok0 | ok0 err ok1 ok0 +C B1 C E1 | ok0 err ok1 ok1 | ok0 err ok1 ok1 +C B1 C X0 | ok0 err ok1 ok0 | ok0 err ok1 ok0 +C B1 C X1 | ok0 err ok1 ok1 | ok0 err ok1 ok1 +C B1 B0 C | ok0 err ok1 ok2 | ok0 err ok0 ok1 +C B1 B0 B0 | ok0 err ok1 err | ok0 err ok0 ok0 +C B1 B0 B1 | ok0 err ok1 ok2 | ok0 err ok0 err +C B1 B0 E0 | ok0 err ok1 err | ok0 err ok0 ok0 +C B1 B0 E1 | ok0 err ok1 ok1 | ok0 err ok0 err +C B1 B0 X0 | ok0 err ok1 ok0 | ok0 err ok0 ok0 +C B1 B0 X1 | ok0 err ok1 ok1 | ok0 err ok0 ok1 +C B1 B1 C | ok0 err err ok1 | ok0 err err ok1 +C B1 B1 B0 | ok0 err err ok1 | ok0 err err ok0 +C B1 B1 B1 | ok0 err err err | ok0 err err err +C B1 B1 E0 | ok0 err err ok0 | ok0 err err ok0 +C B1 B1 E1 | ok0 err err err | ok0 err err err +C B1 B1 X0 | ok0 err err ok0 | ok0 err err ok0 +C B1 B1 X1 | ok0 err err ok1 | ok0 err err ok1 +C B1 E0 C | ok0 err ok0 ok1 | ok0 err ok0 ok1 +C B1 E0 B0 | ok0 err ok0 ok1 | ok0 err ok0 ok0 +C B1 E0 B1 | ok0 err ok0 err | ok0 err ok0 err +C B1 E0 E0 | ok0 err ok0 ok0 | ok0 err ok0 ok0 +C B1 E0 E1 | ok0 err ok0 err | ok0 err ok0 err +C B1 E0 X0 | ok0 err ok0 ok0 | ok0 err ok0 ok0 +C B1 E0 X1 | ok0 err ok0 ok1 | ok0 err ok0 ok1 +C B1 E1 C | ok0 err err ok1 | ok0 err err ok1 +C B1 E1 B0 | ok0 err err ok1 | ok0 err err ok0 +C B1 E1 B1 | ok0 err err err | ok0 err err err +C B1 E1 E0 | ok0 err err ok0 | ok0 err err ok0 +C B1 E1 E1 | ok0 err err err | ok0 err err err +C B1 E1 X0 | ok0 err err ok0 | ok0 err err ok0 +C B1 E1 X1 | ok0 err err ok1 | ok0 err err ok1 +C B1 X0 C | ok0 err ok0 ok1 | ok0 err ok0 ok1 +C B1 X0 B0 | ok0 err ok0 err | ok0 err ok0 err +C B1 X0 B1 | ok0 err ok0 err | ok0 err ok0 err +C B1 X0 E0 | ok0 err ok0 err | ok0 err ok0 err +C B1 X0 E1 | ok0 err ok0 err | ok0 err ok0 err +C B1 X0 X0 | ok0 err ok0 ok0 | ok0 err ok0 ok0 +C B1 X0 X1 | ok0 err ok0 ok1 | ok0 err ok0 ok1 +C B1 X1 C | ok0 err ok1 ok1 | ok0 err ok1 ok1 +C B1 X1 B0 | ok0 err ok1 ok1 | ok0 err ok1 ok0 +C B1 X1 B1 | ok0 err ok1 err | ok0 err ok1 err +C B1 X1 E0 | ok0 err ok1 ok0 | ok0 err ok1 ok0 +C B1 X1 E1 | ok0 err ok1 err | ok0 err ok1 err +C B1 X1 X0 | ok0 err ok1 ok0 | ok0 err ok1 ok0 +C B1 X1 X1 | ok0 err ok1 ok1 | ok0 err ok1 ok1 +C E0 C C | ok0 ok0 ok1 ok2 | ok0 ok0 ok1 ok2 +C E0 C B0 | ok0 ok0 ok1 ok2 | ok0 ok0 ok1 ok0 +C E0 C B1 | ok0 ok0 ok1 ok2 | ok0 ok0 ok1 ok1 +C E0 C E0 | ok0 ok0 ok1 ok0 | ok0 ok0 ok1 ok0 +C E0 C E1 | ok0 ok0 ok1 ok1 | ok0 ok0 ok1 ok1 +C E0 C X0 | ok0 ok0 ok1 ok0 | ok0 ok0 ok1 ok0 +C E0 C X1 | ok0 ok0 ok1 ok1 | ok0 ok0 ok1 ok1 +C E0 B0 C | ok0 ok0 ok1 ok2 | ok0 ok0 ok0 ok1 +C E0 B0 B0 | ok0 ok0 ok1 err | ok0 ok0 ok0 ok0 +C E0 B0 B1 | ok0 ok0 ok1 ok2 | ok0 ok0 ok0 err +C E0 B0 E0 | ok0 ok0 ok1 err | ok0 ok0 ok0 ok0 +C E0 B0 E1 | ok0 ok0 ok1 ok1 | ok0 ok0 ok0 err +C E0 B0 X0 | ok0 ok0 ok1 ok0 | ok0 ok0 ok0 ok0 +C E0 B0 X1 | ok0 ok0 ok1 ok1 | ok0 ok0 ok0 ok1 +C E0 B1 C | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C E0 B1 B0 | ok0 ok0 err ok1 | ok0 ok0 err ok0 +C E0 B1 B1 | ok0 ok0 err err | ok0 ok0 err err +C E0 B1 E0 | ok0 ok0 err ok0 | ok0 ok0 err ok0 +C E0 B1 E1 | ok0 ok0 err err | ok0 ok0 err err +C E0 B1 X0 | ok0 ok0 err ok0 | ok0 ok0 err ok0 +C E0 B1 X1 | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C E0 E0 C | ok0 ok0 ok0 ok1 | ok0 ok0 ok0 ok1 +C E0 E0 B0 | ok0 ok0 ok0 ok1 | ok0 ok0 ok0 ok0 +C E0 E0 B1 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C E0 E0 E0 | ok0 ok0 ok0 ok0 | ok0 ok0 ok0 ok0 +C E0 E0 E1 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C E0 E0 X0 | ok0 ok0 ok0 ok0 | ok0 ok0 ok0 ok0 +C E0 E0 X1 | ok0 ok0 ok0 ok1 | ok0 ok0 ok0 ok1 +C E0 E1 C | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C E0 E1 B0 | ok0 ok0 err ok1 | ok0 ok0 err ok0 +C E0 E1 B1 | ok0 ok0 err err | ok0 ok0 err err +C E0 E1 E0 | ok0 ok0 err ok0 | ok0 ok0 err ok0 +C E0 E1 E1 | ok0 ok0 err err | ok0 ok0 err err +C E0 E1 X0 | ok0 ok0 err ok0 | ok0 ok0 err ok0 +C E0 E1 X1 | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C E0 X0 C | ok0 ok0 ok0 ok1 | ok0 ok0 ok0 ok1 +C E0 X0 B0 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C E0 X0 B1 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C E0 X0 E0 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C E0 X0 E1 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C E0 X0 X0 | ok0 ok0 ok0 ok0 | ok0 ok0 ok0 ok0 +C E0 X0 X1 | ok0 ok0 ok0 ok1 | ok0 ok0 ok0 ok1 +C E0 X1 C | ok0 ok0 ok1 ok1 | ok0 ok0 ok1 ok1 +C E0 X1 B0 | ok0 ok0 ok1 ok1 | ok0 ok0 ok1 ok0 +C E0 X1 B1 | ok0 ok0 ok1 err | ok0 ok0 ok1 err +C E0 X1 E0 | ok0 ok0 ok1 ok0 | ok0 ok0 ok1 ok0 +C E0 X1 E1 | ok0 ok0 ok1 err | ok0 ok0 ok1 err +C E0 X1 X0 | ok0 ok0 ok1 ok0 | ok0 ok0 ok1 ok0 +C E0 X1 X1 | ok0 ok0 ok1 ok1 | ok0 ok0 ok1 ok1 +C E1 C C | ok0 err ok1 ok2 | ok0 err ok1 ok2 +C E1 C B0 | ok0 err ok1 ok2 | ok0 err ok1 ok0 +C E1 C B1 | ok0 err ok1 ok2 | ok0 err ok1 ok1 +C E1 C E0 | ok0 err ok1 ok0 | ok0 err ok1 ok0 +C E1 C E1 | ok0 err ok1 ok1 | ok0 err ok1 ok1 +C E1 C X0 | ok0 err ok1 ok0 | ok0 err ok1 ok0 +C E1 C X1 | ok0 err ok1 ok1 | ok0 err ok1 ok1 +C E1 B0 C | ok0 err ok1 ok2 | ok0 err ok0 ok1 +C E1 B0 B0 | ok0 err ok1 err | ok0 err ok0 ok0 +C E1 B0 B1 | ok0 err ok1 ok2 | ok0 err ok0 err +C E1 B0 E0 | ok0 err ok1 err | ok0 err ok0 ok0 +C E1 B0 E1 | ok0 err ok1 ok1 | ok0 err ok0 err +C E1 B0 X0 | ok0 err ok1 ok0 | ok0 err ok0 ok0 +C E1 B0 X1 | ok0 err ok1 ok1 | ok0 err ok0 ok1 +C E1 B1 C | ok0 err err ok1 | ok0 err err ok1 +C E1 B1 B0 | ok0 err err ok1 | ok0 err err ok0 +C E1 B1 B1 | ok0 err err err | ok0 err err err +C E1 B1 E0 | ok0 err err ok0 | ok0 err err ok0 +C E1 B1 E1 | ok0 err err err | ok0 err err err +C E1 B1 X0 | ok0 err err ok0 | ok0 err err ok0 +C E1 B1 X1 | ok0 err err ok1 | ok0 err err ok1 +C E1 E0 C | ok0 err ok0 ok1 | ok0 err ok0 ok1 +C E1 E0 B0 | ok0 err ok0 ok1 | ok0 err ok0 ok0 +C E1 E0 B1 | ok0 err ok0 err | ok0 err ok0 err +C E1 E0 E0 | ok0 err ok0 ok0 | ok0 err ok0 ok0 +C E1 E0 E1 | ok0 err ok0 err | ok0 err ok0 err +C E1 E0 X0 | ok0 err ok0 ok0 | ok0 err ok0 ok0 +C E1 E0 X1 | ok0 err ok0 ok1 | ok0 err ok0 ok1 +C E1 E1 C | ok0 err err ok1 | ok0 err err ok1 +C E1 E1 B0 | ok0 err err ok1 | ok0 err err ok0 +C E1 E1 B1 | ok0 err err err | ok0 err err err +C E1 E1 E0 | ok0 err err ok0 | ok0 err err ok0 +C E1 E1 E1 | ok0 err err err | ok0 err err err +C E1 E1 X0 | ok0 err err ok0 | ok0 err err ok0 +C E1 E1 X1 | ok0 err err ok1 | ok0 err err ok1 +C E1 X0 C | ok0 err ok0 ok1 | ok0 err ok0 ok1 +C E1 X0 B0 | ok0 err ok0 err | ok0 err ok0 err +C E1 X0 B1 | ok0 err ok0 err | ok0 err ok0 err +C E1 X0 E0 | ok0 err ok0 err | ok0 err ok0 err +C E1 X0 E1 | ok0 err ok0 err | ok0 err ok0 err +C E1 X0 X0 | ok0 err ok0 ok0 | ok0 err ok0 ok0 +C E1 X0 X1 | ok0 err ok0 ok1 | ok0 err ok0 ok1 +C E1 X1 C | ok0 err ok1 ok1 | ok0 err ok1 ok1 +C E1 X1 B0 | ok0 err ok1 ok1 | ok0 err ok1 ok0 +C E1 X1 B1 | ok0 err ok1 err | ok0 err ok1 err +C E1 X1 E0 | ok0 err ok1 ok0 | ok0 err ok1 ok0 +C E1 X1 E1 | ok0 err ok1 err | ok0 err ok1 err +C E1 X1 X0 | ok0 err ok1 ok0 | ok0 err ok1 ok0 +C E1 X1 X1 | ok0 err ok1 ok1 | ok0 err ok1 ok1 +C X0 C C | ok0 ok0 ok1 ok2 | ok0 ok0 ok1 ok2 +C X0 C B0 | ok0 ok0 ok1 err | ok0 ok0 ok1 err +C X0 C B1 | ok0 ok0 ok1 ok2 | ok0 ok0 ok1 ok1 +C X0 C E0 | ok0 ok0 ok1 err | ok0 ok0 ok1 err +C X0 C E1 | ok0 ok0 ok1 ok1 | ok0 ok0 ok1 ok1 +C X0 C X0 | ok0 ok0 ok1 ok0 | ok0 ok0 ok1 ok0 +C X0 C X1 | ok0 ok0 ok1 ok1 | ok0 ok0 ok1 ok1 +C X0 B0 C | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C X0 B0 B0 | ok0 ok0 err err | ok0 ok0 err err +C X0 B0 B1 | ok0 ok0 err err | ok0 ok0 err err +C X0 B0 E0 | ok0 ok0 err err | ok0 ok0 err err +C X0 B0 E1 | ok0 ok0 err err | ok0 ok0 err err +C X0 B0 X0 | ok0 ok0 err ok0 | ok0 ok0 err ok0 +C X0 B0 X1 | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C X0 B1 C | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C X0 B1 B0 | ok0 ok0 err err | ok0 ok0 err err +C X0 B1 B1 | ok0 ok0 err err | ok0 ok0 err err +C X0 B1 E0 | ok0 ok0 err err | ok0 ok0 err err +C X0 B1 E1 | ok0 ok0 err err | ok0 ok0 err err +C X0 B1 X0 | ok0 ok0 err ok0 | ok0 ok0 err ok0 +C X0 B1 X1 | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C X0 E0 C | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C X0 E0 B0 | ok0 ok0 err err | ok0 ok0 err err +C X0 E0 B1 | ok0 ok0 err err | ok0 ok0 err err +C X0 E0 E0 | ok0 ok0 err err | ok0 ok0 err err +C X0 E0 E1 | ok0 ok0 err err | ok0 ok0 err err +C X0 E0 X0 | ok0 ok0 err ok0 | ok0 ok0 err ok0 +C X0 E0 X1 | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C X0 E1 C | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C X0 E1 B0 | ok0 ok0 err err | ok0 ok0 err err +C X0 E1 B1 | ok0 ok0 err err | ok0 ok0 err err +C X0 E1 E0 | ok0 ok0 err err | ok0 ok0 err err +C X0 E1 E1 | ok0 ok0 err err | ok0 ok0 err err +C X0 E1 X0 | ok0 ok0 err ok0 | ok0 ok0 err ok0 +C X0 E1 X1 | ok0 ok0 err ok1 | ok0 ok0 err ok1 +C X0 X0 C | ok0 ok0 ok0 ok1 | ok0 ok0 ok0 ok1 +C X0 X0 B0 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C X0 X0 B1 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C X0 X0 E0 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C X0 X0 E1 | ok0 ok0 ok0 err | ok0 ok0 ok0 err +C X0 X0 X0 | ok0 ok0 ok0 ok0 | ok0 ok0 ok0 ok0 +C X0 X0 X1 | ok0 ok0 ok0 ok1 | ok0 ok0 ok0 ok1 +C X0 X1 C | ok0 ok0 ok1 ok1 | ok0 ok0 ok1 ok1 +C X0 X1 B0 | ok0 ok0 ok1 err | ok0 ok0 ok1 err +C X0 X1 B1 | ok0 ok0 ok1 err | ok0 ok0 ok1 err +C X0 X1 E0 | ok0 ok0 ok1 err | ok0 ok0 ok1 err +C X0 X1 E1 | ok0 ok0 ok1 err | ok0 ok0 ok1 err +C X0 X1 X0 | ok0 ok0 ok1 ok0 | ok0 ok0 ok1 ok0 +C X0 X1 X1 | ok0 ok0 ok1 ok1 | ok0 ok0 ok1 ok1 +C X1 C C | ok0 ok1 ok1 ok2 | ok0 ok1 ok1 ok2 +C X1 C B0 | ok0 ok1 ok1 ok2 | ok0 ok1 ok1 ok0 +C X1 C B1 | ok0 ok1 ok1 ok2 | ok0 ok1 ok1 ok1 +C X1 C E0 | ok0 ok1 ok1 ok0 | ok0 ok1 ok1 ok0 +C X1 C E1 | ok0 ok1 ok1 ok1 | ok0 ok1 ok1 ok1 +C X1 C X0 | ok0 ok1 ok1 ok0 | ok0 ok1 ok1 ok0 +C X1 C X1 | ok0 ok1 ok1 ok1 | ok0 ok1 ok1 ok1 +C X1 B0 C | ok0 ok1 ok1 ok2 | ok0 ok1 ok0 ok1 +C X1 B0 B0 | ok0 ok1 ok1 err | ok0 ok1 ok0 ok0 +C X1 B0 B1 | ok0 ok1 ok1 ok2 | ok0 ok1 ok0 err +C X1 B0 E0 | ok0 ok1 ok1 err | ok0 ok1 ok0 ok0 +C X1 B0 E1 | ok0 ok1 ok1 ok1 | ok0 ok1 ok0 err +C X1 B0 X0 | ok0 ok1 ok1 ok0 | ok0 ok1 ok0 ok0 +C X1 B0 X1 | ok0 ok1 ok1 ok1 | ok0 ok1 ok0 ok1 +C X1 B1 C | ok0 ok1 err ok1 | ok0 ok1 err ok1 +C X1 B1 B0 | ok0 ok1 err ok1 | ok0 ok1 err ok0 +C X1 B1 B1 | ok0 ok1 err err | ok0 ok1 err err +C X1 B1 E0 | ok0 ok1 err ok0 | ok0 ok1 err ok0 +C X1 B1 E1 | ok0 ok1 err err | ok0 ok1 err err +C X1 B1 X0 | ok0 ok1 err ok0 | ok0 ok1 err ok0 +C X1 B1 X1 | ok0 ok1 err ok1 | ok0 ok1 err ok1 +C X1 E0 C | ok0 ok1 ok0 ok1 | ok0 ok1 ok0 ok1 +C X1 E0 B0 | ok0 ok1 ok0 ok1 | ok0 ok1 ok0 ok0 +C X1 E0 B1 | ok0 ok1 ok0 err | ok0 ok1 ok0 err +C X1 E0 E0 | ok0 ok1 ok0 ok0 | ok0 ok1 ok0 ok0 +C X1 E0 E1 | ok0 ok1 ok0 err | ok0 ok1 ok0 err +C X1 E0 X0 | ok0 ok1 ok0 ok0 | ok0 ok1 ok0 ok0 +C X1 E0 X1 | ok0 ok1 ok0 ok1 | ok0 ok1 ok0 ok1 +C X1 E1 C | ok0 ok1 err ok1 | ok0 ok1 err ok1 +C X1 E1 B0 | ok0 ok1 err ok1 | ok0 ok1 err ok0 +C X1 E1 B1 | ok0 ok1 err err | ok0 ok1 err err +C X1 E1 E0 | ok0 ok1 err ok0 | ok0 ok1 err ok0 +C X1 E1 E1 | ok0 ok1 err err | ok0 ok1 err err +C X1 E1 X0 | ok0 ok1 err ok0 | ok0 ok1 err ok0 +C X1 E1 X1 | ok0 ok1 err ok1 | ok0 ok1 err ok1 +C X1 X0 C | ok0 ok1 ok0 ok1 | ok0 ok1 ok0 ok1 +C X1 X0 B0 | ok0 ok1 ok0 err | ok0 ok1 ok0 err +C X1 X0 B1 | ok0 ok1 ok0 err | ok0 ok1 ok0 err +C X1 X0 E0 | ok0 ok1 ok0 err | ok0 ok1 ok0 err +C X1 X0 E1 | ok0 ok1 ok0 err | ok0 ok1 ok0 err +C X1 X0 X0 | ok0 ok1 ok0 ok0 | ok0 ok1 ok0 ok0 +C X1 X0 X1 | ok0 ok1 ok0 ok1 | ok0 ok1 ok0 ok1 +C X1 X1 C | ok0 ok1 ok1 ok1 | ok0 ok1 ok1 ok1 +C X1 X1 B0 | ok0 ok1 ok1 ok1 | ok0 ok1 ok1 ok0 +C X1 X1 B1 | ok0 ok1 ok1 err | ok0 ok1 ok1 err +C X1 X1 E0 | ok0 ok1 ok1 ok0 | ok0 ok1 ok1 ok0 +C X1 X1 E1 | ok0 ok1 ok1 err | ok0 ok1 ok1 err +C X1 X1 X0 | ok0 ok1 ok1 ok0 | ok0 ok1 ok1 ok0 +C X1 X1 X1 | ok0 ok1 ok1 ok1 | ok0 ok1 ok1 ok1 +C B0 C C C | ok0 ok1 ok2 ok3 ok4 | ok0 ok0 ok1 ok2 ok3 +C B0 C C B0 | ok0 ok1 ok2 ok3 err | ok0 ok0 ok1 ok2 ok0 +C B0 C C B1 | ok0 ok1 ok2 ok3 ok4 | ok0 ok0 ok1 ok2 ok1 +C B0 C C E0 | ok0 ok1 ok2 ok3 err | ok0 ok0 ok1 ok2 ok0 +C B0 C C E1 | ok0 ok1 ok2 ok3 ok1 | ok0 ok0 ok1 ok2 ok1 +C B0 C C X0 | ok0 ok1 ok2 ok3 ok0 | ok0 ok0 ok1 ok2 ok0 +C B0 C C X1 | ok0 ok1 ok2 ok3 ok1 | ok0 ok0 ok1 ok2 ok1 +C B0 C B0 C | ok0 ok1 ok2 err ok3 | ok0 ok0 ok1 ok0 ok2 +C B0 C B0 B0 | ok0 ok1 ok2 err err | ok0 ok0 ok1 ok0 ok0 +C B0 C B0 B1 | ok0 ok1 ok2 err ok3 | ok0 ok0 ok1 ok0 ok1 +C B0 C B0 E0 | ok0 ok1 ok2 err err | ok0 ok0 ok1 ok0 ok0 +C B0 C B0 E1 | ok0 ok1 ok2 err ok1 | ok0 ok0 ok1 ok0 ok1 +C B0 C B0 X0 | ok0 ok1 ok2 err ok0 | ok0 ok0 ok1 ok0 ok0 +C B0 C B0 X1 | ok0 ok1 ok2 err ok1 | ok0 ok0 ok1 ok0 ok1 +C B0 C B1 C | ok0 ok1 ok2 ok3 ok4 | ok0 ok0 ok1 ok1 ok2 +C B0 C B1 B0 | ok0 ok1 ok2 ok3 err | ok0 ok0 ok1 ok1 ok0 +C B0 C B1 B1 | ok0 ok1 ok2 ok3 err | ok0 ok0 ok1 ok1 ok1 +C B0 C B1 E0 | ok0 ok1 ok2 ok3 err | ok0 ok0 ok1 ok1 ok0 +C B0 C B1 E1 | ok0 ok1 ok2 ok3 err | ok0 ok0 ok1 ok1 ok1 +C B0 C B1 X0 | ok0 ok1 ok2 ok3 ok0 | ok0 ok0 ok1 ok1 ok0 +C B0 C B1 X1 | ok0 ok1 ok2 ok3 ok1 | ok0 ok0 ok1 ok1 ok1 +C B0 C E0 C | ok0 ok1 ok2 err ok3 | ok0 ok0 ok1 ok0 ok2 +C B0 C E0 B0 | ok0 ok1 ok2 err err | ok0 ok0 ok1 ok0 ok0 +C B0 C E0 B1 | ok0 ok1 ok2 err ok3 | ok0 ok0 ok1 ok0 ok1 +C B0 C E0 E0 | ok0 ok1 ok2 err err | ok0 ok0 ok1 ok0 ok0 +C B0 C E0 E1 | ok0 ok1 ok2 err ok1 | ok0 ok0 ok1 ok0 ok1 +C B0 C E0 X0 | ok0 ok1 ok2 err ok0 | ok0 ok0 ok1 ok0 ok0 +C B0 C E0 X1 | ok0 ok1 ok2 err ok1 | ok0 ok0 ok1 ok0 ok1 +C B0 C E1 C | ok0 ok1 ok2 ok1 ok3 | ok0 ok0 ok1 ok1 ok2 +C B0 C E1 B0 | ok0 ok1 ok2 ok1 err | ok0 ok0 ok1 ok1 ok0 +C B0 C E1 B1 | ok0 ok1 ok2 ok1 ok3 | ok0 ok0 ok1 ok1 ok1 +C B0 C E1 E0 | ok0 ok1 ok2 ok1 err | ok0 ok0 ok1 ok1 ok0 +C B0 C E1 E1 | ok0 ok1 ok2 ok1 ok1 | ok0 ok0 ok1 ok1 ok1 +C B0 C E1 X0 | ok0 ok1 ok2 ok1 ok0 | ok0 ok0 ok1 ok1 ok0 +C B0 C E1 X1 | ok0 ok1 ok2 ok1 ok1 | ok0 ok0 ok1 ok1 ok1 +C B0 C X0 C | ok0 ok1 ok2 ok0 ok3 | ok0 ok0 ok1 ok0 ok2 +C B0 C X0 B0 | ok0 ok1 ok2 ok0 err | ok0 ok0 ok1 ok0 err +C B0 C X0 B1 | ok0 ok1 ok2 ok0 ok3 | ok0 ok0 ok1 ok0 ok1 +C B0 C X0 E0 | ok0 ok1 ok2 ok0 err | ok0 ok0 ok1 ok0 err +C B0 C X0 E1 | ok0 ok1 ok2 ok0 ok1 | ok0 ok0 ok1 ok0 ok1 +C B0 C X0 X0 | ok0 ok1 ok2 ok0 ok0 | ok0 ok0 ok1 ok0 ok0 +C B0 C X0 X1 | ok0 ok1 ok2 ok0 ok1 | ok0 ok0 ok1 ok0 ok1 +C B0 C X1 C | ok0 ok1 ok2 ok1 ok3 | ok0 ok0 ok1 ok1 ok2 +C B0 C X1 B0 | ok0 ok1 ok2 ok1 err | ok0 ok0 ok1 ok1 ok0 +C B0 C X1 B1 | ok0 ok1 ok2 ok1 err | ok0 ok0 ok1 ok1 err +C B0 C X1 E0 | ok0 ok1 ok2 ok1 err | ok0 ok0 ok1 ok1 ok0 +C B0 C X1 E1 | ok0 ok1 ok2 ok1 err | ok0 ok0 ok1 ok1 err +C B0 C X1 X0 | ok0 ok1 ok2 ok1 ok0 | ok0 ok0 ok1 ok1 ok0 +C B0 C X1 X1 | ok0 ok1 ok2 ok1 ok1 | ok0 ok0 ok1 ok1 ok1 +C B0 B0 C C | ok0 ok1 err ok2 ok3 | ok0 ok0 ok0 ok1 ok2 +C B0 B0 C B0 | ok0 ok1 err ok2 err | ok0 ok0 ok0 ok1 ok0 +C B0 B0 C B1 | ok0 ok1 err ok2 ok3 | ok0 ok0 ok0 ok1 ok1 +C B0 B0 C E0 | ok0 ok1 err ok2 err | ok0 ok0 ok0 ok1 ok0 +C B0 B0 C E1 | ok0 ok1 err ok2 ok1 | ok0 ok0 ok0 ok1 ok1 +C B0 B0 C X0 | ok0 ok1 err ok2 ok0 | ok0 ok0 ok0 ok1 ok0 +C B0 B0 C X1 | ok0 ok1 err ok2 ok1 | ok0 ok0 ok0 ok1 ok1 +C B0 B0 B0 C | ok0 ok1 err err ok2 | ok0 ok0 ok0 ok0 ok1 +C B0 B0 B0 B0 | ok0 ok1 err err err | ok0 ok0 ok0 ok0 ok0 +C B0 B0 B0 B1 | ok0 ok1 err err ok2 | ok0 ok0 ok0 ok0 err +C B0 B0 B0 E0 | ok0 ok1 err err err | ok0 ok0 ok0 ok0 ok0 +C B0 B0 B0 E1 | ok0 ok1 err err ok1 | ok0 ok0 ok0 ok0 err +C B0 B0 B0 X0 | ok0 ok1 err err ok0 | ok0 ok0 ok0 ok0 ok0 +C B0 B0 B0 X1 | ok0 ok1 err err ok1 | ok0 ok0 ok0 ok0 ok1 +C B0 B0 B1 C | ok0 ok1 err ok2 ok3 | ok0 ok0 ok0 err ok1 +C B0 B0 B1 B0 | ok0 ok1 err ok2 err | ok0 ok0 ok0 err ok0 +C B0 B0 B1 B1 | ok0 ok1 err ok2 err | ok0 ok0 ok0 err err +C B0 B0 B1 E0 | ok0 ok1 err ok2 err | ok0 ok0 ok0 err ok0 +C B0 B0 B1 E1 | ok0 ok1 err ok2 err | ok0 ok0 ok0 err err +C B0 B0 B1 X0 | ok0 ok1 err ok2 ok0 | ok0 ok0 ok0 err ok0 +C B0 B0 B1 X1 | ok0 ok1 err ok2 ok1 | ok0 ok0 ok0 err ok1 +C B0 B0 E0 C | ok0 ok1 err err ok2 | ok0 ok0 ok0 ok0 ok1 +C B0 B0 E0 B0 | ok0 ok1 err err err | ok0 ok0 ok0 ok0 ok0 +C B0 B0 E0 B1 | ok0 ok1 err err ok2 | ok0 ok0 ok0 ok0 err +C B0 B0 E0 E0 | ok0 ok1 err err err | ok0 ok0 ok0 ok0 ok0 +C B0 B0 E0 E1 | ok0 ok1 err err ok1 | ok0 ok0 ok0 ok0 err +C B0 B0 E0 X0 | ok0 ok1 err err ok0 | ok0 ok0 ok0 ok0 ok0 +C B0 B0 E0 X1 | ok0 ok1 err err ok1 | ok0 ok0 ok0 ok0 ok1 +C B0 B0 E1 C | ok0 ok1 err ok1 ok2 | ok0 ok0 ok0 err ok1 +C B0 B0 E1 B0 | ok0 ok1 err ok1 err | ok0 ok0 ok0 err ok0 +C B0 B0 E1 B1 | ok0 ok1 err ok1 ok2 | ok0 ok0 ok0 err err +C B0 B0 E1 E0 | ok0 ok1 err ok1 err | ok0 ok0 ok0 err ok0 +C B0 B0 E1 E1 | ok0 ok1 err ok1 ok1 | ok0 ok0 ok0 err err +C B0 B0 E1 X0 | ok0 ok1 err ok1 ok0 | ok0 ok0 ok0 err ok0 +C B0 B0 E1 X1 | ok0 ok1 err ok1 ok1 | ok0 ok0 ok0 err ok1 +C B0 B0 X0 C | ok0 ok1 err ok0 ok2 | ok0 ok0 ok0 ok0 ok1 +C B0 B0 X0 B0 | ok0 ok1 err ok0 err | ok0 ok0 ok0 ok0 err +C B0 B0 X0 B1 | ok0 ok1 err ok0 ok2 | ok0 ok0 ok0 ok0 err +C B0 B0 X0 E0 | ok0 ok1 err ok0 err | ok0 ok0 ok0 ok0 err +C B0 B0 X0 E1 | ok0 ok1 err ok0 ok1 | ok0 ok0 ok0 ok0 err +C B0 B0 X0 X0 | ok0 ok1 err ok0 ok0 | ok0 ok0 ok0 ok0 ok0 +C B0 B0 X0 X1 | ok0 ok1 err ok0 ok1 | ok0 ok0 ok0 ok0 ok1 +C B0 B0 X1 C | ok0 ok1 err ok1 ok2 | ok0 ok0 ok0 ok1 ok1 +C B0 B0 X1 B0 | ok0 ok1 err ok1 err | ok0 ok0 ok0 ok1 ok0 +C B0 B0 X1 B1 | ok0 ok1 err ok1 err | ok0 ok0 ok0 ok1 err +C B0 B0 X1 E0 | ok0 ok1 err ok1 err | ok0 ok0 ok0 ok1 ok0 +C B0 B0 X1 E1 | ok0 ok1 err ok1 err | ok0 ok0 ok0 ok1 err +C B0 B0 X1 X0 | ok0 ok1 err ok1 ok0 | ok0 ok0 ok0 ok1 ok0 +C B0 B0 X1 X1 | ok0 ok1 err ok1 ok1 | ok0 ok0 ok0 ok1 ok1 +C B0 B1 C C | ok0 ok1 ok2 ok3 ok4 | ok0 ok0 err ok1 ok2 +C B0 B1 C B0 | ok0 ok1 ok2 ok3 err | ok0 ok0 err ok1 ok0 +C B0 B1 C B1 | ok0 ok1 ok2 ok3 err | ok0 ok0 err ok1 ok1 +C B0 B1 C E0 | ok0 ok1 ok2 ok3 err | ok0 ok0 err ok1 ok0 +C B0 B1 C E1 | ok0 ok1 ok2 ok3 err | ok0 ok0 err ok1 ok1 +C B0 B1 C X0 | ok0 ok1 ok2 ok3 ok0 | ok0 ok0 err ok1 ok0 +C B0 B1 C X1 | ok0 ok1 ok2 ok3 ok1 | ok0 ok0 err ok1 ok1 +C B0 B1 B0 C | ok0 ok1 ok2 err ok3 | ok0 ok0 err ok0 ok1 +C B0 B1 B0 B0 | ok0 ok1 ok2 err err | ok0 ok0 err ok0 ok0 +C B0 B1 B0 B1 | ok0 ok1 ok2 err err | ok0 ok0 err ok0 err +C B0 B1 B0 E0 | ok0 ok1 ok2 err err | ok0 ok0 err ok0 ok0 +C B0 B1 B0 E1 | ok0 ok1 ok2 err err | ok0 ok0 err ok0 err +C B0 B1 B0 X0 | ok0 ok1 ok2 err ok0 | ok0 ok0 err ok0 ok0 +C B0 B1 B0 X1 | ok0 ok1 ok2 err ok1 | ok0 ok0 err ok0 ok1 +C B0 B1 B1 C | ok0 ok1 ok2 err ok3 | ok0 ok0 err err ok1 +C B0 B1 B1 B0 | ok0 ok1 ok2 err err | ok0 ok0 err err ok0 +C B0 B1 B1 B1 | ok0 ok1 ok2 err err | ok0 ok0 err err err +C B0 B1 B1 E0 | ok0 ok1 ok2 err err | ok0 ok0 err err ok0 +C B0 B1 B1 E1 | ok0 ok1 ok2 err err | ok0 ok0 err err err +C B0 B1 B1 X0 | ok0 ok1 ok2 err ok0 | ok0 ok0 err err ok0 +C B0 B1 B1 X1 | ok0 ok1 ok2 err ok1 | ok0 ok0 err err ok1 +C B0 B1 E0 C | ok0 ok1 ok2 err ok3 | ok0 ok0 err ok0 ok1 +C B0 B1 E0 B0 | ok0 ok1 ok2 err err | ok0 ok0 err ok0 ok0 +C B0 B1 E0 B1 | ok0 ok1 ok2 err err | ok0 ok0 err ok0 err +C B0 B1 E0 E0 | ok0 ok1 ok2 err err | ok0 ok0 err ok0 ok0 +C B0 B1 E0 E1 | ok0 ok1 ok2 err err | ok0 ok0 err ok0 err +C B0 B1 E0 X0 | ok0 ok1 ok2 err ok0 | ok0 ok0 err ok0 ok0 +C B0 B1 E0 X1 | ok0 ok1 ok2 err ok1 | ok0 ok0 err ok0 ok1 +C B0 B1 E1 C | ok0 ok1 ok2 err ok3 | ok0 ok0 err err ok1 +C B0 B1 E1 B0 | ok0 ok1 ok2 err err | ok0 ok0 err err ok0 +C B0 B1 E1 B1 | ok0 ok1 ok2 err err | ok0 ok0 err err err +C B0 B1 E1 E0 | ok0 ok1 ok2 err err | ok0 ok0 err err ok0 +C B0 B1 E1 E1 | ok0 ok1 ok2 err err | ok0 ok0 err err err +C B0 B1 E1 X0 | ok0 ok1 ok2 err ok0 | ok0 ok0 err err ok0 +C B0 B1 E1 X1 | ok0 ok1 ok2 err ok1 | ok0 ok0 err err ok1 +C B0 B1 X0 C | ok0 ok1 ok2 ok0 ok3 | ok0 ok0 err ok0 ok1 +C B0 B1 X0 B0 | ok0 ok1 ok2 ok0 err | ok0 ok0 err ok0 err +C B0 B1 X0 B1 | ok0 ok1 ok2 ok0 err | ok0 ok0 err ok0 err +C B0 B1 X0 E0 | ok0 ok1 ok2 ok0 err | ok0 ok0 err ok0 err +C B0 B1 X0 E1 | ok0 ok1 ok2 ok0 err | ok0 ok0 err ok0 err +C B0 B1 X0 X0 | ok0 ok1 ok2 ok0 ok0 | ok0 ok0 err ok0 ok0 +C B0 B1 X0 X1 | ok0 ok1 ok2 ok0 ok1 | ok0 ok0 err ok0 ok1 +C B0 B1 X1 C | ok0 ok1 ok2 ok1 ok3 | ok0 ok0 err ok1 ok1 +C B0 B1 X1 B0 | ok0 ok1 ok2 ok1 err | ok0 ok0 err ok1 ok0 +C B0 B1 X1 B1 | ok0 ok1 ok2 ok1 err | ok0 ok0 err ok1 err +C B0 B1 X1 E0 | ok0 ok1 ok2 ok1 err | ok0 ok0 err ok1 ok0 +C B0 B1 X1 E1 | ok0 ok1 ok2 ok1 err | ok0 ok0 err ok1 err +C B0 B1 X1 X0 | ok0 ok1 ok2 ok1 ok0 | ok0 ok0 err ok1 ok0 +C B0 B1 X1 X1 | ok0 ok1 ok2 ok1 ok1 | ok0 ok0 err ok1 ok1 +C B0 E0 C C | ok0 ok1 err ok2 ok3 | ok0 ok0 ok0 ok1 ok2 +C B0 E0 C B0 | ok0 ok1 err ok2 err | ok0 ok0 ok0 ok1 ok0 +C B0 E0 C B1 | ok0 ok1 err ok2 ok3 | ok0 ok0 ok0 ok1 ok1 +C B0 E0 C E0 | ok0 ok1 err ok2 err | ok0 ok0 ok0 ok1 ok0 +C B0 E0 C E1 | ok0 ok1 err ok2 ok1 | ok0 ok0 ok0 ok1 ok1 +C B0 E0 C X0 | ok0 ok1 err ok2 ok0 | ok0 ok0 ok0 ok1 ok0 +C B0 E0 C X1 | ok0 ok1 err ok2 ok1 | ok0 ok0 ok0 ok1 ok1 +C B0 E0 B0 C | ok0 ok1 err err ok2 | ok0 ok0 ok0 ok0 ok1 +C B0 E0 B0 B0 | ok0 ok1 err err err | ok0 ok0 ok0 ok0 ok0 +C B0 E0 B0 B1 | ok0 ok1 err err ok2 | ok0 ok0 ok0 ok0 err +C B0 E0 B0 E0 | ok0 ok1 err err err | ok0 ok0 ok0 ok0 ok0 +C B0 E0 B0 E1 | ok0 ok1 err err ok1 | ok0 ok0 ok0 ok0 err +C B0 E0 B0 X0 | ok0 ok1 err err ok0 | ok0 ok0 ok0 ok0 ok0 +C B0 E0 B0 X1 | ok0 ok1 err err ok1 | ok0 ok0 ok0 ok0 ok1 +C B0 E0 B1 C | ok0 ok1 err ok2 ok3 | ok0 ok0 ok0 err ok1 +C B0 E0 B1 B0 | ok0 ok1 err ok2 err | ok0 ok0 ok0 err ok0 +C B0 E0 B1 B1 | ok0 ok1 err ok2 err | ok0 ok0 ok0 err err +C B0 E0 B1 E0 | ok0 ok1 err ok2 err | ok0 ok0 ok0 err ok0 +C B0 E0 B1 E1 | ok0 ok1 err ok2 err | ok0 ok0 ok0 err err +C B0 E0 B1 X0 | ok0 ok1 err ok2 ok0 | ok0 ok0 ok0 err ok0 +C B0 E0 B1 X1 | ok0 ok1 err ok2 ok1 | ok0 ok0 ok0 err ok1 +C B0 E0 E0 C | ok0 ok1 err err ok2 | ok0 ok0 ok0 ok0 ok1 +C B0 E0 E0 B0 | ok0 ok1 err err err | ok0 ok0 ok0 ok0 ok0 +C B0 E0 E0 B1 | ok0 ok1 err err ok2 | ok0 ok0 ok0 ok0 err +C B0 E0 E0 E0 | ok0 ok1 err err err | ok0 ok0 ok0 ok0 ok0 +C B0 E0 E0 E1 | ok0 ok1 err err ok1 | ok0 ok0 ok0 ok0 err +C B0 E0 E0 X0 | ok0 ok1 err err ok0 | ok0 ok0 ok0 ok0 ok0 +C B0 E0 E0 X1 | ok0 ok1 err err ok1 | ok0 ok0 ok0 ok0 ok1 +C B0 E0 E1 C | ok0 ok1 err ok1 ok2 | ok0 ok0 ok0 err ok1 +C B0 E0 E1 B0 | ok0 ok1 err ok1 err | ok0 ok0 ok0 err ok0 +C B0 E0 E1 B1 | ok0 ok1 err ok1 ok2 | ok0 ok0 ok0 err err +C B0 E0 E1 E0 | ok0 ok1 err ok1 err | ok0 ok0 ok0 err ok0 +C B0 E0 E1 E1 | ok0 ok1 err ok1 ok1 | ok0 ok0 ok0 err err +C B0 E0 E1 X0 | ok0 ok1 err ok1 ok0 | ok0 ok0 ok0 err ok0 +C B0 E0 E1 X1 | ok0 ok1 err ok1 ok1 | ok0 ok0 ok0 err ok1 +C B0 E0 X0 C | ok0 ok1 err ok0 ok2 | ok0 ok0 ok0 ok0 ok1 +C B0 E0 X0 B0 | ok0 ok1 err ok0 err | ok0 ok0 ok0 ok0 err +C B0 E0 X0 B1 | ok0 ok1 err ok0 ok2 | ok0 ok0 ok0 ok0 err +C B0 E0 X0 E0 | ok0 ok1 err ok0 err | ok0 ok0 ok0 ok0 err +C B0 E0 X0 E1 | ok0 ok1 err ok0 ok1 | ok0 ok0 ok0 ok0 err +C B0 E0 X0 X0 | ok0 ok1 err ok0 ok0 | ok0 ok0 ok0 ok0 ok0 +C B0 E0 X0 X1 | ok0 ok1 err ok0 ok1 | ok0 ok0 ok0 ok0 ok1 +C B0 E0 X1 C | ok0 ok1 err ok1 ok2 | ok0 ok0 ok0 ok1 ok1 +C B0 E0 X1 B0 | ok0 ok1 err ok1 err | ok0 ok0 ok0 ok1 ok0 +C B0 E0 X1 B1 | ok0 ok1 err ok1 err | ok0 ok0 ok0 ok1 err +C B0 E0 X1 E0 | ok0 ok1 err ok1 err | ok0 ok0 ok0 ok1 ok0 +C B0 E0 X1 E1 | ok0 ok1 err ok1 err | ok0 ok0 ok0 ok1 err +C B0 E0 X1 X0 | ok0 ok1 err ok1 ok0 | ok0 ok0 ok0 ok1 ok0 +C B0 E0 X1 X1 | ok0 ok1 err ok1 ok1 | ok0 ok0 ok0 ok1 ok1 +C B0 E1 C C | ok0 ok1 ok1 ok2 ok3 | ok0 ok0 err ok1 ok2 +C B0 E1 C B0 | ok0 ok1 ok1 ok2 err | ok0 ok0 err ok1 ok0 +C B0 E1 C B1 | ok0 ok1 ok1 ok2 ok3 | ok0 ok0 err ok1 ok1 +C B0 E1 C E0 | ok0 ok1 ok1 ok2 err | ok0 ok0 err ok1 ok0 +C B0 E1 C E1 | ok0 ok1 ok1 ok2 ok1 | ok0 ok0 err ok1 ok1 +C B0 E1 C X0 | ok0 ok1 ok1 ok2 ok0 | ok0 ok0 err ok1 ok0 +C B0 E1 C X1 | ok0 ok1 ok1 ok2 ok1 | ok0 ok0 err ok1 ok1 +C B0 E1 B0 C | ok0 ok1 ok1 err ok2 | ok0 ok0 err ok0 ok1 +C B0 E1 B0 B0 | ok0 ok1 ok1 err err | ok0 ok0 err ok0 ok0 +C B0 E1 B0 B1 | ok0 ok1 ok1 err ok2 | ok0 ok0 err ok0 err +C B0 E1 B0 E0 | ok0 ok1 ok1 err err | ok0 ok0 err ok0 ok0 +C B0 E1 B0 E1 | ok0 ok1 ok1 err ok1 | ok0 ok0 err ok0 err +C B0 E1 B0 X0 | ok0 ok1 ok1 err ok0 | ok0 ok0 err ok0 ok0 +C B0 E1 B0 X1 | ok0 ok1 ok1 err ok1 | ok0 ok0 err ok0 ok1 +C B0 E1 B1 C | ok0 ok1 ok1 ok2 ok3 | ok0 ok0 err err ok1 +C B0 E1 B1 B0 | ok0 ok1 ok1 ok2 err | ok0 ok0 err err ok0 +C B0 E1 B1 B1 | ok0 ok1 ok1 ok2 err | ok0 ok0 err err err +C B0 E1 B1 E0 | ok0 ok1 ok1 ok2 err | ok0 ok0 err err ok0 +C B0 E1 B1 E1 | ok0 ok1 ok1 ok2 err | ok0 ok0 err err err +C B0 E1 B1 X0 | ok0 ok1 ok1 ok2 ok0 | ok0 ok0 err err ok0 +C B0 E1 B1 X1 | ok0 ok1 ok1 ok2 ok1 | ok0 ok0 err err ok1 +C B0 E1 E0 C | ok0 ok1 ok1 err ok2 | ok0 ok0 err ok0 ok1 +C B0 E1 E0 B0 | ok0 ok1 ok1 err err | ok0 ok0 err ok0 ok0 +C B0 E1 E0 B1 | ok0 ok1 ok1 err ok2 | ok0 ok0 err ok0 err +C B0 E1 E0 E0 | ok0 ok1 ok1 err err | ok0 ok0 err ok0 ok0 +C B0 E1 E0 E1 | ok0 ok1 ok1 err ok1 | ok0 ok0 err ok0 err +C B0 E1 E0 X0 | ok0 ok1 ok1 err ok0 | ok0 ok0 err ok0 ok0 +C B0 E1 E0 X1 | ok0 ok1 ok1 err ok1 | ok0 ok0 err ok0 ok1 +C B0 E1 E1 C | ok0 ok1 ok1 ok1 ok2 | ok0 ok0 err err ok1 +C B0 E1 E1 B0 | ok0 ok1 ok1 ok1 err | ok0 ok0 err err ok0 +C B0 E1 E1 B1 | ok0 ok1 ok1 ok1 ok2 | ok0 ok0 err err err +C B0 E1 E1 E0 | ok0 ok1 ok1 ok1 err | ok0 ok0 err err ok0 +C B0 E1 E1 E1 | ok0 ok1 ok1 ok1 ok1 | ok0 ok0 err err err +C B0 E1 E1 X0 | ok0 ok1 ok1 ok1 ok0 | ok0 ok0 err err ok0 +C B0 E1 E1 X1 | ok0 ok1 ok1 ok1 ok1 | ok0 ok0 err err ok1 +C B0 E1 X0 C | ok0 ok1 ok1 ok0 ok2 | ok0 ok0 err ok0 ok1 +C B0 E1 X0 B0 | ok0 ok1 ok1 ok0 err | ok0 ok0 err ok0 err +C B0 E1 X0 B1 | ok0 ok1 ok1 ok0 ok2 | ok0 ok0 err ok0 err +C B0 E1 X0 E0 | ok0 ok1 ok1 ok0 err | ok0 ok0 err ok0 err +C B0 E1 X0 E1 | ok0 ok1 ok1 ok0 ok1 | ok0 ok0 err ok0 err +C B0 E1 X0 X0 | ok0 ok1 ok1 ok0 ok0 | ok0 ok0 err ok0 ok0 +C B0 E1 X0 X1 | ok0 ok1 ok1 ok0 ok1 | ok0 ok0 err ok0 ok1 +C B0 E1 X1 C | ok0 ok1 ok1 ok1 ok2 | ok0 ok0 err ok1 ok1 +C B0 E1 X1 B0 | ok0 ok1 ok1 ok1 err | ok0 ok0 err ok1 ok0 +C B0 E1 X1 B1 | ok0 ok1 ok1 ok1 err | ok0 ok0 err ok1 err +C B0 E1 X1 E0 | ok0 ok1 ok1 ok1 err | ok0 ok0 err ok1 ok0 +C B0 E1 X1 E1 | ok0 ok1 ok1 ok1 err | ok0 ok0 err ok1 err +C B0 E1 X1 X0 | ok0 ok1 ok1 ok1 ok0 | ok0 ok0 err ok1 ok0 +C B0 E1 X1 X1 | ok0 ok1 ok1 ok1 ok1 | ok0 ok0 err ok1 ok1 +C B0 X0 C C | ok0 ok1 ok0 ok2 ok3 | ok0 ok0 ok0 ok1 ok2 +C B0 X0 C B0 | ok0 ok1 ok0 ok2 err | ok0 ok0 ok0 ok1 err +C B0 X0 C B1 | ok0 ok1 ok0 ok2 ok3 | ok0 ok0 ok0 ok1 ok1 +C B0 X0 C E0 | ok0 ok1 ok0 ok2 err | ok0 ok0 ok0 ok1 err +C B0 X0 C E1 | ok0 ok1 ok0 ok2 ok1 | ok0 ok0 ok0 ok1 ok1 +C B0 X0 C X0 | ok0 ok1 ok0 ok2 ok0 | ok0 ok0 ok0 ok1 ok0 +C B0 X0 C X1 | ok0 ok1 ok0 ok2 ok1 | ok0 ok0 ok0 ok1 ok1 +C B0 X0 B0 C | ok0 ok1 ok0 err ok2 | ok0 ok0 ok0 err ok1 +C B0 X0 B0 B0 | ok0 ok1 ok0 err err | ok0 ok0 ok0 err err +C B0 X0 B0 B1 | ok0 ok1 ok0 err ok2 | ok0 ok0 ok0 err err +C B0 X0 B0 E0 | ok0 ok1 ok0 err err | ok0 ok0 ok0 err err +C B0 X0 B0 E1 | ok0 ok1 ok0 err ok1 | ok0 ok0 ok0 err err +C B0 X0 B0 X0 | ok0 ok1 ok0 err ok0 | ok0 ok0 ok0 err ok0 +C B0 X0 B0 X1 | ok0 ok1 ok0 err ok1 | ok0 ok0 ok0 err ok1 +C B0 X0 B1 C | ok0 ok1 ok0 ok2 ok3 | ok0 ok0 ok0 err ok1 +C B0 X0 B1 B0 | ok0 ok1 ok0 ok2 err | ok0 ok0 ok0 err err +C B0 X0 B1 B1 | ok0 ok1 ok0 ok2 err | ok0 ok0 ok0 err err +C B0 X0 B1 E0 | ok0 ok1 ok0 ok2 err | ok0 ok0 ok0 err err +C B0 X0 B1 E1 | ok0 ok1 ok0 ok2 err | ok0 ok0 ok0 err err +C B0 X0 B1 X0 | ok0 ok1 ok0 ok2 ok0 | ok0 ok0 ok0 err ok0 +C B0 X0 B1 X1 | ok0 ok1 ok0 ok2 ok1 | ok0 ok0 ok0 err ok1 +C B0 X0 E0 C | ok0 ok1 ok0 err ok2 | ok0 ok0 ok0 err ok1 +C B0 X0 E0 B0 | ok0 ok1 ok0 err err | ok0 ok0 ok0 err err +C B0 X0 E0 B1 | ok0 ok1 ok0 err ok2 | ok0 ok0 ok0 err err +C B0 X0 E0 E0 | ok0 ok1 ok0 err err | ok0 ok0 ok0 err err +C B0 X0 E0 E1 | ok0 ok1 ok0 err ok1 | ok0 ok0 ok0 err err +C B0 X0 E0 X0 | ok0 ok1 ok0 err ok0 | ok0 ok0 ok0 err ok0 +C B0 X0 E0 X1 | ok0 ok1 ok0 err ok1 | ok0 ok0 ok0 err ok1 +C B0 X0 E1 C | ok0 ok1 ok0 ok1 ok2 | ok0 ok0 ok0 err ok1 +C B0 X0 E1 B0 | ok0 ok1 ok0 ok1 err | ok0 ok0 ok0 err err +C B0 X0 E1 B1 | ok0 ok1 ok0 ok1 ok2 | ok0 ok0 ok0 err err +C B0 X0 E1 E0 | ok0 ok1 ok0 ok1 err | ok0 ok0 ok0 err err +C B0 X0 E1 E1 | ok0 ok1 ok0 ok1 ok1 | ok0 ok0 ok0 err err +C B0 X0 E1 X0 | ok0 ok1 ok0 ok1 ok0 | ok0 ok0 ok0 err ok0 +C B0 X0 E1 X1 | ok0 ok1 ok0 ok1 ok1 | ok0 ok0 ok0 err ok1 +C B0 X0 X0 C | ok0 ok1 ok0 ok0 ok2 | ok0 ok0 ok0 ok0 ok1 +C B0 X0 X0 B0 | ok0 ok1 ok0 ok0 err | ok0 ok0 ok0 ok0 err +C B0 X0 X0 B1 | ok0 ok1 ok0 ok0 ok2 | ok0 ok0 ok0 ok0 err +C B0 X0 X0 E0 | ok0 ok1 ok0 ok0 err | ok0 ok0 ok0 ok0 err +C B0 X0 X0 E1 | ok0 ok1 ok0 ok0 ok1 | ok0 ok0 ok0 ok0 err +C B0 X0 X0 X0 | ok0 ok1 ok0 ok0 ok0 | ok0 ok0 ok0 ok0 ok0 +C B0 X0 X0 X1 | ok0 ok1 ok0 ok0 ok1 | ok0 ok0 ok0 ok0 ok1 +C B0 X0 X1 C | ok0 ok1 ok0 ok1 ok2 | ok0 ok0 ok0 ok1 ok1 +C B0 X0 X1 B0 | ok0 ok1 ok0 ok1 err | ok0 ok0 ok0 ok1 err +C B0 X0 X1 B1 | ok0 ok1 ok0 ok1 err | ok0 ok0 ok0 ok1 err +C B0 X0 X1 E0 | ok0 ok1 ok0 ok1 err | ok0 ok0 ok0 ok1 err +C B0 X0 X1 E1 | ok0 ok1 ok0 ok1 err | ok0 ok0 ok0 ok1 err +C B0 X0 X1 X0 | ok0 ok1 ok0 ok1 ok0 | ok0 ok0 ok0 ok1 ok0 +C B0 X0 X1 X1 | ok0 ok1 ok0 ok1 ok1 | ok0 ok0 ok0 ok1 ok1 +C B0 X1 C C | ok0 ok1 ok1 ok2 ok3 | ok0 ok0 ok1 ok1 ok2 +C B0 X1 C B0 | ok0 ok1 ok1 ok2 err | ok0 ok0 ok1 ok1 ok0 +C B0 X1 C B1 | ok0 ok1 ok1 ok2 err | ok0 ok0 ok1 ok1 ok1 +C B0 X1 C E0 | ok0 ok1 ok1 ok2 err | ok0 ok0 ok1 ok1 ok0 +C B0 X1 C E1 | ok0 ok1 ok1 ok2 err | ok0 ok0 ok1 ok1 ok1 +C B0 X1 C X0 | ok0 ok1 ok1 ok2 ok0 | ok0 ok0 ok1 ok1 ok0 +C B0 X1 C X1 | ok0 ok1 ok1 ok2 ok1 | ok0 ok0 ok1 ok1 ok1 +C B0 X1 B0 C | ok0 ok1 ok1 err ok2 | ok0 ok0 ok1 ok0 ok1 +C B0 X1 B0 B0 | ok0 ok1 ok1 err err | ok0 ok0 ok1 ok0 ok0 +C B0 X1 B0 B1 | ok0 ok1 ok1 err err | ok0 ok0 ok1 ok0 err +C B0 X1 B0 E0 | ok0 ok1 ok1 err err | ok0 ok0 ok1 ok0 ok0 +C B0 X1 B0 E1 | ok0 ok1 ok1 err err | ok0 ok0 ok1 ok0 err +C B0 X1 B0 X0 | ok0 ok1 ok1 err ok0 | ok0 ok0 ok1 ok0 ok0 +C B0 X1 B0 X1 | ok0 ok1 ok1 err ok1 | ok0 ok0 ok1 ok0 ok1 +C B0 X1 B1 C | ok0 ok1 ok1 err ok2 | ok0 ok0 ok1 err ok1 +C B0 X1 B1 B0 | ok0 ok1 ok1 err err | ok0 ok0 ok1 err ok0 +C B0 X1 B1 B1 | ok0 ok1 ok1 err err | ok0 ok0 ok1 err err +C B0 X1 B1 E0 | ok0 ok1 ok1 err err | ok0 ok0 ok1 err ok0 +C B0 X1 B1 E1 | ok0 ok1 ok1 err err | ok0 ok0 ok1 err err +C B0 X1 B1 X0 | ok0 ok1 ok1 err ok0 | ok0 ok0 ok1 err ok0 +C B0 X1 B1 X1 | ok0 ok1 ok1 err ok1 | ok0 ok0 ok1 err ok1 +C B0 X1 E0 C | ok0 ok1 ok1 err ok2 | ok0 ok0 ok1 ok0 ok1 +C B0 X1 E0 B0 | ok0 ok1 ok1 err err | ok0 ok0 ok1 ok0 ok0 +C B0 X1 E0 B1 | ok0 ok1 ok1 err err | ok0 ok0 ok1 ok0 err +C B0 X1 E0 E0 | ok0 ok1 ok1 err err | ok0 ok0 ok1 ok0 ok0 +C B0 X1 E0 E1 | ok0 ok1 ok1 err err | ok0 ok0 ok1 ok0 err +C B0 X1 E0 X0 | ok0 ok1 ok1 err ok0 | ok0 ok0 ok1 ok0 ok0 +C B0 X1 E0 X1 | ok0 ok1 ok1 err ok1 | ok0 ok0 ok1 ok0 ok1 +C B0 X1 E1 C | ok0 ok1 ok1 err ok2 | ok0 ok0 ok1 err ok1 +C B0 X1 E1 B0 | ok0 ok1 ok1 err err | ok0 ok0 ok1 err ok0 +C B0 X1 E1 B1 | ok0 ok1 ok1 err err | ok0 ok0 ok1 err err +C B0 X1 E1 E0 | ok0 ok1 ok1 err err | ok0 ok0 ok1 err ok0 +C B0 X1 E1 E1 | ok0 ok1 ok1 err err | ok0 ok0 ok1 err err +C B0 X1 E1 X0 | ok0 ok1 ok1 err ok0 | ok0 ok0 ok1 err ok0 +C B0 X1 E1 X1 | ok0 ok1 ok1 err ok1 | ok0 ok0 ok1 err ok1 +C B0 X1 X0 C | ok0 ok1 ok1 ok0 ok2 | ok0 ok0 ok1 ok0 ok1 +C B0 X1 X0 B0 | ok0 ok1 ok1 ok0 err | ok0 ok0 ok1 ok0 err +C B0 X1 X0 B1 | ok0 ok1 ok1 ok0 err | ok0 ok0 ok1 ok0 err +C B0 X1 X0 E0 | ok0 ok1 ok1 ok0 err | ok0 ok0 ok1 ok0 err +C B0 X1 X0 E1 | ok0 ok1 ok1 ok0 err | ok0 ok0 ok1 ok0 err +C B0 X1 X0 X0 | ok0 ok1 ok1 ok0 ok0 | ok0 ok0 ok1 ok0 ok0 +C B0 X1 X0 X1 | ok0 ok1 ok1 ok0 ok1 | ok0 ok0 ok1 ok0 ok1 +C B0 X1 X1 C | ok0 ok1 ok1 ok1 ok2 | ok0 ok0 ok1 ok1 ok1 +C B0 X1 X1 B0 | ok0 ok1 ok1 ok1 err | ok0 ok0 ok1 ok1 ok0 +C B0 X1 X1 B1 | ok0 ok1 ok1 ok1 err | ok0 ok0 ok1 ok1 err +C B0 X1 X1 E0 | ok0 ok1 ok1 ok1 err | ok0 ok0 ok1 ok1 ok0 +C B0 X1 X1 E1 | ok0 ok1 ok1 ok1 err | ok0 ok0 ok1 ok1 err +C B0 X1 X1 X0 | ok0 ok1 ok1 ok1 ok0 | ok0 ok0 ok1 ok1 ok0 +C B0 X1 X1 X1 | ok0 ok1 ok1 ok1 ok1 | ok0 ok0 ok1 ok1 ok1 +