au-ts / cogent

Cogent Project

Cogent: Code and Proof Co-Generation

Project homepage

For general context of this project, motivation, an overview, and published papers, see our project homepage.

Online documentation

https://cogent.readthedocs.io

Installation

Instructions tested on Debian GNU/Linux 9.8 ("stretch") and Ubuntu 18.04 ("bionic"). Similar distributions may also work.

Install dependencies from the Debian repository.

sudo apt-get install git # git
sudo apt-get install python-lxml python-psutil python-pycparser # regression tester

To install the Cogent compiler, consult file cogent/README.md for details.

The Cogent framework depends on Isabelle-2019. If you already have them on your machine, you can use your local copy. Otherwise you can either obtain it from their website or from the isabelle submodule, via git submodule update --init --recursive -- isabelle.

Add isabelle/bin to your PATH: export PATH="$(pwd)/isabelle/bin:$PATH" If you have an existing Isabelle install, you may want to set ISABELLE_IDENTIFIER instead of PATH.

Initialise Isabelle and install components:

isabelle components -I
isabelle components -a

Consult Isabelle manual for more information.

For more customised settings to run proofs and regression tests, modify build-env.sh.

Note: also see Proofs and Regression tests below.

Compiler

See cogent/README.md for more information.

File systems

See impl/fs/ext2/README and impl/fs/bilby/README for more information on how to build the kernel modules.

Proofs

Firstly, download the AutoCorres release v1.6.1 from https://trustworthy.systems/projects/TS/autocorres, move the extracted folder to this directory, and rename the folder to autocorres.

To build the proofs, it is recommended that your machine (or virtual machine) provides 32G of memory and 4–8 CPU threads.

# Build compilation correctness proof for ext2. (ETA: 120 CPU hours)
(cd impl/fs/ext2/cogent;
 make verification;
 export L4V_ARCH="ARM";
 isabelle build -d plat/verification -d ../../../../cogent/isa -d ../../../../autocorres -b Ext2_AllRefine)

# Build compilation correctness proof for BilbyFs. (ETA: 120 CPU hours)
(cd impl/fs/bilby/cogent;
 make verification;
 patch -d plat/verification < ../../../../BilbyFs_CorresProof.patch;
 export L4V_ARCH="ARM";
 isabelle build -d plat/verification -d ../../../../cogent/isa -d ../../../../autocorres -b -o process_output_limit=999 BilbyFs_AllRefine)

# View end-to-end theorems. Each theory has a "print_theorems" command for this.
# For ext2:
L4V_ARCH="ARM" isabelle jedit -d impl/ext2/cogent/plat/verification -d cogent/isa -d autocorres -l Ext2_CorresProof impl/fs/ext2/cogent/plat/verification/Ext2_AllRefine.thy
# For BilbyFs:
L4V_ARCH="ARM" isabelle jedit -d impl/fs/bilby/cogent/plat/verification -d cogent/isa -d autocorres -l BilbyFs_CorresProof impl/fs/bilby/cogent/plat/verification/BilbyFs_AllRefine.thy

The functional correctness proofs for BilbyFs's sync and iget operations are in impl/fs/bilby/proof/. They are built as part of the regression tests, and can be rebuilt with

regression/run_tests.py -x autocorres -x isabelle -v sync iget

Regression tests (for developers; ETA: 2–3 CPU hours)

For testing the compiler, refer to travis.yml for commands.

Run ./run_tests to test systems implementations and parts of their Isabelle proofs.

For C-refinement proofs, which are excluded from the regression tests because of their size, follow instructions in Proofs section.

Directory

• cogent: Cogent compiler
• c-refinement: Isabelle/HOL theories and proof procedures for Cogent-C refinement
  • tests: Cogent test programs for proof procedures
• isa-parser: Haskell library for parsing and pretty-printing Isabelle/HOL
• impl: Systems implemented in Cogent
  • fs: File systems
    • bilby: Bilby file system
      • cogent: Cogent code for BilbyFs
      • c: C implementation for BilbyFs
      • proof: Functional correctness specs and proofs for BilbyFs
    • ext2: ext2 file system
      • cogent: Cogent code for ext2
• regression: Regression test script

The Gencot Tool

Gencot is a tool for translating C code to Cogent. It's developed by our collaborators. The repository is hosted on Github. See the README file and the documentation for more details.

cogent's Issues

regression in typechecker?

For the file added in 1cbb157 [cogent/tests/pass_none-subtyping.cogent], the old TC is happy with it, but the new one says:

Typechecking...
Cannot discard type Obj but this is needed as it is implicitly taken via subtyping.
   from constraint < None 
                   | Some A > take Some :< < None | Some (A take (..)) >
   from constraint { f1 : Obj, f2 : U8 } :< { f1 : Obj, f2 : U8 } take (f1, f2)
   from constraint Obj :< Obj :& Drop Obj :& U8 :< U8 :& Drop U8
   when checking the expression at ("./tests/pass_none-subtyping.cogent" (line 12, column 15))
   in the 2nd alternative none
   in the definition at ("./tests/pass_none-subtyping.cogent" (line 8, column 1))
   for the function foo
Compilation failed!

const vs. func

foo : U32
foo = let x = bar 1
       in x + 3

bar : U32 -> U32

is accepted by the compiler, whereas foo is not necessarily a constant.

poly : all a. a
poly = poly' ()

poly' : all a. () -> a

fails to parse (because const can't have a poklytype) so cannot be made a constant.

Do we still have a reason to differentiate functions and constants? Will the code generator or verification toolchain do something bad with the first code snippet?

record fields get permuted in solver

Pattern location and error reporting

see commit message c7f2c20 for tasks.

--ftc-ctx-len not working properly

Error message for Integer type mismatch

Now it says something like:

Mismatch between
   U16
and
   U32
   from constraint U16 :< U32
   when checking that the expression at ("fail_large-code.cogent" (line 244, column 80))
      const_ext2Magic
   has type
      U32

Can be better.

calling functions from .ac

Symptom 1: if we use the polymorphic version of f in file cogent.cogent and include f in entry file, then the compile crashes!
Symptom 2: if we use the Char version, the compiler doesn't recognise Char as a primitive type.
Symptom 3: the top-level entrypoint functions have to be monomorphic, which is a limitation atm.

`Drop var` constraint not solved

To compile

type RbtConsumeF k v acc obsv = RbtElemAO k v acc obsv -> acc
type RbtCondF k v acc obsv = (RbtElemAO k v acc obsv)! -> Bool

rbtFTrue: all(k:< DS, v :<DS, acc, obsv). RbtCondF k v acc obsv
rbtFTrue _ = True

I got:

Leftover constraint!
Drop acc
   in the 1st alternative _
   in the definition at ("rbt.cogent" (line 91, column 1))
   for the function rbtFTrue
Leftover constraint!
Drop obsv
   in the 1st alternative _
   in the definition at ("rbt.cogent" (line 91, column 1))
   for the function rbtFTrue

I don't think it's the same bug as #29, as type arguments are applied while calling rbtFTrue.

Inferencer fails to figure out ! on typevars

Synopsis

The Problem

In a nutshell, if there's a function whose type includes a forall quantified type variable a (for example) and a! appears in the type signature, then it's very likely you'll encounter a constraint of the form (?0)! :< T which is unsolvable by the constraint solver and you'll get a typecheck error of leftover constraints.

The Solution

If possible, avoid this form of type signature. Instead, use explicit constraints, like forall (a :< DS). .... There're cases where it is impossible to do so. In that case, you have to explicitly do the type application like f [U8, Bool, A] yourself. Note that partial type application is allowed, and holes are supported so you can only apply the type that is in question. E.g. f [_, Bool].

Also see discussion in #22 and 255f000

context order

f2853a5 is not sufficient. SolvingConstraints are in reverse order.

take/put unsoundness

Can take a linear field multiple times.
Can put a linear field multiple times.

Required fields taken

More travis cache

We can do a bit smarter for Cogent package dependencies. If the new deps have the same version as those of the previous build, just use the cached ones, otherwise reinstall new deps.

libgum not installed properly if `cabal build`

Var vs. Function in error messages

When a function is not defined, sometimes it says "function not found", sometimes "variable not in scope".

Improving "leftover constraints" errors

No guessing in variant types. For more details see discussions below. Symptom: left-over constraints with an Exhaustive constraint. We might want to enhance it in some future.

new typechecker performance

We can solve a lot of performance problems by:

• Coalescing equal constraints rather than LUBing/GLBing them.
• (Possibly) applying substitutions to fixed point in the substitutions themselves (not sure if this is a win)
• other things?

What and Why in README

The README is excellent for installation and so on but lacks description of what Cogent does and why I would want it.

The project was referred to me as:

"This is NICTA/Data61's new language for writing systems code that from a high level DSL generates both efficient run time code and a proof of correctness that can be checked by the Isobelle theorem prover."

I was unable to glean that from the README but the problem may also just be me :-)

