Limited functions #54

ole-thoeb · 2024-10-23T14:39:32Z

This PR implements limited functions from the paper "Computing with an SMT Solver".
If enabled, the transformation is only applied to functions that have a direct definition, i.e. of the form func func_name(<args>): <returnType> = <def>.

Three new command line options have been added

--limited-functions implicitly adds a fuel parameter to all applicable functions and restricts the defining axiom accordingly.
--force-ematching forces e-matching by disabling mbqi. Otherwise the different encoding has no effect.
--lit-wrap adds a Lit marker around constant values and a version of the defining axiom for constant values, that does not consume any fuel.

Open TODOs and questions

Varaius open TODOs / questions in the code
Testing - How to check for fast rejection?
Lit-wrapping is not propagated (Lit(1) + Lit(2) -> Lit(1 + 2) or Fac(Lit(3)) -> Lit(Fac(Lit(3)))). I don't have a good idea here.
SmtVcUnit::simplify removes Lit wrapper from the verification condition. Hence, --no-simplify is currently also needed.
Need to investigate why coupon-collector.heyvl no longer verifies with everything new disabled - .\tests/coupon-collector.heyvl::inner_loop: Unknown result! (reason: (incomplete (theory array)))
- ~~The generated SMT-lib code is now identical (except for patterns, but removing them does also not change the following fact) but z3 does no longer terminate~~
- Going back to explicitly enumerating all quantified variables when generating SMT-lib code solves the problem

Philipp15b

Thanks for your PR! I've left mostly documentation- and cosmetic-related comments. We can discuss the theoretical questions in our next meeting.

Philipp15b · 2024-10-24T08:42:07Z

src/opt/fuzz_test.rs

@@ -198,7 +198,7 @@ fn prove_equiv(expr: Expr, optimized: Expr, tcx: &TyCtx) -> TestCaseResult {
        optimized.clone(),
    );
    let ctx = z3::Context::new(&z3::Config::new());
-    let smt_ctx = SmtCtx::new(&ctx, tcx);
+    let smt_ctx = SmtCtx::new(&ctx, tcx, false, false);


These additional parameters are rather mysterious here. I suggest just adding a new type like SmtCtxOptionsto capture those options.

Philipp15b · 2024-10-24T08:43:12Z

src/smt/mod.rs

-                        .map(|param| ty_to_sort(self, &param.ty))
-                        .collect();
+
+                    let mut domain = if self.is_limited_function_decl(&func) {


Maybe capture this functionality in some method somewhere else in a section/module of code specifically for the fuel transformation?

Philipp15b · 2024-10-24T08:43:35Z

src/smt/mod.rs

+                            translate.pop();
+                        }
+
+                        let mut add_defining_axiom = |name: Ident, lhs: &Expr, rhs: &Expr| {


Same here, maybe capture this in another method?

Philipp15b · 2024-10-24T08:44:21Z

src/smt/mod.rs

+                            // Defining axiom
+                            add_defining_axiom(func.name, &app, body); // TODO: create a new name for the axiom
+
+                            // Computing axiom


Also here, capture in another method. And please add comments showing roughly what the generated axiom(s) look like.

Philipp15b · 2024-10-24T08:45:39Z

src/smt/mod.rs

@@ -204,3 +299,36 @@ fn ty_to_sort<'ctx>(ctx: &SmtCtx<'ctx>, ty: &TyKind) -> Sort<'ctx> {
        }
    }
 }
+
+pub enum Lit<'ctx> {


Maybe add a comment how this wraps z3rro's Lit type? And also explain what this is and why it's needed.

Philipp15b · 2024-10-24T08:47:09Z

src/smt/translate_exprs.rs

@@ -175,18 +207,24 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
                panic!("illegal cast to {:?} from {:?}", &expr.ty, &operand.ty)
            }
            ExprKind::Quant(quant_op, quant_vars, ann, operand) => {
+                self.push(); // avoid leaking any fresh quant_vars into the outside scope


Why is this now needed? Why wasn't this an issue before?

I relied heavily on the functionality of the SmtScope for creating fresh quantified variables (creating the quantified fuel on demand). The quantifier translation does actually not use this feature. Instead, a scope with all quantified variables is manually created. The problem is that mk_scope calls get_local which calls init_local if the variable is new (this is always the case for mk_scope) and init_local automatically adds the new variable to the current scope. Therefore, we have the variables twice. Once in the current scope and once in the scope created by mk_scope.

This is my easy "fix". Maybe this is actually a problem with mk_scope or with my understanding of the translation code.

The explanation does make some sense to me. But I just do not understand why this issue wouldn't have shown up before already. Wouldn't any call to mk_scope always create the same variables on the outer quantifier as well?

Could you maybe create a quick example HeyVL file with (nested?) quantifiers where this problem does/does not show up in the SMT output?

Also if this change is correct, definitely don't forget the case for t_eureal :)

Nested quantifiers in heyvl are not a problem since they are created with mk_scope and the variables are fixed. The problem only occurs if the capturing of fresh variables and mk_scope is used together. This was previously not the case as the axioms were first build as heyvl expressions and then translated.

Regarding the fix: I'm not super happy and we might need to talk about it. I think it is not conceptually sound and there are theoretically situations where the fuel translation fails here. For example, if the fuel parameter is first needed inside a heyvl quantifier, the fuel variable is created and added to the current "dummy scope", which is then dropped after the quantifier translation. This can't happen currently since we always translate the function application (lhs) first which needs the fuel variable.

Philipp15b · 2024-10-24T08:49:47Z

src/smt/translate_exprs.rs

        };
        self.locals.insert(ident, local);
    }

