Trace Reconstruction #2

RoryBrennan-Jones · 2024-07-31T17:21:07Z

Major Changes

Test Suite

In the lcf directory, running make test will verify the go predicate of every Datalog+ file in the tests directory. The results are saved as .thm files with names matching the original code files. Using the Python script in the tools directory, it is possible to randomly generate example Datalog+ programs involving edge connectivity problems.

New Trace Reconstruction Algorithm

The trace output of a Prolog program shows an exploration of many possible paths before settling on one that allows the query to be true or resolves some unification. The new trace reconstruction algorithm attempts to discard all the failed paths and look at just the successful path, which greatly simplifies the process of constructing a proof tree for that query. The algorithm does this by only looking at trace events that use the exit port, since these events result from successes and contain full variable assignments. However, failed paths can have zero or more temporary successes, potentially leading to the presence of "junk" events with exit ports in the trace output.

Since exit ports always follow successes, the first exit ports in the trace happen after finding succesful base cases (builtin operations, facts, etc.), and later exit ports show the successes of predicates that depended on other rules and facts. As a result, the algorithm reads from the trace backwards in order to go from the root to the leaves instead of vice versa. The algorithm uses a mix of recursion and iteration, where the recursion helps the algorithm move "up" and "down" the tree, and the iteration helps algorithm move between siblings in the tree and skip junk events. A trace event with a prop such as a fact, equality, or builtin becomes a leaf in the proof tree, whereas other trace events become regular theorems that have proofs using other theorems and leaves from lower down in the tree as arguments.

Support for Types and Builtins

Unlike Datalog, Datalog+ supports constants other than atoms, including numbers, strings, and lists. These types are not complete yet. It has not been decided yet if the numbers should be natural numbers or integers (or if both should be supported). Furthermore, strings do not support all characters that could be found in a legal Datalog+ string, including escaped characters such as double quotes. Also, lists currently only support constant terms and cannot use the pipe operator. In addition to these types, there is also support for certain builtin operations, such as equality operators and string and list builtins.

…d changing the trace parsing

…, allowing me to remove bound

… which requires one less parameter

…struct to function

… are parsed as nats or atoms

…e a few changes to the Dafny kernel

mmcloughlin · 2024-08-01T18:08:19Z

dafny/lcf/.gitignore

 *.dll
+# Test outputs
+*.trace
+*.thm


Please could we fix the missing newlines at the end of files? I think there's a few examples of it in this PR.

I think there's a vscode setting for this: https://stackoverflow.com/a/44704969

mmcloughlin · 2024-08-01T18:11:38Z

dafny/lcf/README.md

@@ -0,0 +1,20 @@
+## Project Overview
+
+The Veri-Datalog project is a verified Datalog+ engine. It proves the correctness of Datalog+ programs by constructing proof trees from their trace output. Datalog+ is a research defined language that is similar to Datalog but with more feature support; both are subsets of Prolog.


nit: wrap paragraphs to some reasonable width, 100 or 120 characters perhaps?

mmcloughlin · 2024-08-01T18:12:00Z

dafny/lcf/README.md

+
+The Veri-Datalog project is a verified Datalog+ engine. It proves the correctness of Datalog+ programs by constructing proof trees from their trace output. Datalog+ is a research defined language that is similar to Datalog but with more feature support; both are subsets of Prolog.
+
+## Contributions by Rory Brennan-Jones


Perhaps remove this heading? We know it was your work, but I don't think the README needs to say that.

mmcloughlin · 2024-08-01T18:12:26Z

dafny/lcf/datalog.g4

@@ -9,7 +9,7 @@ trace
  ;

 traceevent
-  : port level=integer id=integer goal=clause ';'
+  : port level=integer id=integer goal=clause';'


nit: keep the space after clause?

mmcloughlin · 2024-08-01T18:14:52Z

dafny/lcf/datalog.g4

  ;

 atom
  : val=Identifier
  ;

+natural
+  : numeral=Int // TODO: make natural use the Nat rule, or switch support from natural numbers to integers


Is there a reason we can't do this TODO now?

It's odd to have a rule called natural actually be an integer. I'd suggest we either rename natural to integer, or change Int to Nat. Either is fine, just the mixed naming is odd right now.

As I mentioned in person, this may have to stay unresolved for now. To summarize, the kernel only supports natural numbers right now, but the Nat lexer rule in the parser doesn't seem to work.

Agreed that the naming issue is worth resolving now, if we can.

I have resolved the naming issue. The Int lexer rule has been commented out, and the rest of the Antlr uses the Nat rule.

mmcloughlin · 2024-08-01T18:22:33Z

dafny/lcf/tools/connectivity_generator.py

+    print(f'destination("{p.dst}").', file=out)
+
+
+def _write_datalog(p, out): # cls


Probably remove the _ prefix in the function name.

mmcloughlin · 2024-08-01T18:25:05Z

dafny/lcf/tools/connectivity_generator.py

+    # Query.
+    # print(f'{cls.QUERY_NAME}(S, D) :- source(S), destination(D), connected(S, D).', file=out)
+
+_write_datalog(random_connectivity_problem(100), sys.stdout)


