Translate literal bytes to Coma

[niooss-ledger]

Creusot failed to analyze Rust programs using literal bytes as they were not translated in the generated Coma files. Introduce a new Coma function of_seq in Slice modules to enable crafting a pure WhyML term with the contents of the literal bytes.

Use this new Coma function Slice.of_seq to translate arrays as well.

This Pull Request follows a discussion in issue #2161 where several approaches were suggested. It adds a function and an axiom (which is hopefully sound) to the prelue:

function of_seq (s : seq 'a) : slice 'a
axiom of_seq_elts : forall s : seq 'a [(of_seq s).elts] . UInt$bits_count$.in_bounds (Seq.length s) -> (of_seq s).elts = s

There is observable drawback: some tests now fail with timeouts. On my host, I observed that should_succeed/slices/03_std times out after the first commit (which only introduces of_seq and the translation of literal bytes, not modifying anything else). More precisely, using only the prelude changes from the latest commit in branch master fails:

# Create a new branch from master
git checkout b51999c4c950de375064c0bd8a22a1fbbcc2c868 -b test-with-slice-of_seq
# Patch the Coma prelude
patch -Np1 -i prelude-of_seq.patch
# Run the test
cargo test --test why3 -- should_succeed/slices/03_std 

With prelude-of_seq.patch containing:

diff --git a/prelude-generator/slice.in.coma b/prelude-generator/slice.in.coma
index 11538425dd64..3006864e9c2a 100644
--- a/prelude-generator/slice.in.coma
+++ b/prelude-generator/slice.in.coma
@@ -14,6 +14,9 @@ module Slice$bits_count$
 
   function view (s : slice 'a) : seq 'a = s.elts
 
+  function of_seq (s : seq 'a) : slice 'a
+  axiom of_seq_elts : forall s : seq 'a [(of_seq s).elts] . UInt$bits_count$.in_bounds (Seq.length s) -> (of_seq s).elts = s
+
   function length (s : slice 'a) : UInt$bits_count$.t
   axiom length_spec : forall s : slice 'a . (UInt$bits_count$.t'int (length s)) = Seq.length s.elts
 
@@ -55,6 +58,9 @@ module Slice$bits_count$BW
 
   function view (s : slice 'a) : seq 'a = s.elts
 
+  function of_seq (s : seq 'a) : slice 'a
+  axiom of_seq_elts : forall s : seq 'a [(of_seq s).elts] . UInt$bits_count$BW.in_bounds (Seq.length s) -> (of_seq s).elts = s
+
   function length (s : slice 'a) : UInt$bits_count$BW.t
   axiom length_spec : forall s : slice 'a . (UInt$bits_count$BW.t'int (length s)) = Seq.length s.elts
 

... The test fails:

$ cargo test --test why3 -- should_succeed/slices/03_std
    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.06s
     Running tests/why3.rs (target/debug/deps/why3-43308a50ef290ce7)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.06s
     Running `target/debug/prelude-generator`
Building prelude...
Testing tests/should_succeed/slices/03_std.coma ... failure
******** STDOUT ********
Goal M_check_iter.vc_check_iter: ✘ (22/26)
Theory 03_std.M_check_iter: ✘ (29/33)
Theory 03_std.M_check_iter_as_slice: ✔ (4)
Theory 03_std.M_check_iter_mut: ✔ (24)
Theory 03_std.M_check_iter_mut_as_slice: ✔ (5)
******** STDERR ********
Error: 1 unproved file
************************
Failure!
error: test failed, to rerun pass `-p why3tests --test why3`

Caused by:
  process didn't exit successfully: `/creusot/target/debug/deps/why3-43308a50ef290ce7 should_succeed/slices/03_std` (exit status: 1)

Adding --time 5 (to the cargo test command) fixes the test, and tests/should_succeed/slices/03_std/proof.json shows that Z3 takes 10 times more time to achieve a proof:

               {
                 "tactic": "split_vc",
-                "children": [ { "prover": "z3", "time": 0.38 } ]
+                "children": [ { "prover": "z3", "time": 3.8 } ]
               },

This happens in the test check_iter in

creusot/tests/should_succeed/slices/03_std.rs

Lines 17 to 18 in b51999c

	let a = iter.next_back().unwrap();
	proof_assert!(a@ == 4);

So there is currently a strong performance regression caused by the introduction of function of_seq and axiom of_seq_elts, even when not using the function. This regression becomes all the more visible with the second commit of this Pull Request, which modifies how Rust arrays are translated: this makes more tests time out.

Fixes: #2161

[niooss-ledger]

I asked Claude Code (model Sonnet 4.6) to take a look and it emitted a very reasonable diagnostic:

Root cause: Declaring of_seq as a logical function with an axiom caused Why3 to generate a hidden universally-quantified type invariant axiom — ∀ s. in_bounds(Seq.length (of_seq s).elts). Combined with the user's of_seq_elts axiom using trigger [(of_seq s).elts], this fed Z3 an (of_seq X).elts term for every sequence constant in the proof context. The check_iter test has many sequence constants (6-element iterator, 7 assertions), causing O(n) axiom instantiations and 10× slowdown on the hardest subgoal (0.38s → 3.8s).

At first, I had trouble with this explanation, as I was believing that function of_seq (s : seq 'a) : slice 'a was "only" defined on sequences s such that UInt$bits_count$.in_bounds (Seq.length s). Then, I understood this notation actually means something else, in Why3:

• Calling of_seq s with a sequence s is guaranteed to always return a valid slice.
• This slice has .elts = s only when the length is within-bounds (which is what axiom of_seq_elts is about). Otherwise, the result of of_seq s may be unrelated to s.

Therefore Why3 generates a type-invariant axiom ∀ s. in_bounds(Seq.length (of_seq s).elts), which triggers the trigger of axiom of_seq_elts. This could create (to be confirmed) some expressions for each sequence s appearing in Coma files, such as: in_bounds (Seq.length s) -> in_bounds(Seq.length (of_seq (of_seq s).elts).elts), leading to a visible performance regression.

I am therefore now looking into ways to define a pure function (function of_seq (s : seq 'a) : slice 'a) over a domain restricted by a pre-condition (s: seq such that UInt$bits_count$.in_bounds (Seq.length s)), if doing so is possible in Why3.

Btw, it would be much simpler if Coma/WhyML had a way to instantiate record types with invariant, as the condition here is very simple to prove (it is "some length constant is below the MAX of Uint$bits_count$"), but I guess there is a reason why this is impossible.

[jhjourdan]

caused Why3 to generate a hidden universally-quantified type invariant axiom — ∀ s. in_bounds(Seq.length (of_seq s).elts)

That is wrong. Why3 generates once and for all an axiom ∀ s: slice. in_bounds(Seq.length s.elts) for an abstract type slice. Thus, I don't think the matching loop you are referring to exists actually.

Instead, I think the problem is that sequenc literals in Why3 are translated with a combination of Seq.create and a cascade of ifs, which the SMT solvers are a bit afraid of unfolding. That combined with the need to use extensionality of equality of sequences kills the provers....

The core of the problem is that support of sequences in Why3 is not very good. At some point I thought it was because Why3 is not using native SMTLib support of sequences, but then I tried to port Why3 sequences to SMTLib, and a whole lot of proofs broke in the test suite of Why3...

What should we do ? Perhaps we could find a better encoding of sequence literals in Why3, based on axioms like those we were adding before this PR???

[jhjourdan]

Btw, it would be much simpler if Coma/WhyML had a way to instantiate record types with invariant, as the condition here is very simple to prove (it is "some length constant is below the MAX of Uint$bits_count$"), but I guess there is a reason why this is impossible.

Essentially, such a syntax would be encoded just like of_seq. The logic of Why3 tries to avoid partial constructions, letting the user introduce them manually if she really wants them. We are exactly in this case.