Pomagma

Pomagma is an inference engine for extensional untyped λ-join-calculus, a simple model of computation in which nondeterminism gives rise to an elegant gradual type system.

Pomagma can:

simplify code fragments expressed in λ-join-calculus
validate codebases of programs and assertions
solve systems of inequalities and horn clauses
synthesize code from sketches and inequality constraints

Pomagma's base theory is being formally verified in the Hstar project.

Pomagma's architecture follows a client-server model, where a Python client library performs high-level syntactic tasks, and a shared C++ database server performs low-level inference work.

Installing

The server targets Ubuntu 14.04 and 12.04, and installs in a python virtualenv.

git clone https://github.com/fritzo/pomagma
cd pomagma
. install.sh
make small-test     # takes ~5 CPU minutes
make test           # takes ~1 CPU hour

The client library supports Python 2.7.

pip install pomagma

Quick Start

Start a local analysis server with the tiny pre-built atlas

pomagma analyze             # starts server, Ctrl-C to quit

Then in another terminal, start an interactive python client session

$ pomagma connect           # starts a client session, Ctrl-D to quit
>>> simplify(['APP I I'])
[I]
>>> validate(['I'])
[{'is_bot': False, 'is_top': False}]
>>> solve('x', 'EQUAL x APP x x', max_solutions=4)
['I', 'BOT', 'TOP', 'V']
>>> validate_facts(['EQUAL x TOP', 'LESS x BOT'])
False

Alternatively, connect using the Python client library

python
from pomagma import analyst
with analyst.connect() as db:
    print db.simplify(["APP I I"])
    print db.validate(["I"])
    print db.solve('x', 'EQUAL x APP x x', max_solutions=4)
    print db.validate_facts(['EQUAL x TOP', 'LESS x BOT'])

Get an Atlas

Pomagma reasons about large programs by approximately locating code fragments in an atlas of 10³-10⁵ basic programs. The more basic programs in an atlas, the more accurate pomagma's analysis will be. Pomagma ships with a tiny pre-built atlas of ~2000 basic programs.

To get a large pre-built atlas, put your AWS credentials in the environment and

export AWS_ACCESS_KEY_ID=...        # put your id here
export AWS_SECRET_ACCESS_KEY=...    # put your hey here
pomagma pull                        # downloads latest atlas from S3

To start building a custom atlas from scratch

pomagma make max_size=10000         # kill and restart at any time

Pomagma is parallelized and needs lots of memory to build a large atlas.

Atlas Size	Compute Time	Memory Space	Storage Space
1 000 atoms	~1 CPU hour	~10MB	~1MB
10 000 atoms	~1 CPU week	~1GB	~100MB
100 000 atoms	~1 CPU year	~100GB	~10GB

License

Pomagma ships with the Google Farmhash library, licensed under the MIT license.