Can you wrap this in the usual Python boilerplate:

def main(): write_datalog(random_connectivity_problem(100), sys.stdout) if __name__ == "__main__": main()

https://stackoverflow.com/questions/419163/what-does-if-name-main-do

mmcloughlin · 2024-08-01T18:28:23Z

dafny/lcf/tests/connectivity1.pl

If I recall, some of these tests had interesting trace features that triggered bugs in prior failed versions of trace reconstruction.

Are you able to provide comments where appropriate explaining what properties they have which make them interesting cases.

I guess the parser may not support comments right now? In which case, can you add your comments to tests/README.md or something?

I added some comments in README, although I might need to write more than what I currently have.

mmcloughlin · 2024-08-01T18:31:12Z

dafny/lcf/def.dfy

+function lower_char(c : char) : char {
+  match (c)
+  case 'A' => 'a'
+  case 'B' => 'b'
+  case 'C' => 'c'
+  case 'D' => 'd'
+  case 'E' => 'e'
+  case 'F' => 'f'
+  case 'G' => 'g'
+  case 'H' => 'h'
+  case 'I' => 'i'
+  case 'J' => 'j'
+  case 'K' => 'k'
+  case 'L' => 'l'
+  case 'M' => 'm'
+  case 'N' => 'n'
+  case 'O' => 'o'
+  case 'P' => 'p'
+  case 'Q' => 'q'
+  case 'R' => 'r'
+  case 'S' => 's'
+  case 'T' => 't'
+  case 'U' => 'u'
+  case 'V' => 'v'
+  case 'W' => 'w'
+  case 'X' => 'x'
+  case 'Y' => 'y'
+  case 'Z' => 'z'
+  case _ => c
+}


I think you may be able to rewrite this by converting to integer with (c as int), doing the ascii math, and converting back with (... as char).

https://dafny.org/dafny/DafnyRef/DafnyRef.html#sec-characters

mmcloughlin · 2024-08-01T18:31:48Z

