Verusport #3

eobardthawne21p · 2024-08-01T05:43:06Z

Updates to codebase:

I added the files for TmpStringHashMap, Verusport, README.md, and main.rs. In README.md, all major information was included, and I tried to be as thorough as possible. Verusport contains a toy example as the end for an edge connectivity problem, but we need to work on tst_connected_thm later due to verification errors.

import string_hash_map axiomatization

add deep views

…atalog into verusport

verus/lcf/src/verusport.rs

mmcloughlin · 2024-08-01T19:33:35Z

verus/lcf/README.md

+Term types are enums that have 2 variants:
+1. Const(Const)
+2. Var(String)
+
+Its spec versions for SpecTerm are:
+1. Const(SpecConst)
+2. Var(Seq<char>)
+
+Functions that can be used on Term types:
+1. (in impl DeepView for Term) open spec fn deep_view(&self) -> Self::V
+2. (in impl Clone for Term) fn clone(&self) -> (res: Self)
+3. (in impl PartialEq for Term) fn eq(&self, other: &Self) -> (res: bool)
+4. pub open spec fn spec_complete_subst(self, s: SpecSubst) -> bool
+5. pub open spec fn spec_concrete(self) -> bool
+6. pub open spec fn spec_subst(self, s: SpecSubst) -> (res: SpecTerm)
+7. pub fn term_eq(&self, other: &Self) -> (res: bool)
+8. pub fn complete_subst(self, s: &Subst) -> (res: bool)
+9. pub fn concrete(self) -> (res: bool)
+10. pub fn subst(self, s: &Subst) -> (res: Term)


I am not sure that documentation like this makes sense in the README. It's a copy of the code, and the code itself is a more authoritative description of the types and methods. We can also auto-generate API descriptions using the documentation generators from Rust and Verus.

What we need at this level is a concise conceptual description of what the datatypes are and the role they play. That is, the higher-level thought process that you can't see directly in the code itself.

This same comment applies to all the sections under Data types of Kernel.

Agreed---we don't need this list of function signatures. Instead, it would be good to have some description of what each data type represents in the kernel, similar to what you have in Prop. For example, for Term, you could say that it represents the Datalog notion of a term, i.e., the arguments to a Datalog atom.

mmcloughlin · 2024-08-01T19:35:54Z

verus/lcf/README.md

+
+## Rule
+
+Rules are the equivalent to rules in Datalog. A Rule in the kernel with no body is equivalent to a fact in Datalog. In this datalog line of code: connected(a, b) :- edge(a, b). ---- connected(a, b) :- edge(a, b) is a Rule that is also a rule in Datalog. In this datalog line of code: edge("x", "y"). ---- edge("x", "y"). is a Rule that is a fact in Datalog because it only has a head and no body.


Have you looked at the rendered markdown? I suspect paragraphs like these will not come out right. You need to wrap things in code markers as appropriate.

mmcloughlin · 2024-08-01T19:36:28Z

verus/lcf/README.md

+
+## Purpose 
+
+The purpose of this verified kernel is to encode a RuleSet corresponding to a set of Datalog rules and encode a set of facts( rules without bodies) in order to solve Datalog predicates. The major goal of this kernel is to one day encode a set of rules of criteria for verifiable X.509 web certificate fields and sets of facts corresponding to the fields' values in order to produce a theorem if the proof tree corresponding to these rules and facts is valid. 


Please wrap paragraphs to a reasonable line width.

mmcloughlin · 2024-08-01T19:37:39Z

verus/lcf/README.md

@@ -0,0 +1,396 @@
+## Verified Kernel in Dafny


Generally in this document, I think it makes sense to remove documentation that's just a copy of the code itself. Please keep it to a description of the high-level concepts that aid the understanding of the code.

mmcloughlin · 2024-08-01T19:42:34Z

verus/lcf/src/verusport.rs

