Name generation for machine variables should be dependent on the type, e.g. _n1, _n2, ... for natural, _xs1, _xs2, ... for lists/tensors and only fall back to _x1, _x2, ... by default...

Have to write every (x : (Tensor Int [2])) . True rather than every (x : Tensor Int [2]) . True

Currently we have a horrible hack in 361939e to replace lf line endings with crlf line endings in windows. This should be pushed up to Prettyprinter.

Change needs to be in Render.Lazy (https://hackage.haskell.org/package/prettyprinter-1.7.1/docs/src/Prettyprinter.Render.Text.html)

BNFC doesn't seem to allow us to have them as both token and layout keywords. See BNFC/bnfc#372 for details.

Turn all instances of Name in grammars to Ident and similarly symbol in Haskell code

Duplicate the VNNLib file for now, and rename it Marabou, strip out the meta-network steps and make the minor tweaks necessary for it to work.

In order to translate to SMTLib we need all quantifiers to be at the top of the expression.

So that we can have a build script that supports both Windows and Linux.

The steps required to support these are as follows:

1. Let-lift all network applications in a property to the top-level (#26)
2. If we have multiple applications of the same network to different inputs then update the onnx file to contain that number of independent copies of the network, and label the inputs/outputs X1 .... XN, X[N+1] ... X[2N], ... etc
3. If we have multiple networks, then merge the onnx files to contain both networks independently and again label the inputs X1 .... XN, X[N+1] .... XM

Currently when we compile rational literals to SMTLib we simply cast the Rational value back to a double and then print the result. Unfortunately this obviously runs into floating point precision issues, and e.g. in andGate.vnnlib we currently end up with -3.1365920000000003 rather than -3.136592.

The right way to do this is to distinguish between rational and floating point literals in the frontend (e.g. 1.31 and 1.31f) and then make a similar distinction in SMTLib (which also supports that).

This issue arises from trying to get the following to type check:

polyId : forall t. t -> t
polyId = \{t} -> \x -> x

Vehicle currently crashes with Error: DeBruijn index 0 greater than current context size 0 (Line 3, Columns 20-21) (perhaps with different line numbers). This error is thrown by the conversion from de Bruijn back to concrete named representation.

Currently the de Bruijn to concrete names conversion works in two stages:

1. de Bruijn indices in the AST are converted to Names, which either copies over the user's original name, or uses Machine for machine generated binders
2. Then a second pass converts all Names to Symbols (so they can be printed) and simultaneously converts all the annotations (which contain the types of each sub term) from de Bruijn to names (and then symbols).

The problem is that when the second pass converts annotations from de Bruijn to Names, it operates on each annotation in isolation without taking into account the binding context. The variable occurrence x at the end is annotated by the type checker with the type TVar 0, where the de Bruijn index 0 makes sense in the content of the binder {t}. However, the conversion of the annotation TVar 0 does not know about this context yielding the error above.

The solution therefore is to convert de Bruijn to Names in the main AST and the annotations in the same past.

However, this violates the current setup of the DataflowT monad transformer. Processing of type and expression arguments (sorts 'TARG 'EARG) is assumed to only result in bindings being added to the context. But arguments are annotated with their kind/type, so they need converting from de Bruijn to Names. To do this, processing needs access to the current context which is not allowed by the current definition of DataflowT.

Two solutions come to mind:

1. Do not treat arguments as a special kind, so they get handled by their surrounding AST node.
2. Tweak DataflowT to be more permissive, and use a state monad for arguments.

This seems likely to be a mistake?

We can generalize our getter type classes using the following code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Proxy (Proxy(..))

data Pos = Here | Left Pos | Right Pos

type family Elem (a :: *) (b :: *) :: Maybe Pos where
  Elem a a      = 'Just 'Here
  Elem a (l, r) = Choose (Elem a l) (Elem a r)
  Elem a b      = 'Nothing

type family Choose (l :: Maybe a) (r :: Maybe a) :: Maybe a where
  Choose ('Just x) _         = 'Just x
  Choose _         ('Just y) = 'Just y
  Choose _         _         = 'Nothing

class Get (mp :: Maybe Pos) (a :: *) (b :: *) where
  get :: Proxy p -> a -> b

instance Get (Just Here) a a where
  get _p a = a

instance Get (Just p) a b => Get (Just (Left p)) a (b, c) where
  get _p (b, c) = get Proxy b

instance Get (Just p) a c => Get (Just (Right p) a (b, c) where
  get _p (b, c) = get Proxy c

type Has a b = Get (Elem a b) a b

This should let us define classes such as HasProvenance in a way that doesn't restrict them to being strictly left or right biased, and which happens to also generalize over the type that we are getting.

Some adaptation may be required to let this search through the AST.

The trick is taken from the following paper:

• https://dl.acm.org/doi/10.1145/2633628.2633635
• https://www.youtube.com/watch?v=OqybbwYpnuw

Thrashed out with @wenkokke this morning.

• Use keywords every and some to avoid the type-level forall
• Two types of quantifiers
  1. Quantification over types: every x . intruderFarAway x => advisesClearOfConflict x desugars to primEvery (\x -> intruderFarAway x => advisesClearOfConflict x)
  • Will need to do some domain analysis when generating loss functions to avoid naively implementing rejection sampling
  2. Quantification over containers: every x in theDataset . robustAround x desugars to fold and true (map robustAround dataset)

The command line check DATABASE_FILEPATH PROPERTY_UUID mode already exists. Therefore need to:

• read in the provided database file
• lookup the property from the UUID and lookup any networks it involves.
• check the stored hash of the network model against it's current hash

Provenance of an Arg is also stored in their expression

Different backends may or may not support different operators, so it would be a good idea to extend the normalization algorithm to optionally normalize/not normalize certain built-ins (or even defined functions).

Switching back to the BNFC printing code has revealed that BNFC does not determine between layout braces and non-layout braces. Printing anything with implicit arguments results in the following mess:

(Tensor Real) ((([((5 {
                      ?2
                    }
                    ) {{ ?3 }})] {
                      ?5
                    }
                    ) {
                      ?4
                    }
                    ) {{ ?6 }});

instead of

(Tensor Real) ((([((5 {?2}) {{ ?3 }})] {?5}) {?4}) {{ ?6 }});

TODO: submit an upstream issue to BNFC

Currently it's:

EAll.       Expr13 ::= TokAll;
EAny.       Expr13 ::= TokAny;

Shouldn't it be?

EAll.       Expr13 ::= TokAll Expr Expr;
EAny.       Expr13 ::= TokAny Expr Expr;

We should document:

• the naming schemes behind short variable names should be documented;
• design decisions such as "everything that doesn't influence the semantics of an expression should be in the generic ann field";
• programming guidelines such as "don't pattern match on Binder or Ann, rather use their accessors";
• etc.

When running the andGate example we end up trying to type the type of the let binding (initially a hole) in infer mode and therefore we error out with:

Error: the type of '_' could not be resolved (Line 16, Columns 8-9)

Currently we only normalise things like 2 + 3 but not (2 + x) + 3.

@wenkokke has found some work which she reckons might be relevant.

First off, there's this:
https://gallais.github.io/pdf/icfp13.pdf

Secondly, there's the extended abstract by Conor and Fred for their language feet: adapters.pdf

The feet project is where Fred and I muck around with this stuff, and there are loads of goodies in the pipe: free abelian groups, categories, presheaves and profunctors! Once the penny drops that walking open terms can be designed totally differently from running closed terms, fabulous possibilities emerge. You can have as much type information as you could wish for. You can do algebra as well as arithmetic. You can sneakily impose a total ordering on the terms of any type.

The following vehicle code should type check:

network A : Type 0
network B : A -> Type 0

network fn : forall {x : A}. B x -> B x

However, it fails with:

Error: Could not solve the constraint: A ~ (B (i1)) (Line 4, Columns 39-40)
Fix: Check your types

Checking the debugging output, it seems that the problem is that something is going wrong with the names to de Bruijn conversion. The translation of the final line to core syntax with de Bruijn is:

(declare-network fn : (pi {x :type A} (pi (_ :type (B (i0))) (B (i0))))) 

but it ought to be:

(declare-network fn : (pi {x :type A} (pi (_ :type (B (i0))) (B (i1))))) 

(the last variable reference on the line ought to be i1, not i0 which refers to the B x argument.

As discussed, to export to json we will use the Aeson Haskell library. We don't want to export the full Vehicle AST as 1) it contain lots of redundant information (annotations etc.) and 2) many of the built operations (map/folds etc.) will have been normalised out and therefore will never be exported to json.

Therefore the first step to doing so is to define a new cut down AST for expressions containing only the information and operations we want to translate to json in a new file Vehicle.Compile.Backend.JSON and define a translation to it from our core AST found in
Vehicle.Language.AST.Core.

For starters @ndslusarz the json expression type JExpr should only be very basic. Let's include:

• App
• Var
• Literal
• BooleanOp2 builtins (see Vehicle.Language.AST.Builtin)
• Order builtins

When trying to translate anything that is not in that list, the translation function of type CheckeExpr -> JExpr should throw a developerError if it is a type-related construct (Pi, Meta, Hole) or it should have been normalised out (e.g. Ann, list operations etc.) and otherwise throw a sensible user error that says the operation is not yet supported by the json backend.

e.g. allow the user to write 2 <= x < y < 3.

• Adjust precedence of RHS of comparison operator grammar rules, change Expr8 ::= Expr9 TokLe Expr9; to Expr8 ::= Expr9 TokLe Expr8;
• Decide how we're going to fold and unfold and in a invertible way.

For instance, in the absence of further evidence, 3 should default to Nat. The defaults should always be the smallest possible subtype in the numerical lattice:

3   -> Nat
3.0 -> Rational

Currently it's only been tested with every. Reachability tests would be an excellent example query.

Currently we just stick the PrimDict stuff in there and run away never using it. Came up across this when compiling literals to Agda. For example even if we have a Nat literal, if it has type rational then we need to resolve it and convert it to a rational. At the moment I've hacked it into the Agda complilation stage, but we should really do something principled probably involving inserting conversion functions.

Need to:

• add command line "verify" mode
• create a database file if it doesn't already exist
• assign every property a unique ID and hash
• assign every network a unique ID and hash
• compile to chosen verifier
• call chosen verifier
• store result in database

We currently overload the module name Core to both mean a module that shouldn't be re-exported and a module that concerns the non-user facing BNFC grammar.

Why not elaborate front-end x => y to not x v y in the backend? If there is a reason we should document it in the core syntax file.