dafny/lcf/def.dfy

        match strings(parts.l) {
-          case Ok(parts_strings) => str.s == string_join(sep.s, parts_strings)
+          case Ok(parts_strings) => str.s == string_join(sep.s, parts_strings) // TODO: add support for padding


Okay to not implement it, but it would be good if the code errors when a non-empty padding is passed in.

pratapsingh1729

Great work! I think Mike already made most of the comments, so I think this can be merged as-is.

pratapsingh1729 · 2024-08-01T21:02:04Z

dafny/lcf/datalog.g4

  ;

 atom
  : val=Identifier
  ;

+natural
+  : numeral=Int // TODO: make natural use the Nat rule, or switch support from natural numbers to integers


Agreed that the naming issue is worth resolving now, if we can.

pratapsingh1729 · 2024-08-01T21:06:01Z

dafny/lcf/README.md

+the pipe operator. In addition to these types, there is also support for
+certain builtin operations, such as equality operators and string and list
+builtins.
+


Is it possible to add a list of the primitives that we currently do support? For instance, which comparison operators are supported for numbers?

Sure, I added a few lists to the readme.

pratapsingh1729 · 2024-08-01T21:10:15Z

dafny/lcf/def.dfy

+        invariant |trace'| < |trace|
+        invariant forall j :: 0 <= j < |args| ==> args[j].wf(rs)
+      {
+        // This while loop skips over all ineligble trace events until it finds one that matches with the next child rule.


How does it determine the match? I guess just by seeing if the substitutions line up?

Yes, more or less.

pratapsingh1729 · 2024-08-01T21:10:40Z

dafny/lcf/def.dfy

-  // Deduce theorem.
-  var root := outcome.nodes[0];
-  var maybe_match := reconstruct(root, root.prop, rs);
+  print "tree:\n"; // if there was a flag that disabled printing in build_proof_tree, this line should be disabled as well


What does this comment refer to?

"// Deduce theorem" refers to the section where the theorem object is created.
"// if there was a flag, ..." is a note that in Verus port, this line will be enabled by a flag. (If the user doesn't want the tree to be printed out, they wouldn't want "tree:" to be printed.)

add deep views

mmcloughlin and others added 30 commits June 12, 2024 10:59

comment out old trace reconstruction code

ab9c4b6

wip

11938f0

implemented wip solutions for reconstruct and build_trace_tree

005b519

implemented different fix for build_trace_reconstruction that involve…

efbef7c

…d changing the trace parsing

included additional comments and a new test case

11e73be

implemented exit-only trace building technique

f3be6d8

Convinced Dafny that |trace| was being decreased in build_trace_tree2…

f4efe32

…, allowing me to remove bound

Convinced Dafny that the trace is required to be concrete

7afbec6

Convinced Dafny that the returned trace tree is wf

ebbfd64

Performed code surgery on build_trace_tree2 to get build_trace_tree3,…

2986a42

… which requires one less parameter

Created build_proof_tree and slightly enhanced trace.pl

a453727

Removed match from build_proof_tree, as it was created to allow recon…

189b11d

…struct to function

There was a mk_thm that used head.i instead of ri, so I fixed that

64843d4

Added an ensures and an invariant, and removed two assumes

13feca4

Removed unnecessary comments

de7f272

Changed comments in def.dfy

2f27b15

Added parser support for predicates without arguments

c01aa06

Experimented with makefile and trace.pl in preparation for test suite

f026007

Added test suite

2ea9437

Created new test case

d560d23

Created limited, experimental parser support for numbers

bf14157

Added parser rule for constants

925c59d

Began adding support for strings, but encountered issue where strings…

329465c

… are parsed as nats or atoms

Strings are now supported

17834a0

Added new test

ef7b2d9

Implemented support for builtin operations involving numbers, and mad…

be6a50b

…e a few changes to the Dafny kernel

Moved around code in a way that did not effect functionality

6978483

Made small change

908a9a8

Added support for two more operators

8ad939a

Made minor change

a2443b1

RoryBrennan-Jones added 2 commits July 31, 2024 12:16

Changed README.md

e892cc1

Changed README.md

52b96fb

pratapsingh1729 requested review from mmcloughlin and pratapsingh1729 August 1, 2024 15:02

mmcloughlin reviewed Aug 1, 2024

View reviewed changes

RoryBrennan-Jones added 17 commits August 1, 2024 14:45

Added final newlines

b5e93fc

Reformatted README

822249f

Removed heading in README

28ab87e

Minor changes to Python script

43a92a7

Addressed issue with escaping

2705f6b

Actually fixed issue with escaping

eac52a9

Cleaned up VisitString

323233e

Cleaned up VisitBuiltin and VisitExpression

19359d4

Disabled support for escaped double quotes because of resulting bugs

0a10520

Cleaned up VisitBuiltin

7a7f372

Added back the removed space

47d0914

Cleaned up switch statement

adfc803

Updated Python script to use main method

8d61cc6

Cleaned up lower_char

4ac2338

Made use of padchars in split string illegal for now

e9ac6c5

Expanded README

b3b635b

Added missing final newline

04b3a71

pratapsingh1729 reviewed Aug 1, 2024

View reviewed changes

RoryBrennan-Jones added 4 commits August 2, 2024 08:51

Updated readme

7dd1cb0

Updated readme

8b3d786

Fixed naming issue involving natural numbers

ae4da38

Changed readme

55c5b56

pratapsingh1729 pushed a commit that referenced this pull request Aug 2, 2024

Merge pull request #2 from eobardthawne21p/pratap-deepviews

23f4f27

add deep views

Removed comment

abc81b5

mmcloughlin merged commit 3e23775 into secure-foundations:trace-reconstruction Aug 2, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Trace Reconstruction #2

Trace Reconstruction #2

RoryBrennan-Jones commented Jul 31, 2024

mmcloughlin Aug 1, 2024

RoryBrennan-Jones Aug 1, 2024

mmcloughlin Aug 1, 2024

mmcloughlin Aug 1, 2024

RoryBrennan-Jones Aug 1, 2024

mmcloughlin Aug 1, 2024

RoryBrennan-Jones Aug 1, 2024

mmcloughlin Aug 1, 2024

RoryBrennan-Jones Aug 1, 2024

pratapsingh1729 Aug 1, 2024

RoryBrennan-Jones Aug 2, 2024 •

edited

Loading

mmcloughlin Aug 1, 2024

RoryBrennan-Jones Aug 1, 2024

mmcloughlin Aug 1, 2024

RoryBrennan-Jones Aug 1, 2024

mmcloughlin Aug 1, 2024

RoryBrennan-Jones Aug 1, 2024

mmcloughlin Aug 1, 2024

RoryBrennan-Jones Aug 1, 2024

mmcloughlin Aug 1, 2024

RoryBrennan-Jones Aug 1, 2024

pratapsingh1729 left a comment

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

RoryBrennan-Jones Aug 2, 2024

pratapsingh1729 Aug 1, 2024

RoryBrennan-Jones Aug 2, 2024

pratapsingh1729 Aug 1, 2024

RoryBrennan-Jones Aug 2, 2024

		@@ -0,0 +1,20 @@
		## Project Overview

		The Veri-Datalog project is a verified Datalog+ engine. It proves the correctness of Datalog+ programs by constructing proof trees from their trace output. Datalog+ is a research defined language that is similar to Datalog but with more feature support; both are subsets of Prolog.


		The Veri-Datalog project is a verified Datalog+ engine. It proves the correctness of Datalog+ programs by constructing proof trees from their trace output. Datalog+ is a research defined language that is similar to Datalog but with more feature support; both are subsets of Prolog.

		## Contributions by Rory Brennan-Jones

		print(f'destination("{p.dst}").', file=out)


		def _write_datalog(p, out): # cls

Trace Reconstruction #2

Trace Reconstruction #2

Conversation

RoryBrennan-Jones commented Jul 31, 2024

Major Changes

Test Suite

New Trace Reconstruction Algorithm

Support for Types and Builtins

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RoryBrennan-Jones Aug 2, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pratapsingh1729 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RoryBrennan-Jones Aug 2, 2024 •

edited

Loading