+impl DeepView for Const {
+    type V = SpecConst;
+
+    // function deep_view allows for reasoning about spec-level data structures and types while in exec mode


I'd also suggest avoiding comments like this. Verus developers should know what deep_view is. It's the job of Verus documentation to explain that, not your code.

mmcloughlin · 2024-08-01T19:43:32Z

verus/lcf/src/verusport.rs

+}
+
+impl Term {
+    // function proves equality for Term types


I'd avoid prefixing your comments with function .... Just say // Check equality for terms.

mmcloughlin · 2024-08-01T19:46:58Z

verus/lcf/src/verusport.rs

+    {
+        match self {
+            SpecProp::App(h, args) => {
+                //map_values calls spec_subst on all SpecTerm items in args and stores in new sequence


Best to avoid verbatim descriptions of the code. Prefer something like // Apply substitution to arguments, or avoid it altogether since it's quite simple.

mmcloughlin · 2024-08-01T19:50:57Z

verus/lcf/src/verusport.rs

+
+    //spec function checks whether valid SpecProp types are concrete and are equal
+    pub open spec fn spec_valid(self) -> bool {
+        if self.spec_symbolic() == true || self.spec_concrete() == false {


You can avoid comparisons with booleans.

x == true can just be x and x == false is !x.

mmcloughlin · 2024-08-01T19:51:53Z

verus/lcf/src/verusport.rs

+    }
+    //if all properties were satisfied
+
+    if flag == true {


Maybe do if !flag { return Err(()) } and then the rest of the code can be indented one less.

pratapsingh1729

Overall, this is great work! It's really exciting that you have been able to port the kernel over to Verus. I've left a few comments, mostly stylistic/to do with comments and text descriptions in your code. I also noted some TODO items that I think are worth addressing at some point, but I think we can merge this before those are done.

pratapsingh1729 · 2024-08-01T19:57:24Z

verus/lcf/README.md

+Term types are enums that have 2 variants:
+1. Const(Const)
+2. Var(String)
+
+Its spec versions for SpecTerm are:
+1. Const(SpecConst)
+2. Var(Seq<char>)
+
+Functions that can be used on Term types:
+1. (in impl DeepView for Term) open spec fn deep_view(&self) -> Self::V
+2. (in impl Clone for Term) fn clone(&self) -> (res: Self)
+3. (in impl PartialEq for Term) fn eq(&self, other: &Self) -> (res: bool)
+4. pub open spec fn spec_complete_subst(self, s: SpecSubst) -> bool
+5. pub open spec fn spec_concrete(self) -> bool
+6. pub open spec fn spec_subst(self, s: SpecSubst) -> (res: SpecTerm)
+7. pub fn term_eq(&self, other: &Self) -> (res: bool)
+8. pub fn complete_subst(self, s: &Subst) -> (res: bool)
+9. pub fn concrete(self) -> (res: bool)
+10. pub fn subst(self, s: &Subst) -> (res: Term)


Agreed---we don't need this list of function signatures. Instead, it would be good to have some description of what each data type represents in the kernel, similar to what you have in Prop. For example, for Term, you could say that it represents the Datalog notion of a term, i.e., the arguments to a Datalog atom.

pratapsingh1729 · 2024-08-01T20:01:37Z

verus/lcf/README.md

+
+## Prop
+
+Props are the heads of rules that are used in rulesets for mk_thm.


Note that Props don't just appear in rule heads, they are also the bodies of rules---they correspond to the Datalog notion of an "atom" or "predicate".

pratapsingh1729 · 2024-08-01T20:04:53Z

verus/lcf/README.md

+## Prop
+
+Props are the heads of rules that are used in rulesets for mk_thm.
+In this datalog line of code: connected(a, b) :- edge(a, b). ---- connected(a, b) is the Prop


edge(a,b) would also be represented with a Prop here

pratapsingh1729 · 2024-08-01T20:06:07Z

verus/lcf/README.md

+
+## Ruleset
+
+A RuleSet is a set of Rules in our kernel. 


I would add that we use RuleSet to encompass all of the rules from the Datalog program that we start with, and relate it to valid for Proof.

pratapsingh1729 · 2024-08-01T20:08:14Z

verus/lcf/README.md

+
+
+## Thm
+Theorems (thm) are used in our kernel as the final result that we are producing and want to run Ok on. If the theorem is valid, Ok will be returned, and if it is invalid, Err will be returned.


Not sure what you mean by "run Ok on" here. The Ok is a constructor from the Result type, which is used in mk_thm to tell us whether we successfully constructed a Thm or not. The key thing about Thm is that if it is well-formed, then we know that there exists a valid proof tree for the atom denoted by val.

pratapsingh1729 · 2024-08-01T20:40:00Z

verus/lcf/src/kernel.rs

+                ;
+                Prop::App(h.clone(), v)
+            },
+            Prop::Eq(x, y) => Prop::Eq(x.clone().subst(s), y.clone().subst(s)),


Are the clone calls here required?

pratapsingh1729 · 2024-08-01T20:40:23Z

verus/lcf/src/kernel.rs

+        proof {
+            assert_seqs_equal!(v.deep_view(), self.body.deep_view().map_values(|p: SpecProp| p.spec_subst(s.deep_view())));
+        }
+        ;


Remove this semicolon

pratapsingh1729 · 2024-08-01T20:40:44Z

verus/lcf/src/kernel.rs

+    {
+        let mut v = Vec::<Prop>::new();
+        //assertion uses forall statement to show the two positions of deep_view are the same result
+        assert(forall|k: int|


Again, this assertion could be factored into a lemma. For now, a comment would be helpful.

pratapsingh1729 · 2024-08-01T20:42:12Z

verus/lcf/src/kernel.rs

+    closed spec fn deep_view(&self) -> Self::V;
+}
+
+//#[verifier::external_body] needed due to postocondition failing


I would note here that we add this axiom because of an issue with Verus: verus-lang/verus#1222

That way, if/when that issue is resolved, someone reading this code can corroborate and work on replacing the axiom with an actual definition.

pratapsingh1729 · 2024-08-01T20:45:17Z

verus/lcf/src/kernel.rs

+        forall|j: int| #![auto] 0 <= j < args.len() ==> args[j].deep_view().spec_wf(rs.deep_view()),
+    ensures
+//ensures block specifies conditions that must be met in order for the thm to be valid at termination
+


These conditions are a little complicated---it would be nice to have a plain-language, high-level description of what they mean. For instance, the first one says that if we provide "reasonable" arguments (the substitution is complete for the rule in question, we have the right number of proofs for the arguments, and those proofs prove the atoms in the body of the rule), then mk_thm will produce a valid Thm for that Prop.

pratapsingh1729

Overall, this is great work! It's really exciting that you have been able to port the kernel over to Verus. I've left a few comments, mostly stylistic/to do with comments and text descriptions in your code. I also noted some TODO items that I think are worth addressing at some point, but I think we can merge this before those are done.

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

comment out old trace reconstruction code

ab9c4b6

Start verusport branch

6e69b8a

import string_hash_map axiomatization

86dc91c

working on deep_view issue

636e1d6

Merge branch 'verusport' into verus-string-hash-map

bf21110

Merge pull request #1 from eobardthawne21p/verus-string-hash-map

5598631

import string_hash_map axiomatization

utilizing StringHashMap and showing it works

8de1ff2

Added a couple of functions in impl Term

435a440

created impl for Const with clone

eaca976

saved file then pushed

03af4ad

finished prop impl

00584a1

symbloic verifies and working on valid

9144ac3

fixed first version of valid

7887faf

Changed Rule enum to struct and did match exercise for valid()

adc8350

added complete_subst and concrete fns for Rule impl

4444aa9

finished Rule impl

405f8ee

added enum for Proof

737d128

found issue with cloning vector

a600652

working on contains fn for RuleSet

750f1d7

implemented PartialEq for StringHashmap

7bda8f4

Cleaned up code and added additional cases for PartialEq match

5f0c800

Merged redundant if statements

eedf6ce

add deep views

c11f999

Merge pull request #2 from eobardthawne21p/pratap-deepviews

23f4f27

add deep views

merged Pratap's changes

9c89ca6

fixed code on my branch

14b6fc8

fixed

3b514eb

created playground and attempting to do spec stuff

d71dd16

added specterm fix

f8d256f

Merge branch 'verusport' of https://github.com/eobardthawne21p/veri-d…

885ee17

…atalog into verusport

eobardthawne21p added 8 commits August 1, 2024 00:51

added tst_connected_thm

cbae708

test

caeade3

ran verusfmt on code

b27c932

added Const and Subst

cc0af36

added Term

54273fc

added Prop

475ab79

added Rule

172e4f6

finished project

75fc185

pratapsingh1729 assigned pratapsingh1729 and mmcloughlin and unassigned mmcloughlin and pratapsingh1729 Aug 1, 2024

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

eobardthawne21p added 4 commits August 1, 2024 11:08

fixed error

d0ab2ad

fixed error

f9d40f3

fixed error

19d6931

got last example to verify

c9f90a8

mmcloughlin reviewed Aug 1, 2024

View reviewed changes

eobardthawne21p added 2 commits August 1, 2024 16:27

fixed kernel

cd1c9c2

fixed README

3154f67

eobardthawne21p requested a review from mmcloughlin August 1, 2024 20:41

pratapsingh1729 reviewed Aug 1, 2024

View reviewed changes

pratapsingh1729 self-requested a review August 1, 2024 20:47

pratapsingh1729 reviewed Aug 1, 2024

View reviewed changes

eobardthawne21p added 3 commits August 2, 2024 09:05

fixed headers

bf301bc

removed redundant code from README

7f3650c

fixed more changes from comments on PR

6a1dba2

mmcloughlin changed the base branch from mbm/x-trace-reconstruction to trace-reconstruction August 2, 2024 15:15

pratapsingh1729 merged commit 4322b16 into secure-foundations:trace-reconstruction Aug 2, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Verusport #3

Verusport #3

eobardthawne21p commented Aug 1, 2024 •

edited

Loading

mmcloughlin Aug 1, 2024

pratapsingh1729 Aug 1, 2024

mmcloughlin Aug 1, 2024

mmcloughlin Aug 1, 2024

mmcloughlin Aug 1, 2024

mmcloughlin Aug 1, 2024

mmcloughlin Aug 1, 2024

mmcloughlin Aug 1, 2024

mmcloughlin Aug 1, 2024

mmcloughlin Aug 1, 2024

pratapsingh1729 left a comment

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

pratapsingh1729 Aug 1, 2024

pratapsingh1729 left a comment


		## Rule

		Rules are the equivalent to rules in Datalog. A Rule in the kernel with no body is equivalent to a fact in Datalog. In this datalog line of code: connected(a, b) :- edge(a, b). ---- connected(a, b) :- edge(a, b) is a Rule that is also a rule in Datalog. In this datalog line of code: edge("x", "y"). ---- edge("x", "y"). is a Rule that is a fact in Datalog because it only has a head and no body.


		## Purpose

		The purpose of this verified kernel is to encode a RuleSet corresponding to a set of Datalog rules and encode a set of facts( rules without bodies) in order to solve Datalog predicates. The major goal of this kernel is to one day encode a set of rules of criteria for verifiable X.509 web certificate fields and sets of facts corresponding to the fields' values in order to produce a theorem if the proof tree corresponding to these rules and facts is valid.


		## Prop

		Props are the heads of rules that are used in rulesets for mk_thm.



		## Thm
		Theorems (thm) are used in our kernel as the final result that we are producing and want to run Ok on. If the theorem is valid, Ok will be returned, and if it is invalid, Err will be returned.

Verusport #3

Verusport #3

Conversation

eobardthawne21p commented Aug 1, 2024 • edited Loading

Updates to codebase:

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

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

eobardthawne21p commented Aug 1, 2024 •

edited

Loading