Expand Laurel implementation, so that tests T2 (impure expressions) and T3 (dag control flow) pass as well #2
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…#187) *Issue #, if available:* *Description of changes:* This PR contains some several improvements to Lambda's typing rules and type inference: 1. Refactors constants to use a typed representation rather than representing all as strings. This has significant benefits when typechecking (`inferConst` in `LExprT.lean`) and in the typing rules (`HasType` in `LExprTypeSpec.lean`). It also rules out cases like `.const "3" .bool` automatically. 2. This changes the representation of real constants from strings to `Rat`, and this PR includes functions to convert between `Decimal` and `Rat` in `DecimalRat.lean`. 3. Adds quantifier case to typing rules (`HasType` in `LExprTypeSpec.lean`) 4. Updates and simplifies proofs in `LExprWF.lean` By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com>
Implements initial version of Python AST -> Boogie translation. The main pain point is handling kw args. We choose a canonical ordering for function args and use that for the Boogie representation. The code for this is in `Strata/Languages/Python/FunctionSignatures.lean` Ideally, we can mechanically extract this from the Boogie prelude. Instructions for running the code are here: StrataTest/Languages/Python/README.md The code in `StrataTest/Internal` is empty stubs for internal code. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
The previous semantics are big-step, which is less standard and makes loops awkward. To continue to make use of the existing transformation correctness proofs, we could prove equivalence between the big-step and small-step semantics (which shouldn't be too hard, but would be some work). By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Add CI for Python Analysis By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
*Issue #, if available:* *Description of changes:* This PR adds a mechanism for defining inductive types in Strata using a `TypeFactory`, modeled after a `Factory` for functions. This includes synthesis of constructor and eliminator `LFunc` instances, supporting recursion over strictly positive, uniform types (these conditions are checked when the `TypeFactory` is created). The implementation of inductive types can be found at `Strata/DL/Lambda/TypeFactory.lean`, and several test cases and examples can be found at `StrataTest/DL/Lambda/TypeFactoryTests.lean`. Note also that the Lambda partial evaluator has been modified to allow for the evaluation of the generated eliminators. Right now the eliminator-based mechanism for writing functions over inductive types is difficult to read; we would likely need some kind of syntactic sugar to make this more usable (much like one typically writes pattern matches in Lean rather than using recursors directly). By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com>
… of Boogie Factory ops (strata-org#201) This patch adds a random testing of Boogie operations registered in factory, by (1) choosing random constant inputs to the operations (2) doing concrete evaluation and getting the results, (3) SMT encoding the expression, and (4) checking using the SMT solver whether the concrete output is equal to the SMT expression. :) The random input generator for string/regex is rather simplistic, but most of the advanced string operations don't have concrete evaluators implemented in Factory. The random const generator for triggers are omitted but I will be happy to get inputs. Also, Boogie's `Env.init` is updated to have `Boogie.Factory` by default (discussed with Shilpi). By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
*Description of changes:* Preliminary parser of and translator from basic regex patterns into Strata.Boogie's built-in regex operations. Also add new Strata.Boogie factory functions: `str.substr` -- substring of a string, and `re.none` -- denoting the empty set of strings. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
…rg#209) This adds a DDM Init category Init.ByteArray for byte literals along with textual and Ion encodings. It uses this to fix an issue in the Python dialect where byte array constants were encoded as ellipsis. This also fixes CI to run again. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Shilpi Goel <shigoel@gmail.com>
…n LMonoTy, fix broken Reflect (strata-org#211) This patch expand Lambda's basic functions to support arbitrary types rather than LMonoTy, to use them for formal evaluation semantics of Lambda which should be agnostic of the type system. This also fixes broken Reflect. Also: - Generalize Factory's two top-level fns to receive non LMonoTy as well - Remove getConcreteLFuncCall because it must use isCanonicalValue, not isConst, but isCanonicalValue cannot be used due to cyclic dependency between modules .. and it isn't used anywhere. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
*Issue #, if available:* *Description of changes:* By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Removes `partial def`, instead proving termination for `isCanonicalValue`, as discussed in comments for strata-org#167 By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com>
Extract variable names (and types) from AST. Additionally, add Str.Concat BinOp and ConBytes support. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Add expected output files for a few more BoogieToStrata tests. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. Co-authored-by: Shilpi Goel <shigoel@gmail.com>
Makes `HasType` consistent with behavior of the typechecker by adding `LContext` and rules for operators. In particular, this PR adds the condition that constants are well-typed only if their corresoponding type is known and adds rules for annotated and un-annotated operators based on their `Factory` instance. It also adds a rule for annotated free variables. Annotated operators and free variables are somewhat complex, as they require the annotation to be an instantiation of their general type. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com>
* Added a new generic metadata field to every construct of `Lambda.LExpr` * Replaced `LExprT` by `LExpr` whose metadata field is a pair of a metadata and the type. * Replaced all type arguments of `LExpr` by a unique type structure named `T: LExprParamsT` everywhere * `LExprParamsT` is a structured pair of an `LExprParams` and a type, so that `T.mono` uses `LMonoTy` as the type when `T: LExprParams` * Renamed all environments using `Env` or `E` instead of `T`. * Replaced `LExprT.fromLExpr` with `LExpr.resolve` * Replaced `LExprT.toLExpr` with `LExpr.unresolved`. I'm using the passive form because the unresolved version is really easy to obtain from a resolved version. * Update `Boogie` and `CSimp` so that they can use `Unit` for this metadata. * Ensured that formatting instances are chosen by priority to `LExprT.format` and default otherwise to LExpr.format` * `Traceable` make it possible to combine metadata in a generic way, added an example in `LExprEval` when doing beta reduction on terms. ### Benefits * Extensibility: * By combining all type parameters in ones, it makes it easier to add more type parameters * Since the metadata is generic, we can use it to store structured data whenever needed. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com>
Test CBMC in CI By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Handle function declarations. This involves: 1) Hoist function declarations before the `__main__` procedure. 2) Parse and use function signatures. 3) Refactor translation so almost everything flows through the Python function -> Boogie Procedure translation. Additionally, added `pyTranslate` command to help converting Python to a Boogie prelude. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
This pull request adds a small-steps semantics of Lambda! :) `LExprEvalTests.lean` shows how the small-step semantics evaluates to the same result, for examples that were already working for concrete evaluator. There is an interesting update in the definition if `isCanonicalValue`. If `e:LExpr` is a series of `.app`, say `e0 e1 .. en`, `e` is a canonical value if (1) (_already existed before this PR, added by @joscoh_) `e0` is a constructor and `e1 .. en` are all canonical values, or (2) (_newly added_) `e0` is a named function `f` (not abstraction) and `n` is less than the number of arguments required to run the function `f`. The intuition of case (2) is as follows. Let's assume that we would like to calculate `Int.Add 1 (2+3)`. According to the small step semantics, we would like to calculate `2+3` to `5`, hence it becomes `Int.Add 1 5` and eventually 6. Without (2), this is impossible because the `reduce_2` rule of small step semantics only fires when `Int.Add 1` is a 'canonical value'. Therefore, without (2), the semantics stuck and `2+3` can never be evaluated to `5`. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Propagate sufficient metadata throughout the verification pipeline for `StrataVerify` to report the source location associated with each proof obligation. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Resolves TODO in strata-org#189 by removing duplication in beq proofs Closes strata-org#234 By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. Co-authored-by: Josh Cohen <cohenjo@amazon.com>
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
These help Kiro understand the codebase so it can more effectively perform tasks on it, with specific instructions for testing and writing proofs. Thanks to @rnagasam for writing these! By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
… to BoogieTransform.lean (strata-org#232) *Issue #, if available:* *Description of changes:* This pull request - Implements procedure inlining. It is unverified, but has a few unit tests; it implements alpha equivalence to check whether the output is equivalent to the 'answer' - Factors out the common code that is used between call elimination and procedure inlining into 'BoogieTransform.lean'. I think this file can be a nice place for monad, helper functions, etc, for implementing even more transformations :) By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
# Add stdin support to Strata executables
Adds support for reading from stdin using `-` as the filename argument
(standard Unix convention).
## Usage
```bash
# Pipe from file
cat Examples/SimpleProc.boogie.st | lake exe StrataVerify -
# Use heredoc
lake exe StrataVerify - <<'EOF'
program Boogie;
procedure Test() returns () { assert true; };
EOF
# With options
cat program.boogie.st | lake exe StrataVerify --parse-only -
```
## Changes
- Added `Strata/Strata/Util/IO.lean` with stdin reading utilities
- Updated `StrataMain.lean`, `StrataVerify.lean`, `StrataToCBMC.lean` to
support `-`
- Added unit tests in `StrataTest/Util/IO.lean`
- Error messages display `<stdin>` when reading from stdin
## Testing
All existing tests pass. Tested with piping, heredocs, and both Boogie
and C_Simp dialects.
---------
Co-authored-by: Vidas Jocius <vjjocius@users.noreply.github.com>
…-org#221) This modifies the Lean expression generation for dialects to reduce time required to declaring dialects by roughly half. also generates auxilary definitions to reduce the size of the Lean expression for a Strata program. This has a slight performance improvement, but more importantly reduces the stack requirements when parsing large Strata programs. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
*Description of changes:* This pull request updates the expression evaluator (`SemanticEval` in Strata) which previously needed to take two states: one for old expressions, one for normal (‘new’) expressions, but after this pull request it takes only one state. It introduces a couple of `sorry`s, but these will be eventually fixed. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
*Description of changes:* * Reorganize the Python-specific Boogie prelude. * Add PyFactory, a Python-specific Lambda factory that -- for now -- contains a candidate model for Python's `re.compile`. * Turn on elimination of irrelevant axioms for Python analyses. * Suppress any counterexample parsing errors from a SAT solver. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Juneyoung Lee <lebjuney@amazon.com> Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com> Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
Add pyAnalyze tests. Inline procedure calls. Move test_helper procedure spec to asserts within body. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Right now, `TypeFactory` is separate from `LContext` (e.g. in `Lambda.typeCheckAndPartialEval`). This PR bundles them together, simplifying `typeCheckAndPartialEval`, unifying the typechecking for datatypes, and making it possible to add datatypes to Boogie. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com>
…trata-org#259) pyTranslate and pyAnalyze search for the Python dialect using a search path despite being known at compile time. This changes Strata main to use the builtin version.
*Issue #, if available:* strata-org#295 *Description of changes:* Resolve type aliases and monomorphize polytypes in function arguments and body during type checking. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
## Add B3 Language Support as Strata Backend Dialect This PR adds complete support for the [B3 verification language](https://b3-lang.org/) as a new Strata backend dialect. **The implementation successfully parses the entire B3 motivating example as-is.** ### DDM Definition **Three components:** 1. **Concrete Syntax Tree (ParseCST.lean)** - Defines B3's concrete syntax using DDM - Matches B3 language syntax including dots in identifiers (e.g., `Map.select`) - Pipe-delimited identifiers for special cases (e.g., `|@0|`) 2. **Abstract Syntax Tree (DefinitionAST.lean)** - Defines B3's abstract syntax for Strata Core - De Bruijn indices for variable binding - Metadata unwrapping with `@[unwrap]` to simplify terminal nodes - Customizable metadata mapping 3. **Bidirectional Conversion (Conversion.lean)** - AST ↔ CST conversion - Error tracking for unresolved identifiers, out-of-bounds references, and unsupported variable patterns ### Technical Highlights - **Inout parameters**: Modeled as two values in the context (old and current), enabling `old x` syntax in procedure bodies and postconditions to reference pre-state values - **Shadowed variables**: Proper handling with disambiguation and detection of unsupported middle occurrences ### Testing Tests split across four categories: expressions, statements, declarations, and programs. Round-trip tests display a formatted and minimal version of the AST in the conversion for better understanding. ### Future Work - Verify B3 text files by invoking the B3 tool from Strata - Convert Strata Core to B3 AST for backend verification --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com>
*Description of changes:* Fix the proofs in CallElimCorrect.lean for the commit: strata-org@7d87684 By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Aaron Tomb <aarotomb@amazon.com> Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com>
This PR encodes datatypes using the SMT `declare-datatype` mechanism. In particular it: - Adds generation of testers (e.g. `isNil` and `isCons`) and destructors/projections (e.g. `head` and `tail`) to `TypeFactory` in `TypeFactory.lean`. - Adds a new attribute `inline_if_val` to the Lambda partial evaluator which inlines a function body if all of the arguments are values. - Adds a datatype declaration to the Boogie AST and adds the appropriate typechecks (in `ProgramType.lean`) - Adds primitives to represent datatype operations in the SMT dialect (`Op.lean` and `Encoder.lean`) - Modifies Boogie to SMT translation to (1) add datatype declarations (2) map constructors, testers, and projections to the SMT counterparts (`SMTEncoder.lean`). This involves adding datatypes and tester/destructor function maps to the `Env` (`Env.lean`). Additionally, this requires some dependency analysis to ensure that datatypes are outputted in the correct order. - Small changes to the end-to-end verification pipeline (`Boogie.lean` and `Verifier.lean`). There are several sets of test cases: - `TypeFactoryTests.lean` contains tests about testers and destructors in the Lambda partial evaluator - `SMTEncoderDatatypeTests.lean` contains tests for SMT output of datatypes and derived functions - `DatatypeVerificationTests.lean` contains tests for end-to-end verification of Boogie programs using datatypes. This does NOT (yet) include concrete Boogie syntax to generate datatypes; it only changes the Boogie AST. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com> Co-authored-by: Shilpi Goel <shigoel@gmail.com>
*Issue #, if available:* *Description of changes:* By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Josh Cohen <cohenjo@amazon.com>
…tions (strata-org#305) *Issue #, if available:* strata-org#304 *Description of changes:* Function typechecking no longer monomorphizes functions Includes test demonstrating correct behavior By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. Co-authored-by: Josh Cohen <cohenjo@amazon.com>
…rata-org#309) *Issue #, if available:* strata-org#102 *Description of changes:* This change percolates source location metadata from the DDM definition all the way down to Boogie/Imperative/Lambda. In particular, now we get source location and debugging information when Lambda's type check fails. See `Examples/TypeError.boogie.st` and `Examples/expected/TypeError.boogie.expected`. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
…#298) This applies performance optimizations to Ion serialization and deserialization to improve performance. The deserialization performance is roughly 10x before while the serialization performance doubles. The new performance numbers with a microbenchmark are: ``` ┌──────┬────────┬─────────┬─────────────┬─────────────┬────────────┬────────────┐ │ Size │ Target │ Encoded │ Serialize │ Deserialize │ Ser MB/s │ Deser MB/s │ ├──────┼────────┼─────────┼─────────────┼─────────────┼────────────┼────────────┤ │ 1MB │ 1.0MB │ 929KB │ 5.2ms │ 8.9ms │ 180 MB/s │ 105 MB/s │ │ 5MB │ 5.0MB │ 4.7MB │ 23.8ms │ 40.8ms │ 207 MB/s │ 121 MB/s │ │ 10MB │ 10.0MB │ 9.5MB │ 48.7ms │ 80.8ms │ 205 MB/s │ 123 MB/s │ │ 25MB │ 25.0MB │ 24.5MB │ 125.6ms │ 196.1ms │ 204 MB/s │ 131 MB/s │ │ 50MB │ 50.0MB │ 49.9MB │ 234.6ms │ 397.7ms │ 223 MB/s │ 131 MB/s │ └──────┴────────┴─────────┴─────────────┴─────────────┴────────────┴────────────┘ ``` Prior to this change the performance measurements using the same microbenchmark are: ``` ┌──────┬────────┬─────────┬─────────────┬─────────────┬────────────┬────────────┐ │ Size │ Target │ Encoded │ Serialize │ Deserialize │ Ser MB/s │ Deser MB/s │ ├──────┼────────┼─────────┼─────────────┼─────────────┼────────────┼────────────┤ │ 1MB │ 1.0MB │ 929KB │ 10.3ms │ 86.0ms │ 92 MB/s │ 11 MB/s │ │ 5MB │ 5.0MB │ 4.7MB │ 55.5ms │ 398.8ms │ 89 MB/s │ 12 MB/s │ │ 10MB │ 10.0MB │ 9.5MB │ 100.0ms │ 752.9ms │ 100 MB/s │ 13 MB/s │ │ 25MB │ 25.0MB │ 24.5MB │ 248.4ms │ 1.8s │ 103 MB/s │ 13 MB/s │ │ 50MB │ 50.0MB │ 49.9MB │ 516.8ms │ 3.9s │ 101 MB/s │ 13 MB/s │ └──────┴────────┴─────────┴─────────────┴─────────────┴────────────┴────────────┘ ``` By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
B3 quantifiers now support multiple comma-separated variable declarations and use the built-in Seq Pattern combinator for cleaner syntax: Simplifications: - Replaced custom Patterns list structure with Seq Pattern - Removed separate _no_patterns quantifier variants - Eliminated 75 lines of code Roundtrip tests verify the behavior.
This patch adds 1. A translator from SMT.Term -> SMTDDM.Term as well as 2. A string converter from SMTDDM.Term -> String 3. Hooks the converter to SMT/DL/Encoder.lean, only when it is encoding a primitive term (as a small-step start!) 4. Adds the `get-option` SMT command and relevant syntax categories (mentioned in the previous pull request). 5. Slightly changes the `.real` constructor of the old SMT Term, from `String` to `Decimal`. After 3, I checked the generated .smt2 files at `vcs/` dir, and confirmed that they are equivalent modulo spaces! :) There are a few features in the string converters that are unimplemented; they will be added later when Encoder.lean uses the DDM string converter more. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Shilpi Goel <shigoel@gmail.com>
…a into laurelMoreStmtExpr
This bumps documentation to 4.26.0 By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
**Java Code Generator for DDM Dialects** Generates Java source files from DDM dialect definitions for Java tooling to build ASTs that Lean can consume. **Generated:** - Sealed interfaces for categories - Record classes for operators - Static factory methods (`num(1)` vs `new Num(SourceRange.NONE, ...)`) - Ion serializer for Lean interop **Usage:** ```bash lake exe strata javaGen dialect.st com.example.pkg output/ ``` **Tests:** 12 tests including javac compilation and Java→Ion→Lean roundtrip.
*Issue #, if available:* *Description of changes:* By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Changes
ToFormatinstance for the Laurel type to help with debuggingConcreteToAbstractTreeTranslatorandLaurelToBoogieTranslator, which perform 1-1 translations.LiftExpressionAssignments, which attempts to lift any assignments that occur in an expression position so they are done in the innermost enclosing statement block instead.Caveats
I think there are a lot of cases of impure expressions that aren't supported yet. It would be good to add explicit tests for those and to return not supported diagnostics in those cases. Created a GH issue to address something that's not supported: strata-org#282
Testing