Groebner extension #53

yizhou7 · 2022-02-08T00:22:24Z

No description provided.

cases

a special exception on the `inout` branch for the "_default" module vs. the original master code, due to the presence of rank_is_less_than. Rustan then made the original logic more complex in support of "Revise export reference types", commit 3a9524f.

the linear pass more complete

when naming functor applications. Should be safe, in theory. Closes #49

compiled. Closes #51

resolved argument names when naming the functor's output

and use it in both the Compiler, and when the Resolver checks for duplicate compile names. Closes #52.

parno

Do all of those examples go through? If so, that's really cool! I'm also impressed you could whip this together so quickly!

parno · 2022-02-08T03:04:50Z

Source/Dafny/Translator.cs

+    }
+
+    string OpacifySubExpr(Expression expr) {
+      if (expr is SeqSelectExpr) {


C# will let you write:

if (expr is SeqSelectExpr seqSelExpr) { ...

i.e., you can combine the test with the naming of the new variable. The name scoping is annoying though, each new variable needs to be unique, so you can't just call them all e, for example.

Ah that's good to know. Thanks for the tip!

parno · 2022-02-08T03:05:53Z

Source/Dafny/Translator.cs

+        }
+        var seq = this.OpacifySubExpr(seqSelExpr.Seq);
+        var index = this.OpacifySubExpr(seqSelExpr.E0);
+        return String.Format("{0}[{1}]", seq, index);


It seems like this is going to emit something like x[5] to Singular. Won't that confuse it?

Oh wait, I see. The goal is just to create a unique string 'key' to use later in the opaqueExprs dictionary?

Ah yes, exactly. We create a temp variable in place of the expression, and when the exact same expression shows up again, we will just use the temp variable. Singular will have next to no understanding of the expression, only knowing that it is some integer.

parno · 2022-02-08T03:10:15Z

Source/Dafny/Translator.cs

+        var mod = this.EncodeSubExpr(appplyExpr.Args[2]);
+        // add the mod to the generators
+        polys.Add(mod); 
+        return this.EncodeEqualityPoly(appplyExpr.Args[0], appplyExpr.Args[1]);


Why aren't Args[0] and Args[1] encoded here? They were encoded in EncodeGeneratorPoly.

Oh in this case we are encoding the "question": is it true that Args[0] and Args[1] are congruent modulo Args[2]? So Args[2] goes into the ideal, while Args[0] - Args[1] becomes the query.

Right, but I was expecting something like:

return this.EncodeEqualityPoly(this.EncodeSubExpr(appplyExpr.Args[0]),this.EncodeSubExpr(appplyExpr.Args[1]));

Oh in this case the Args[2] needs to go into the ideal. The rest of the polys in the generators are effectively all 0, except this one. Then if the difference Args[0] - Args[1] can be written in terms of a linear combination of the generators, it must be a multiple of Args[2], proving the congruence.

parno · 2022-02-08T03:10:47Z

Source/Dafny/Translator.cs

+      }
+    }
+
+    string EncodeQueryPoly(Expression expr) {


This looks very similar to EncodeGeneratorPoly. Would it make sense to factor out the common bits?

That is true, I will try extract some common bits.

parno · 2022-02-08T03:11:14Z

Source/Dafny/Translator.cs

+        } else if (ss is AssumeStmt) {
+          this.EncodeGeneratorPoly((ss as AssumeStmt).Expr);
+        } else {
+          Console.WriteLine("Error: Unexpected Grobner poorf body statement {0}", ss);


"proof body"

Good catch. I can't English :)

parno · 2022-02-08T03:15:07Z

Source/Dafny/Translator.cs

+              var assumeFalse = new AssumeStmt(stmt.Tok, stmt.EndTok, falseBody, null);
+              assertStmt.Proof.Body.Add(assumeFalse);
+            }
+            TrStmt(assertStmt.Proof, proofBuilder, locals, etran);


Just to confirm, this is a Dafny level change that adds a Dafny-level "assume false" to the proof body that's supplied in the by { ... } clause of the assert? And it's added at the end of the body, so that Dafny will check the assertions the developer wrote, since Singular trusts that they are correct?

Yes, that is exactly my intention.

It might be worth adding a small comment explaining the overall intent, or even showing a "before" and "after" version of some sample Dafny code.

Good point, will do.

…correctly)

close the `queryFile` for Singular solver. Otherwise there will be IOException error when deleting it on Windows.

[groebner-extension]: close query file after writing

Chris-Hawblitzel and others added 30 commits December 10, 2020 22:26

Add Docs/Linear directory with documentation on the linear type system

040c727

Fix some typos in Docs/Linear/TypingRules.md

4336f32

Minor reformatting in Docs/Linear/TypingRules.md

