Pact checking #422

joelburget · 2019-03-05T00:15:25Z

Feedback please. Things that still need to be done:

Emit trace steps for resets (@bts I started working on this but had some trouble with it -- if you want to tackle it that would be amazing. If not I can continue with your guidance). Edit: now done
The method we currently use for resets is pretty lame -- we just free everything that could be changed between steps, without considering what could actually be changed with the API presented by the module. This is pretty weak (in terms of what we can prove). It would be better to take the closure of sequences of operations available in the module. Unfortunately I'm not sure how to do this. Also I'm not sure which things need to be freed between steps in the current method.
If someone declares (property (= (column-delta accounts 'balance) 1)) for a pact, does that mean that the sum of that column is the same when the pact finishes executing, or that the code in the pact itself doesn't change the sum of the column? Edit: we're going with the latter
Need to do a lot of testing. This is partly dependent on questions like the previous.
Note: please ignore that I commented out all the other tests

src/Pact/Analyze/Translate.hs

bts · 2019-03-06T21:17:29Z

I can add the trace steps once I take care of the pending capability analysis tweaks I need to finish up

Sans testing.

src/Pact/Analyze/Model/Text.hs

src/Pact/Analyze/Translate.hs

src/Pact/Analyze/Eval/Term.hs

(After the first)

We were mistakenly translating pacts as defuns causing test failures.

(used in the previous commit to make debugging easier)

src/Pact/Analyze/Eval/Term.hs

At this point we generate the correct graph for the failure of the last pact test -- the very last test in the test suite.

Fixes: 1. We had mistakenly reversed the order of cancels and rollbacks in pact translation. 2. In evaluation we had (nondeterministically) tagged some rollbacks as triggering, even though their corresponding step had not run.

src/Pact/Analyze/Eval/Term.hs

* reset registry * reset `aeGuardPasses` * unset any `rowExists` that are set to false.

Rollback steps are executed all at once.

This fails to parse in CI.

Also, several cosmetic cleanups in AnalyzeSpec.

src/Pact/Analyze/Types/Eval.hs

src/Pact/Analyze/Translate.hs

src/Pact/Analyze/Model/Tags.hs

src/Pact/Analyze/Eval/Term.hs

src/Pact/Analyze/Eval.hs

bts

We're very close. Mainly a naming question

Primarily, renaming "nondets" to "pactSteps".

joelburget requested a review from bts March 5, 2019 00:15

bts reviewed Mar 6, 2019

View reviewed changes

src/Pact/Analyze/Translate.hs Outdated Show resolved Hide resolved

joelburget added 4 commits March 8, 2019 08:19

Pact analysis.

f69f815

Several things which I thought were good ideas weren't.

2caddac

Fix pact evaluation control flow.

1296ce6

Sans testing.

Implement withVar TODO.

fdd814a

joelburget force-pushed the pact-checking branch from dc557ce to fdd814a Compare March 8, 2019 16:34

joelburget added 3 commits March 8, 2019 08:47

Fix nondet allocation for new sbv version.

98cd036

Simplify since we can check pacts and functions in the same way.

412910e

Update second pact example test.

30c0be5

bts reviewed Mar 11, 2019

View reviewed changes

src/Pact/Analyze/Model/Text.hs Outdated Show resolved Hide resolved

bts reviewed Mar 11, 2019

View reviewed changes

src/Pact/Analyze/Translate.hs Outdated Show resolved Hide resolved

bts reviewed Mar 11, 2019

View reviewed changes

src/Pact/Analyze/Eval/Term.hs Outdated Show resolved Hide resolved

joelburget added 3 commits March 11, 2019 15:56

Remove some old tracing.

f663780

Update pact checking to work with the graph.

d37f801

Update for review feedback.

1c8907c

joelburget force-pushed the pact-checking branch from 76e0eae to 1c8907c Compare March 11, 2019 23:02

joelburget and others added 9 commits March 11, 2019 16:21

Make sure there's a cancel vid for every step.

82a3734

(After the first)

Fix broken pact translation.

6ee92a1

We were mistakenly translating pacts as defuns causing test failures.

Implement describeVerificationFailure.

4a468e4

(used in the previous commit to make debugging easier)

WIP: paired graph changes

b4f5e01

Fill in Languages boilerplate after Step changes.

c978d3c

Sketch of a pact evaluation tagging idea.

db57f04

Don't tag subpath start for first step.

6f43bf5

Fix cancel / success mixup.

9a3252e

More explicit lack of cancellation in first step.

a8deda8

bts reviewed Mar 13, 2019

View reviewed changes

src/Pact/Analyze/Eval/Term.hs Outdated Show resolved Hide resolved

bts reviewed Mar 13, 2019

View reviewed changes

src/Pact/Analyze/Eval/Term.hs Outdated Show resolved Hide resolved

bts reviewed Mar 13, 2019

View reviewed changes

src/Pact/Analyze/Eval/Term.hs Outdated Show resolved Hide resolved

bts and others added 8 commits March 19, 2019 11:14

Always set path head after extending

783987f

Emit subpath event for cancel path

adc4b5e

Use startNewSubpath helper

c62ae70

Fix graph generation for simple pact failure.

8e29d91

At this point we generate the correct graph for the failure of the last pact test -- the very last test in the test suite.

Add messaging to example so we can see which path executes.

ccc5121

Add a bit of pact testing.

4719bed

Add many-step pact tests and fixes.

d4b43bc

Fixes: 1. We had mistakenly reversed the order of cancels and rollbacks in pact translation. 2. In evaluation we had (nondeterministically) tagged some rollbacks as triggering, even though their corresponding step had not run.

Clean up / document pact translation.

dd92b96

bts reviewed Mar 20, 2019

View reviewed changes

src/Pact/Analyze/Eval/Term.hs Outdated Show resolved Hide resolved

joelburget added 7 commits March 25, 2019 13:49

More work on pacts.

bdbbe71

Finish resetting everything between pacts.

dcfedd3

* reset registry * reset `aeGuardPasses` * unset any `rowExists` that are set to false.

Remove unnecesary resets.

6edb3b4

Rollback steps are executed all at once.

Re-enable non-pact tests.

68c2ece

Merge branch 'master' of github.com:kadena-io/pact into pact-checking

6bda324

Check in generated documentation.

115e898

Remove haddock-style comments from GADT-style declaration.

80bd275

This fails to parse in CI.

joelburget marked this pull request as ready for review March 27, 2019 15:15

joelburget added 2 commits March 27, 2019 11:26

Add testing of single-step pact.

61e1fa5

Also, several cosmetic cleanups in AnalyzeSpec.

A few notes / cleanups.

40b15d5

bts reviewed Mar 27, 2019

View reviewed changes

src/Pact/Analyze/Types/Eval.hs Outdated Show resolved Hide resolved

bts reviewed Mar 27, 2019

View reviewed changes

src/Pact/Analyze/Translate.hs Outdated Show resolved Hide resolved

bts reviewed Mar 27, 2019

View reviewed changes

src/Pact/Analyze/Model/Tags.hs Outdated Show resolved Hide resolved

bts reviewed Mar 27, 2019

View reviewed changes

src/Pact/Analyze/Eval/Term.hs Outdated Show resolved Hide resolved

bts reviewed Mar 27, 2019

View reviewed changes

src/Pact/Analyze/Eval.hs Outdated Show resolved Hide resolved

bts suggested changes Mar 27, 2019

View reviewed changes

joelburget added 2 commits March 27, 2019 12:51

Address review feedback.

265c779

Primarily, renaming "nondets" to "pactSteps".

Merge branch 'master' of github.com:kadena-io/pact into pact-checking

d84d33d

bts approved these changes Mar 28, 2019

View reviewed changes

bts merged commit e594d43 into master Mar 28, 2019

bts deleted the pact-checking branch March 28, 2019 01:36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Pact checking #422

Pact checking #422

joelburget commented Mar 5, 2019 •

edited

bts commented Mar 6, 2019

bts left a comment

Pact checking #422

Pact checking #422

Conversation

joelburget commented Mar 5, 2019 • edited

bts commented Mar 6, 2019

bts left a comment

Choose a reason for hiding this comment

joelburget commented Mar 5, 2019 •

edited