Time reasoning #1275

Pialex99 · 2023-01-06T12:30:20Z

Add time reasoning functionality.

The error reporting is a bit hacky but it works.
Does not work on pure functions and closures.
Quadratic runtime does not work because z3 can't handle it out of the box.

prusti-common/src/vir/optimizations/functions/simplifier.rs

Aurel300 · 2023-01-06T13:22:00Z

prusti-common/src/vir/optimizations/functions/simplifier.rs

+            }) => if b {
+                conjunct


@vakaras If we inline a dummy trigger function body (with the body true) and also simplify, this would change semantics of quantifiers. Do you know in what order the inlining is performed?

Yes, this can be a problem. For this and other reasons, it is better to use domain functions as triggers (with an axiom that says its value is always true).

prusti-common/src/vir/optimizations/functions/simplifier.rs

prusti-common/src/vir/optimizations/methods/simplifier.rs

prusti-common/src/vir/optimizations/predicates/delete_unused_predicates.rs

Aurel300 · 2023-01-06T13:37:34Z

prusti-tests/tests/typecheck/fail/time-resources/condition.rs

+
+use prusti_contracts::*;
+
+// ignore-test: prusti-constract functions used outside specification check not yet implemented


I'm not sure about "not yet" here: we don't want to implement something like this. Many specification functions don't make sense in executable code, and branching on time_credits or receipts is also such an example. I would remove this test.

As they don't make sense in executable code why don't we report them when we find them?

Because nobody has implemented that feature yet...

prusti-common/src/vir/to_viper.rs

prusti-utils/src/config.rs

prusti-viper/src/encoder/errors/error_manager.rs

prusti-viper/src/encoder/mir/pure/specifications/interface.rs

vir/defs/polymorphic/ast/expr.rs

vir/src/legacy/ast/expr.rs

vir/defs/polymorphic/ast/common.rs

prusti-viper/src/encoder/foldunfold/requirements.rs

prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs

prusti-viper/src/encoder/procedure_encoder.rs

prusti-tests/tests/verify/fail/time-resources/array_cmp.rs

Aurel300 · 2023-01-06T14:23:07Z

prusti-tests/tests/verify/fail/time-resources/variable.rs

+
+use prusti_contracts::*;
+
+// ignore-test: prusti-constract functions used outside specification check not yet implemented


Remove this test.

Aurel300 · 2023-01-06T14:24:12Z

prusti-tests/tests/verify/pass/time-resources/array_cmp.rs

+fn safe_array_cmp<T: Eq>(a: &[T], b: &[T]) -> bool {
+  let mut i = 0;
+  let mut res = true;
+  while i < a.len() {


Why don't we need to put time_credits in the invariant?

Prusti didn't complain so I thought I didn't have to and the loop.rs tests were passing without so I thought that it was okay but playing a bit with the generated Viper code showed me that it doesn't 😅

prusti-tests/tests/verify/pass/time-resources/array_cmp.rs

Aurel300 · 2023-01-06T14:26:04Z

prusti-tests/tests/verify/pass/time-resources/flag.rs

+
+use prusti_contracts::*;
+
+// This test checks that setting the time reasoning option to false ignores timing constrains


As written in another comment, I don't think this should be the behaviour. This test also isn't even fully testing what the comment says: there is no timing specification to "ignore", only the default zero permissions.

prusti-tests/tests/verify/pass/time-resources/rec.rs

Implications are brocken with time credits and receipts contraints as they are impure but Prusti translate them into ors which viper doesn't accept. Simplifying those expression solve this issue as they are changed back to an implication.

Aurel300 · 2023-06-26T11:03:56Z

Superseded by #1408.