030cdaa

Minor fixes

0a4c475

Add Docs/Linear/RelatedWork.md

5bb1a8d

Add Rust comparison to Docs/Linear/RelatedWork.md

dfd9eac

Minor fixes to Docs/Linear/RelatedWork.md

12a20d7

Minor formatting fixes to Docs/Linear/RelatedWork.md

ee03518

Minor bug fixes in Resolver/Linear

1e5f9b0

Allow "linear var D() := ...;" to deconstruct empty linear datatype

dab22ed

cases

Add Docs/Linear/Library.md

0b97e53

Add Docs/Linear/Implementation.md

87c291b

Add Docs/Linear/PossibleChanges.md and Docs/Linear/README.md

7e7b8b0

Closes #15

c03692e

Merge branch 'cpp' of github.com:secure-foundations/dafny into cpp

5b3fc6f

Merge branch 'master' into cpp

d3b9911

Remove some outdated notes to simplify comparisons between branches

12992dc

Remove project files that are no longer needed

b5a6a82

This LIMITATIONS file has been absorbed into Docs/Compilation/Cpp.md

78f9a55

Merge branch 'cpp' into inout

d302369

Many fixes to restore everything to a state that compiles

2b74270

Attempt to resolve a lookup in GetTypeOfFunction

157fe9a

Fix a number of failing tests by eliminating bugs and/or making

e375420

the linear pass more complete

Fix another case in Linear.cs

6849c08

Restore a portion of the parser that got lost in the merge

82a06d4

Fix a problem with emitting default values. Addresses 6 test cases

ae81dfb

Fix another bad default to address 4 more test cases

8cb2a75

Remove redundant use of isGhost in favor of usage

1661d73

Import a fix from master commit 5129ec3

279504d

parno and others added 16 commits October 4, 2021 12:45

Restore the ability to import an export set

166da2b

Compute function fuel over virtual modules as well

bd5acc1

Test case for opaque

2150693

Alternate approach to generating compile names. Removes unique counter

a8826da

when naming functor applications. Should be safe, in theory. Closes #49

Don't compile modules that have arguments that are not going to be

d86e8ea

compiled. Closes #51

Part way through revamp of FunctorApplication, so we can use the fully

63a234e

resolved argument names when naming the functor's output

Consolidate the checking of whether something should be compiled,

7302337

and use it in both the Compiler, and when the Resolver checks for duplicate compile names. Closes #52.

parser changes for gbassert

a2de340

a skeleton for SingularDriver in Translator

8793a19

a very basic version

d3f239c

open a subprocess for Singular

bbcc107

cannot get WaitForExit with timeout working for whatever reason

a244118

hardcode timeout in process start

3aab717

handle certain sub expressions as opaque

fc17e5e

use separate files for queries

3960f0b

add some use cases

0b15020

parno approved these changes Feb 8, 2022

View reviewed changes

yizhou7 and others added 13 commits February 8, 2022 14:00

address some comments from @parno

c63e273

fix missing variable

ebb6341

handle more opaque expressions

07cc617

add more support for opaque operations (binop)

4573075

emit null as empty string in opaque

c7e597d

bug fix for OpacifySubExpr (args for function calls were not encoded …

87df8bc

…correctly)

add groebner keyword for lemma call

299f5ab

retain support for gbassert

b402d2a

[groebner-extension]: close query file after writing

410403a

close the `queryFile` for Singular solver. Otherwise there will be IOException error when deleting it on Windows.

Merge pull request #54 from zhenkuny/patch-1

f5e1873

[groebner-extension]: close query file after writing

Merge branch 'betr' into groebner-extension

1adbb8d

fix type errors

c50e9ca

fix seq index access in gbassert

d865d2e

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Groebner extension #53

Groebner extension #53

yizhou7 commented Feb 8, 2022

parno left a comment

parno Feb 8, 2022

yizhou7 Feb 8, 2022

parno Feb 8, 2022

parno Feb 8, 2022

yizhou7 Feb 8, 2022 •

edited

Loading

parno Feb 8, 2022

yizhou7 Feb 8, 2022

parno Feb 8, 2022

yizhou7 Feb 8, 2022

parno Feb 8, 2022

yizhou7 Feb 8, 2022

parno Feb 8, 2022

yizhou7 Feb 8, 2022

parno Feb 8, 2022

yizhou7 Feb 8, 2022

parno Feb 8, 2022

yizhou7 Feb 8, 2022

Groebner extension #53

Are you sure you want to change the base?

Groebner extension #53

Conversation

yizhou7 commented Feb 8, 2022

parno 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

yizhou7 Feb 8, 2022 • 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

yizhou7 Feb 8, 2022 •

edited

Loading