Thanks!

PP for typed ast

parser bug

type Option a = <Some a | None>

type A = {f1 : Obj, f2 : U8}
type Obj

free : Obj -> ()

foo : Option A -> Option (A take (..))
foo | Some a -> let a_t {f1} = a
                and _ = free f1
                 in Some a_t
    | none -> none

parses OK. If we put the pattern Some a in parens, then it's rejected:

zilinc@zilinc-dell-xps:~/nicta/ts/cogent-public/cogent$ cogent -t tests/pass_none-subtyping.cogent 
Parsing...
"./tests/pass_none-subtyping.cogent" (line 9, column 13):
unexpected Some
expecting irrefutable pattern
Compilation failed!

Error messages (esp. contexts) can be bad again due to #50, please report!

Syntax highlight for .congent?

Hi there,

Are there any possible syntax highlight for .cogent at text editor such as vim or sublime?

Thanks!

---

Found it at dir cogent/

porting libgum to new language style

• remove typearg applications
• use kinds instead of ! on type vars

Bang function types

In the old compiler, (A->B)! == A -> B, and now (A->B)! == A! -> B!. Which is more appropriate?

new syntax: `type` defines multiple types

type A, B, C

Cogent Macros

Just as a reminder and placeholder for now. No concrete ideas atm.

Unnecessarily mandatory `upcast`

In some cases the compiler can infer the integral types. We might want to do so? as they occur a lot.
(This is part of our syntactic improvements)

Q: In which cases is an upcast necessary to help the compile make a decision?

generate manpage

Generate a Cogent manpage with cabal install

porting the desugarer to the new typechecker

This is actually a substantial bit of work.

We need to:

• Add a pass to add "promote" nodes for subtyping (the existing "promote" infrastructure is no longer needed). I (@liamoc) can do this. I'm going to try and do this at the same time as core typechecking or just after.
• Adapting the core AST to include widen (for integer) and promote (for subtyping) nodes.
• Adapt the existing desugarer to deal with the new type system. I think we should make it so that instead of outputting UntypedExpr t v VarName it produces UntypedExpr t v (VarName, RawType). That should work nicely and mean we can get rid of most of the actual type checking in the core type checker, which might be good.

Once this is done, I can write the core type checker.

Giant error message

If we run cogent -t impl/ext2/cogent/fs/super.cogent under 0859d9e, we'll see a larrrrrrrrrrge error. funny!

generate all types and functions that are not mentioned when possible

Can be a flag.

Now the compiler only generates things that are either mentioned (transitively) in the entry-point file or in Cogent code. For monomorphic functions and types, we can selectively blindly generate all of them.

Or add types also in the entry-point file.

Also we'd like to generate constant definitions in C.

"bound at" information isn't very precise.

This program doesn't look correct but typechecks:

foo : all a. (a, a!) -> a

type A

bar : (A, A) -> A
bar (a,a') = let a'' = foo (a, a') !a'
              in a''

Update vfat and ext2fs implementations to build/run against the latest kernel

Our implementation of both ext2 and vfat in Cogent is a little dated, and we need to update it to build against the latest kernel implementation.
Currently, it works against the patched 4.3 kernel in Debian, but doesn't build on the Arch's kernel.

Makefile for cogent compiler should keep sandbox

installing deps takes ages, so if possible we'd like to keep the sandbox (even in make clean maybe), unless it's terribly broken. I propose a realclean target, and should be used with caution.

Order of TC errors

If there're more than 1 error in a compilation unit, the number of errors and the order it reports them are different from the old compiler.

• need to figure out in what cases multiple errors can be reported in one go (todo)
• the first error doesn't seem always to be the root cause (fixme)
• some test files to illustrate this phenomenon (todo)

include <> syntax highlight

type well-formedness not checked

they're mostly the passing tests that should fail as in ff23824.
where is the best place to check?

A flag to switch on/off constraints in TC error messages

examples in doc and testsuite

There'd be a top-level pointer which new users can find and follow.
Also good to include them in CI.

update license headers

We should now gradually change from NICTA to Data61.

1st alternative

foo : A -> B
foo a = ...

the compiler will report 1st alternative (a) even there's only one top-level alt.

Widen unresolved

type X = <A U8 | B Bool>

f : () -> X
f _ = if True then widen (A 3) else widen (B False)

ends up with error message

