From c49d9e34f47900a34e9b61d51588433a6b21e90b Mon Sep 17 00:00:00 2001 From: Helder Gregorio Date: Sun, 20 Sep 2026 14:12:54 +0000 Subject: [PATCH 1/2] Add Bend 2 research notes and a checked Flight SQL prepared-statement model Research on the Bend 2 language (released 2026-09-17): what it is, how it is used, and where it could fit around Arrow, Flight and Flight SQL. dev/bend2/README.md holds the notes. dev/bend2/prepared_statement/ is a Bend 2 model of the Flight SQL prepared-statement lifecycle with five laws (closed handles never execute, created handles do execute, stale handles after a bind are rejected, and a freshness invariant that holds at start and is kept by every request). `bend PROOF.bend` checks it in 0.2 s and rejects three injected bugs; the model also compiles to JS and to a native binary. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_015wBzfARVa1g7nkB1muT5Sj --- dev/bend2/README.md | 477 ++++++++++++++++++++++++ dev/bend2/prepared_statement/LAWS.bend | 80 ++++ dev/bend2/prepared_statement/PROOF.bend | 257 +++++++++++++ dev/bend2/prepared_statement/main.bend | 156 ++++++++ 4 files changed, 970 insertions(+) create mode 100644 dev/bend2/README.md create mode 100644 dev/bend2/prepared_statement/LAWS.bend create mode 100644 dev/bend2/prepared_statement/PROOF.bend create mode 100644 dev/bend2/prepared_statement/main.bend diff --git a/dev/bend2/README.md b/dev/bend2/README.md new file mode 100644 index 0000000000..3aa5ac3e9a --- /dev/null +++ b/dev/bend2/README.md @@ -0,0 +1,477 @@ + + +# 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. + +## 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 five such laws about +prepared statements, proves them, checks in 0.2 seconds, and rejects +three injected bugs. 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. + +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`) | 139 | +| Laws (`LAWS.bend`, 5 laws) | 63 | +| Proofs (`PROOF.bend`) | 240 | + +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`). `ABind` on a live handle retires +it and issues the counter as the new handle. `replay` runs a trace. + +### 4.2 The laws + +`LAWS.bend` states five laws over arbitrary server states: + +1. `closed_never_executes`: after `AClose{h}`, `AExec{h}` answers `RErr`. +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`: after `ABind{h}` rotates the handle, + `AExec{h}` on the old handle answers `RErr`. This is the spec + sentence quoted above. +4. `fresh_start` and 5. `fresh_kept`: the initial state is fresh (all + live handles are below the counter) and every request preserves + freshness. Law 3 is stated for fresh states, and laws 4 and 5 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 +stale handle) and print `Err`. + +## 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 (good fit, some work) + +Because the model compiles to JavaScript, and `bend2/main.ts` doubles +as a bun and node loader (`import Model from "./main.bend"` exposes +every non-IO def with constructors as `{$: "Name", ...}` and `Nat` as +`BigInt`), a Bend model can drive or check traces. A differential +test would generate request traces, run them through the model to get +the expected responses, and replay them against `FlightSqlClient` and +a producer such as `FlightSqlStatelessExample`, comparing the +`Ok`/error outcome per step. `TestFlightSqlStateless` is the natural +home. This needs a small bridge (a JSON trace format, a node step in +the test, or committing generated expectations), and the oracle is +only as good as the model, but it turns the prose rules into a +regression test. + +### 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. Build the differential harness in 5.2 against + `FlightSqlStatelessExample` and `FlightSqlExample`, starting with + the prepared-statement traces the model already generates. +4. 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..42ba69084d --- /dev/null +++ b/dev/bend2/prepared_statement/LAWS.bend @@ -0,0 +1,80 @@ +# 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. +law closed_never_executes: + for +h : Nat + for +live : List<&2, Nat> + for +next : Nat + {PS.resp(PS.step_s(PS.AExec{h}, PS.state(PS.step(PS.AClose{h}, live, next)))) == 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 + {PS.resp(PS.step_s(PS.AExec{next}, PS.state(PS.step(PS.ACreate{}, live, next)))) == 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." +# 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)))) == PS.RErr{} : PS.Resp} + +# LAW: the initial state is fresh +law fresh_start: + Fresh_s(PS.start()) + +# LAW: every request keeps the state fresh +law fresh_kept: + for a : PS.Act + for +live : List<&2, Nat> + for +next : Nat + for w : Fresh(live, next) + Fresh_s(PS.state(PS.step(a, live, next))) diff --git a/dev/bend2/prepared_statement/PROOF.bend b/dev/bend2/prepared_statement/PROOF.bend new file mode 100644 index 0000000000..a37281ee63 --- /dev/null +++ b/dev/bend2/prepared_statement/PROOF.bend @@ -0,0 +1,257 @@ +# 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): + %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): + %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{} + +# 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, over the verdict c of has(h, live) +def kept_bind.fin(c: Bool, +h: Nat, +live: List<&2, Nat>, +next: Nat, w: Laws.Fresh(live, next)) + -> Laws.Fresh_s(PS.state(PS.bind(h, live, next, c))): + match c: + 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 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, 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), 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, c)))) == 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) diff --git a/dev/bend2/prepared_statement/main.bend b/dev/bend2/prepared_statement/main.bend new file mode 100644 index 0000000000..b74c2759ee --- /dev/null +++ b/dev/bend2/prepared_statement/main.bend @@ -0,0 +1,156 @@ +# 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. This is the "stateless" server style +# from the Flight SQL spec: binding parameters (DoPut) may rotate the +# handle, and the client must use the rotated one afterwards. +# +# 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, retire it and issue a fresh one; else Err +def bind(+h: Nat, +live: List<&2, Nat>, +next: Nat, ok: Bool) -> Server & Resp: + match ok: + case True{}: + (Server{next <> remove(h, live), 1n+next}, ROk{next}) + case False{}: + (Server{live, next}, RErr{}) + +# one request against one state +def step(a: Act, +live: List<&2, Nat>, +next: Nat) -> Server & Resp: + match a: + case ACreate{}: + (Server{next <> live, 1n+next}, ROk{next}) + case ABind{+h}: + bind(h, live, next, 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) -> Server & Resp: + Server{live, next} = s + step(a, live, next) + +def start() -> Server: + Server{Nil{}, 0n} + +# a whole trace, threading the state and the last response +def run(acts: List, sr: Server & Resp) -> Server & Resp: + match acts: + case Nil{}: + sr + case a <> rest: + (s, last) = sr + run(rest, step_s(a, s)) + +def replay(acts: List) -> Server & Resp: + run(acts, (start(), RErr{})) + +# Show +# ---- + +def Resp.show(r: Resp) -> String: + match r: + case ROk{h}: + "Ok(" ++ Nat.show(h) ++ ")" + case RErr{}: + "Err" + +# create, bind (handle 0 -> 1), execute the stale 0: Err +def main() -> IO(Unit): + IO.print(Resp.show(resp(replay([ACreate{}, ABind{0n}, AExec{0n}])))) From 668746c4142f19e21c0848940e42c0243483a2af Mon Sep 17 00:00:00 2001 From: Helder Gregorio Date: Sun, 20 Sep 2026 15:22:03 +0000 Subject: [PATCH 2/2] Validate Flight SQL example servers against the proven Bend 2 model Turn the prepared-statement model into a test oracle for the Java servers. The model gains the bind policy the spec allows ("may return an updated handle"): rotate or keep, with a sixth law that a kept handle still executes. traces.bend enumerates 1085 request sequences, runs them through the proven model under both policies and prints the expected response to each request; the output is committed as a test resource so the Java build needs no Bend toolchain. TestFlightSqlBendConformance replays every trace against FlightSqlExample (keep column) and FlightSqlStatelessExample (rotate column) through the raw Flight client and compares success or error per request. The stateful example matches on all 4221 steps. The stateless example deviates in three documented categories, kept as a known-deviation set so the test fails on a fix or a regression: executing or binding stale and closed handles succeeds, and binding a rotated handle again fails. dev/bend2/DIFFERENTIAL_TESTING.md explains the chain of trust, the pieces, the results and the limits; the research notes are updated. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_015wBzfARVa1g7nkB1muT5Sj --- dev/bend2/DIFFERENTIAL_TESTING.md | 245 ++++ dev/bend2/README.md | 113 +- dev/bend2/prepared_statement/LAWS.bend | 32 +- dev/bend2/prepared_statement/PROOF.bend | 59 +- dev/bend2/prepared_statement/main.bend | 59 +- dev/bend2/prepared_statement/traces.bend | 212 ++++ .../test/TestFlightSqlBendConformance.java | 404 ++++++ .../bend2/prepared_statement_traces.txt | 1109 +++++++++++++++++ 8 files changed, 2160 insertions(+), 73 deletions(-) create mode 100644 dev/bend2/DIFFERENTIAL_TESTING.md create mode 100644 dev/bend2/prepared_statement/traces.bend create mode 100644 flight/flight-sql/src/test/java/org/apache/arrow/flight/sql/test/TestFlightSqlBendConformance.java create mode 100644 flight/flight-sql/src/test/resources/bend2/prepared_statement_traces.txt 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 index 3aa5ac3e9a..6c0b420c45 100644 --- a/dev/bend2/README.md +++ b/dev/bend2/README.md @@ -27,7 +27,10 @@ Written against Bend 2.0.21, commit `c15a75f8` of 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. +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 @@ -43,12 +46,16 @@ 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 five such laws about +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. 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. +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 @@ -226,9 +233,10 @@ Writing the prototype gave a feel for the effort: | Item | Lines | | --- | ---: | -| Model (`main.bend`) | 139 | -| Laws (`LAWS.bend`, 5 laws) | 63 | -| Proofs (`PROOF.bend`) | 240 | +| 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 @@ -266,24 +274,31 @@ 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`). `ABind` on a live handle retires -it and issues the counter as the new handle. `replay` runs a trace. +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 five laws over arbitrary server states: +`LAWS.bend` states six laws over arbitrary server states: -1. `closed_never_executes`: after `AClose{h}`, `AExec{h}` answers `RErr`. +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`: after `ABind{h}` rotates the handle, - `AExec{h}` on the old handle answers `RErr`. This is the spec - sentence quoted above. -4. `fresh_start` and 5. `fresh_kept`: the initial state is fresh (all +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. Law 3 is stated for fresh states, and laws 4 and 5 show - every reachable state is fresh, so together they cover every trace. + 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 @@ -305,7 +320,28 @@ 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 -stale handle) and print `Err`. +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 @@ -336,20 +372,18 @@ 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 (good fit, some work) - -Because the model compiles to JavaScript, and `bend2/main.ts` doubles -as a bun and node loader (`import Model from "./main.bend"` exposes -every non-IO def with constructors as `{$: "Name", ...}` and `Nat` as -`BigInt`), a Bend model can drive or check traces. A differential -test would generate request traces, run them through the model to get -the expected responses, and replay them against `FlightSqlClient` and -a producer such as `FlightSqlStatelessExample`, comparing the -`Ok`/error outcome per step. `TestFlightSqlStateless` is the natural -home. This needs a small bridge (a JSON trace format, a node step in -the test, or committing generated expectations), and the oracle is -only as good as the model, but it turns the prose rules into a -regression test. +### 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) @@ -432,10 +466,13 @@ code should do, and section 5.2 turns that into tests. action per state as laws. 2. Model `PollFlightInfo` (descriptor reuse, monotone progress, expiration, cancel) the same way. -3. Build the differential harness in 5.2 against - `FlightSqlStatelessExample` and `FlightSqlExample`, starting with - the prepared-statement traces the model already generates. -4. Revisit runtime integration only if a Python or JVM target or a +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 diff --git a/dev/bend2/prepared_statement/LAWS.bend b/dev/bend2/prepared_statement/LAWS.bend index 42ba69084d..0dca14da6a 100644 --- a/dev/bend2/prepared_statement/LAWS.bend +++ b/dev/bend2/prepared_statement/LAWS.bend @@ -41,40 +41,54 @@ def Fresh_s(s: PS.Server) -> Data: # LAW: "Closes server resources associated with the prepared statement # handle." Once a handle is closed, executing it is an error, from any -# server state. +# server state and under either bind policy. law closed_never_executes: for +h : Nat for +live : List<&2, Nat> for +next : Nat - {PS.resp(PS.step_s(PS.AExec{h}, PS.state(PS.step(PS.AClose{h}, live, next)))) == PS.RErr{} : PS.Resp} + 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 - {PS.resp(PS.step_s(PS.AExec{next}, PS.state(PS.step(PS.ACreate{}, live, next)))) == PS.ROk{next} : PS.Resp} + 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." -# 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. +# 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)))) == PS.RErr{} : PS.Resp} + {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 +# 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))) + 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 index a37281ee63..d7147476e9 100644 --- a/dev/bend2/prepared_statement/PROOF.bend +++ b/dev/bend2/prepared_statement/PROOF.bend @@ -57,11 +57,11 @@ def eq_refl(n: Nat) -> {True{} == Nat.is_eq(n, n) : Bool}: # Laws # ---- -def Laws.closed_never_executes(h, live, next): +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): +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} {==} @@ -85,6 +85,22 @@ 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: @@ -207,16 +223,25 @@ def has_lt(+h: Nat, xs: List<&2, Nat>, +n: Nat) -> Laws.T(PS.has(h, xs)) -> Laws def Laws.fresh_start(): Unit{} -# the Bind arm, over the verdict c of has(h, live) -def kept_bind.fin(c: Bool, +h: Nat, +live: List<&2, Nat>, +next: Nat, w: Laws.Fresh(live, next)) - -> Laws.Fresh_s(PS.state(PS.bind(h, live, next, c))): - match c: +# 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))): @@ -226,12 +251,12 @@ def kept_exec.fin(c: Bool, +h: Nat, +live: List<&2, Nat>, +next: Nat, w: Laws.Fr case False{}: w -def Laws.fresh_kept(a, live, next, 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), h, live, next, w) + 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}: @@ -242,7 +267,7 @@ def Laws.fresh_kept(a, live, next, w): # 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, c)))) == PS.RErr{} : PS.Resp}: + -> {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)) @@ -255,3 +280,19 @@ def stale.fin(+h: Nat, +live: List<&2, Nat>, +next: Nat, c: Bool, e: {c == PS.ha 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 index b74c2759ee..3f94ad2978 100644 --- a/dev/bend2/prepared_statement/main.bend +++ b/dev/bend2/prepared_statement/main.bend @@ -18,9 +18,10 @@ # 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. This is the "stateless" server style -# from the Flight SQL spec: binding parameters (DoPut) may rotate the -# handle, and the client must use the rotated one afterwards. +# 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 @@ -92,21 +93,29 @@ def exec(+h: Nat, live: List<&2, Nat>, +next: Nat, ok: Bool) -> Server & Resp: case False{}: (Server{live, next}, RErr{}) -# Bind: on a live handle, retire it and issue a fresh one; else Err -def bind(+h: Nat, +live: List<&2, Nat>, +next: Nat, ok: Bool) -> Server & Resp: - match ok: +# 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 -def step(a: Act, +live: List<&2, Nat>, +next: Nat) -> Server & Resp: +# 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, has(h, live)) + bind(h, live, next, rot, has(h, live)) case AExec{+h}: exec(h, live, next, has(h, live)) case AClose{+h}: @@ -122,24 +131,37 @@ def resp(sr: Server & Resp) -> Resp: r # a request against a whole server -def step_s(a: Act, s: Server) -> Server & Resp: +def step_s(a: Act, s: Server, rot: Bool) -> Server & Resp: Server{live, next} = s - step(a, live, next) + 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) -> Server & Resp: +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)) + run(rest, step_s(a, s, rot), rot) -def replay(acts: List) -> Server & Resp: - run(acts, (start(), RErr{})) +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 # ---- @@ -151,6 +173,9 @@ def Resp.show(r: Resp) -> String: case RErr{}: "Err" -# create, bind (handle 0 -> 1), execute the stale 0: 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): - IO.print(Resp.show(resp(replay([ACreate{}, ABind{0n}, AExec{0n}])))) + 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 +