zeke

See `docs/grammar.md` for what this ought to look like.

Allow non list objects in the tail position of lists

1

``` >> (cons 1 1) (cons 1 1) ^---- | error: expected list, got 1 *--> repl:0:0 ``` Currently errors but should not.

Recently in lustc we modified `let` semantics and added a `set` expression. Docs [here]( https://github.com/ZekeMedley/lustc/blob/main/docs/assignment.md).

Add Support For Zeek-Style Patterns

1

Currently paraglob supports glob style patterns. Zeek uses a different pattern type in its scripting layer which use the same syntax as [flex regular expressions](http://people.cs.aau.dk/~marius/sw/flex/Flex-Regular-Expressions.html). This pattern matching is implemented...

Presently, the serialization function only serializes the vector of patterns contained inside a paraglob. For unserializing, a new paraglob is built from that serialized vector of patterns, and its aho-corasick...

Update comment once we learn how CosmWasm message ordering works

1

i think the CosmWasm documentation and code are a little self-contradictory about message ordering. this doesn't impact the functionality of this contract, but we'll need to update a comment in...

Test light client missbehavior

1

The IBC spec discusses misbehavior [here](https://github.com/cosmos/ibc/tree/main/spec/core/ics-002-client-semantics#updatestateonmisbehaviour). This test is the same as #5, but for a light client that is frozen due to misbehavior. We need to be able to...

Informal has a CosmWasm Apalache example here: https://github.com/informalsystems/atomkraft/blob/dev/examples/cosmwasm/counter/models/counter.tla We should explore what we can formally verify about this contract using Apalache. This learning will be very useful for our other...