Leftover constraint!
< > :<~ ?0 :& < A U8 > :<~ ?0
   in the definition at ("./test.cogent" (line 3, column 1))
   for the function f
   in the 1st alternative (_)
   when checking that the expression at ("./test.cogent" (line 4, column 7))
      if True then widen (A 3) else widen (B False)
   has type
      X
   in the then branch
   when checking the expression at ("./test.cogent" (line 4, column 20))
Leftover constraint!
< > :<~ ?2 :& < B Bool > :<~ ?2
   in the definition at ("./test.cogent" (line 3, column 1))
   for the function f
   in the 1st alternative (_)
   when checking that the expression at ("./test.cogent" (line 4, column 7))
      if True then widen (A 3) else widen (B False)
   has type
      X
   in the else branch
   when checking the expression at ("./test.cogent" (line 4, column 37))

cogent/README.md is not in markdown format

It used to be a plain txt file...

partial records not solved correctly

TC subtyping bug

See file cogent/tests/pass_weird_ext2_error.cogent in 7e09138.

record wildcard

This is a case where it's particularly bad without record wildcard:

deserialise_into_Ext2Superblock: (ExState, OSBuffer!, Ext2Superblock take (..), U32) -> RR (ExState) (Ext2Superblock, U32) (Ext2Superblock take (..))
deserialise_into_Ext2Superblock (ex, buf, obj_t, idx) =
    osbuffer_deserialise_Ple32 (buf, idx)
    | Success (inode_count, idx) ->
        osbuffer_deserialise_Ple32 (buf, idx)
        | Success (block_count, idx) ->
            osbuffer_deserialise_Ple32 (buf, idx + 4) -- skip 1 U32 field
            | Success (free_block_count, idx) ->
                osbuffer_deserialise_Ple32 (buf, idx)
                | Success (free_inode_count, idx) ->
                    osbuffer_deserialise_Ple32 (buf, idx)
                    | Success (first_data_block, idx) ->
                        osbuffer_deserialise_Ple32 (buf, idx)
                        | Success (block_size_lg2, idx) ->
                            osbuffer_deserialise_Ple32 (buf, idx + 4) -- skip 1 U32 field
                            | Success (blocks_per_group, idx) ->
                                osbuffer_deserialise_Ple32 (buf, idx)
                                | Success (fragments_per_group, idx) ->
                                    osbuffer_deserialise_Ple32 (buf, idx)
                                    | Success (inodes_per_group, idx) ->
                                        osbuffer_deserialise_Ple16 (buf, idx + (3 * 4)) -- skip 4 fields (2x U16, 2xU32 = 3xU32) 
                                        | Success (magic, idx) ->
                                            let -- obj = obj_t { .. }
                                                obj = obj_t { inode_count
                                                            , block_count
                                                            , free_block_count 
                                                            , free_inode_count
                                                            , first_data_block
                                                            , block_size_lg2
                                                            , blocks_per_group
                                                            , fragments_per_group
                                                            , inodes_per_group
                                                            , magic
                                                            }
                                            in (ex, Success (obj, idx))
                                        | Error () -> (ex, Error (obj_t))
                                    | Error () -> (ex, Error (obj_t))
                                | Error () -> (ex, Error (obj_t))
                            | Error () -> (ex, Error (obj_t))
                        | Error () -> (ex, Error (obj_t))
                    | Error () -> (ex, Error (obj_t))
                | Error () -> (ex, Error (obj_t))
            | Error () -> (ex, Error (obj_t))
        | Error () -> (ex, Error (obj_t))
    | Error () -> (ex, Error (obj_t))

Luckily this problem will go once we have DDSL again.

Error message when C variables are surrounded by $exp

For antiQ C code like the following:

$ty:(Foo) foo;
foo->item = 12;
$exp:(some_cogent_function(foo));

The compiler returns the error message:
cogent: desugarExpr (Error): the 'impossible' happened!

The actual error is that foo is actually a variable in C, but surrounding the argument by $exp as well makes the compiler treat it as a Cogent variable, where it is undefined.

`toRawType` panic

Trying on tests/pass_case-default.cogent, if giving compiler -t, it's OK; if giving --ast-tc, that function panics.

typechecker forgetful?

As in the file below, None _ fails because the compiler cannot infer what the type _ has. However it should know it's casing on an Option Ext2DirEnt type where None () is the type. In fact, if you tell the compiler that _ has some type, it always believes.

type synonyms not expanded properly

F is not a function type
   in the definition at ("./tests/pass_fun-type-synonym.cogent" (line 3, column 1))
   for the function foo