+    fn get_maybe_const_local(&mut self, ident: Ident) -> Symbolic<'ctx> {


I'm very unsure what this method does or why it's needed?

Philipp15b · 2024-10-24T08:50:47Z

src/smt/translate_exprs.rs

+    }
+}
+
+#[derive(Default)]


Add a comment saying that this is a lazily initialized fuel's ScopeSymbolic. Explain where it is initialized and when not.

Philipp15b · 2024-10-24T08:53:16Z

z3rro/src/lit.rs

+    func: FuncDef<'ctx>,
+}
+
+/// Identity function that is used to mark constants values. They allow for axioms instantiation


Add this comment on the struct, not on the impl. Say that it is parameterized over the Z3 Sort of the literal.

Philipp15b · 2024-10-24T08:55:57Z

z3rro/src/prover.rs

+    pub fn enforce_ematching(&mut self) {
+        let mut params = Params::new(self.solver.get_context());
+        params.set_bool("auto-config", false);
+        params.set_bool("smt.mbqi", false);


Maybe also add this to the Rustdoc documentation of the Fuel type or somewhere that preventing instantiations by the SMT solver of the fuel type is necessary and that disabling MBQI accomplishes that.

ole-thoeb · 2024-11-04T17:34:26Z

Thanks for the feedback! I think I address most of it. Regarding the Lit-wrapping and computation axiom: I'am unhappy with the current (unfinished) approach and will look into alternatives.

Philipp15b · 2024-12-18T14:13:20Z

src/smt/translate_exprs.rs

@@ -98,8 +98,13 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
        &mut self.fuel_context
    }

-    pub fn add_constant_exprs(&mut self, constant_vars: &[Ident], expr_to_analyse: &mut Expr) {
-        let mut collector = ConstantExprCollector::new(constant_vars);
+    pub fn add_constant_exprs(


As discussed, I think the proper phrase would be "literal" instead of constant. And this function needs a comment explaining why it exists.

Previously, the limited functions had no effect, since z3 made up fuel parameters. Forcing z3 to only use ematching (by disabling mbqi) has the desired effect of forcing it to fail fast.

…ameter

- Added command line options for generating limited-functions and enforcing ematching. - Fix some bugs regarding nested quantifiers

The SMT-lib output (without any extra flags) is now the same as previously (main) except that the definitional axiom has a patter

Reverts back to explicitly enumerate the quantified variables through `mk_scope`. Therefor, the need for the `push()` and `pop()` operations is no longer necessary. Now also correctly encodes calls of limited functions in user defined axioms.

This allows approach allows us to limit user defined with triggers in a sensible way

calls to limited function outside the generated axioms are always translated with a fixed fuel value (i.e. call context). Also remove a non-working examples from the tests.

- the trigger for the computation axiom was wrong - lit wrapping was not always applied properly - define lit functions as uninterpreted functions + axiom to avoid them being removed during preprocessing

Some tests where failing after constructing foralls differently

A function call is now only consider to be constant if - all arguments are constant - if the function has a definition <-- new

The ability to lit wrap is now a trait that a datatype must implement. This enables different specialisations per datatype. The main motivation is to avoid boxing the pair EUReal representation into a single value before passing it into the lit function. The bool and real are now wrapped separately.

…llector

This should avoid triggering the z3 incremental solver

This reverts commit 669d70c.

Parameters set with `Solver::set_params` get ignored without a `Solver::push`

In the process the fuel encoding code was completely restructured

Philipp15b requested changes Oct 24, 2024

View reviewed changes

ole-thoeb force-pushed the limited branch from df0be38 to 71a19ac Compare November 5, 2024 19:04

ole-thoeb marked this pull request as ready for review December 10, 2024 11:18

ole-thoeb requested a review from Philipp15b December 10, 2024 11:18

Philipp15b reviewed Dec 18, 2024

View reviewed changes

ole-thoeb force-pushed the limited branch from 56ff058 to 78e781a Compare December 23, 2024 19:23

ole-thoeb and others added 23 commits January 3, 2025 18:29

ignore .idea

6a0eb63

generation working?

86636f0

stop z3 from being too smart.

edea5f6

Previously, the limited functions had no effect, since z3 made up fuel parameters. Forcing z3 to only use ematching (by disabling mbqi) has the desired effect of forcing it to fail fast.

Always add the "fuel synonym axiom" for function that have a fuel par…

f32b61f

…ameter

Cleanup fuel code

694edfd

- Added command line options for generating limited-functions and enforcing ematching. - Fix some bugs regarding nested quantifiers

Use OnceCell<T> over RefCell<Option<T>> for lazy initialisation

e049f54

Lit-wrap constants without propagation

722f145

rustfmt

180403d

clippy

ac29f5a

bundle flags for SmtCtx in SmtCtxOptions struct

fc14dca

Address most of the PR feedback

40cb672

propagate const information and cleanup axiom generation

ea7b6c9

Correctly construct SmtCtx in test

5ea3ba3

Change quantifier translation a bit, again

0858fa1

The SMT-lib output (without any extra flags) is now the same as previously (main) except that the definitional axiom has a patter

update/improve comments

710cdb8

All caps TODO breaks test runner??!

fe24531

Fix run command

79a853f

don't try to compile example type given in docs

1df7670

Make rust type provided for intuition actually compile

63bfd4e

Ensure new types/function can not clash with user defined code

9bed56d

Only encode non-zero fuel condition in trigger

6ec2096

This allows approach allows us to limit user defined with triggers in a sensible way

More examples

09dc2c3

ole-thoeb added 13 commits January 3, 2025 18:29

Closely mimic encoding from paper

9b701c6

Revert back to the Dafny way of fuel.

d0e7b15

calls to limited function outside the generated axioms are always translated with a fixed fuel value (i.e. call context). Also remove a non-working examples from the tests.

Fix lit wrapping

e807772

- the trigger for the computation axiom was wrong - lit wrapping was not always applied properly - define lit functions as uninterpreted functions + axiom to avoid them being removed during preprocessing

Add quantifier ids and weight to foralls

0c16039

Adjust integration tests

6f8b365

Some tests where failing after constructing foralls differently

rust fmt

4a82860

Consider less function calls as constant

0a53472

A function call is now only consider to be constant if - all arguments are constant - if the function has a definition <-- new

Make test less flaky by adding @trigger

1f0fe09

Fixes after rebasing

fc6d452

Rename ConstantExpr... to LiteralExpr... and use builder style for co…

8ba5a71

…llector

Add tracing to literal value collecting

631b728

Do not lit-wrap if we can not profit from it

f944bea

ole-thoeb force-pushed the limited branch from a915cc1 to f944bea Compare January 3, 2025 18:15

ole-thoeb added 6 commits January 9, 2025 18:30

clone prover when slicing instead of using push/pop

971fdfd

This should avoid triggering the z3 incremental solver

Fighting in vain with z3 params

669d70c

Revert "Fighting in vain with z3 params"

5b8fdaa

This reverts commit 669d70c.

set parameters via set_global_param

de430c5

Parameters set with `Solver::set_params` get ignored without a `Solver::push`

Removed superfluous parameter setting

932eedb

Add plain version of fuel, not using datatype

68c1680

ole-thoeb force-pushed the limited branch from ca9b5a4 to a85d589 Compare February 10, 2025 15:15

Add --static-fuel flag

5ffd375

In the process the fuel encoding code was completely restructured

ole-thoeb force-pushed the limited branch from a85d589 to 5ffd375 Compare February 10, 2025 15:58

ole-thoeb added 2 commits February 11, 2025 17:24

Also generate computation axioms for static fuel

0d7232e

Rename different encodings and consolidate fuel encodings

d3ed935

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Limited functions #54

Limited functions #54

ole-thoeb commented Oct 23, 2024 •

edited

Loading

Philipp15b left a comment

Philipp15b Oct 24, 2024

Philipp15b Oct 24, 2024

Philipp15b Oct 24, 2024

Philipp15b Oct 24, 2024

Philipp15b Oct 24, 2024

Philipp15b Oct 24, 2024

ole-thoeb Nov 4, 2024 •

edited

Loading

Philipp15b Nov 4, 2024

ole-thoeb Nov 4, 2024 •

edited

Loading

Philipp15b Oct 24, 2024

Philipp15b Oct 24, 2024

Philipp15b Oct 24, 2024

Philipp15b Oct 24, 2024

ole-thoeb commented Nov 4, 2024

Philipp15b Dec 18, 2024

Limited functions #54

Are you sure you want to change the base?

Limited functions #54

Conversation

ole-thoeb commented Oct 23, 2024 • edited Loading

Philipp15b 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

ole-thoeb Nov 4, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ole-thoeb Nov 4, 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

ole-thoeb commented Nov 4, 2024

Choose a reason for hiding this comment

ole-thoeb commented Oct 23, 2024 •

edited

Loading

ole-thoeb Nov 4, 2024 •

edited

Loading

ole-thoeb Nov 4, 2024 •

edited

Loading