Request: term_eval and term_eval_unint

[msaaltink]

While looking for a proof, it can be useful to experiment in the REPL. Here, the unfold_term and rewrite functions reflect the actions of unfolding and simplify. For some things, though, like expanding maps, folds, or comprehensions, a proof needs to use goal_eval or goal_eval_unint. There's no analogue of these for terms, but they could be quite useful.

[brianhuffman]

This sounds like a reasonable idea, and it shouldn't be too much work to add.

[brianhuffman]

I now have a draft PR (#927) that partially implements this feature. Here's an example of what it can do:

sawscript> mul <- define "mul" {{ \(x : [8]) (y : [8]) -> pmod (pmult x y) 0b100001011 }}
sawscript> type mul
[17:27:57.120] [8] -> [8] -> [8]
sawscript> term_eval_unint ["mul"] {{ foldr mul 0 [3,5..19] }}
[17:28:29.683] fresh:mul#57 (Prelude.bvNat 8 3)
  (fresh:mul#57 (Prelude.bvNat 8 5)
     (fresh:mul#57 (Prelude.bvNat 8 7)
        (fresh:mul#57 (Prelude.bvNat 8 9)
           (fresh:mul#57 (Prelude.bvNat 8 11)
              (fresh:mul#57 (Prelude.bvNat 8 13)
                 (fresh:mul#57 (Prelude.bvNat 8 15)
                    (fresh:mul#57 (Prelude.bvNat 8 17)
                       (fresh:mul#57 (Prelude.bvNat 8 19)
                          (Prelude.bvNat 8 0)))))))))

Currently it's restricted to evaluating terms with simple, non-function types. If you want to use it on a function, you'll have to generate some arguments with fresh_symbolic and fully apply the term first. (The plan is to make term_eval do that automatically for you, but it will take a bit more work than I wanted to spend at the moment.) If you supply a term with a type it doesn't like, it will fail very ungracefully.

Anyway, if you check out the term-eval branch of saw-script (which will also require the term-eval branch of the saw-core submodule) you can try it out; if you still think it's useful I can go back and finish it later.

[msaaltink]

I am experimenting a bit, and it seems useful when it works. Sometimes I get the obscure message rebuildTerm VFun, and I do not know what I have done wrong. Any suggestions?

[brianhuffman]

What is the type of the term you're trying to use it with? That's the error message I'd expect to see if you use term_eval_unint on a term with a function type. If it does have a function type, you should be able to make it work by applying the term to some symbolic arguments, as I suggested above.

[msaaltink]

I got the error with term_eval {{ \ (x:[2]Integer) -> [x@0, x@1] == x }}

[brianhuffman]

Indeed, that term has a function type. You'll need to do this instead:

x <- fresh_symbolic "x" {| [2]Integer |};
term_eval {{ [x@0, x@1] == x }};

[msaaltink]

This explains a lot --- I had not clearly understood your original explanation of the restriction. Thanks.

[andreistefanescu]

@brianhuffman our use-case is to use term_eval in order to get rewrite rules to apply after goal_eval, e.g.

prove_print trivial (term_eval {{ \(x : [2]Integer) -> [x@0, x@1] == x }})

so term_eval must be able to handle theorems.

[msaaltink]

@andreistefanescu I have realized that this use case is unlikely to work, at least in cases of the "undo the ripping apart" theorems we seem to need. e.g., above the term_eval just results in True, and had it not done so, the xwould have been split into two parts, as you can see in term_eval {{x == x'}} with x and x' both of type [2]Integer, which comes back as a conjunction of two integer equalities. So while term_eval and term_eval_unint are useful in exploring what various proof steps will do, I don't think they will help much in generating rewrite rules.

[andreistefanescu]

@msaaltink I just realized it's already possible to "undo the ripping apart" for arrays, although I'm not sure why f is necessary:

sawscript> let {{ f : [6][64] -> [6][64]; f x = x }}
sawscript> x <- fresh_symbolic "x" {| [6][64] |};
sawscript> let lhs = term_eval_unint["f"] {{ f x }}
sawscript> t <- prove_print (w4_unint_z3 []) (rewrite (cryptol_ss ()) (rewrite basic_ss (unfold_term ["f"] (abstract_symbolic {{ lhs == f x }}))))
[20:18:46.236] Valid
sawscript> t
[20:21:10.261] Theorem (let { x@1 = Prelude.Vec 64 Prelude.Bool
    }
 in (x : Prelude.Vec 6 x@1)
-> Prelude.EqTrue
     (Prelude.vecEq 6 x@1 (Prelude.bvEq 64)
        [ Prelude.at 6 x@1 x 0
        , Prelude.at 6 x@1 x 1
        , Prelude.at 6 x@1 x 2
        , Prelude.at 6 x@1 x 3
        , Prelude.at 6 x@1 x 4
        , Prelude.at 6 x@1 x 5 ]
        x))
sawscript> lhs
[20:21:11.814] let { x@1 = Prelude.Vec 64 Prelude.Bool
    }
 in cryptol:f#4675
      [ Prelude.at 6 x@1 fresh:x#58 0
      , Prelude.at 6 x@1 fresh:x#58 1
      , Prelude.at 6 x@1 fresh:x#58 2
      , Prelude.at 6 x@1 fresh:x#58 3
      , Prelude.at 6 x@1 fresh:x#58 4
      , Prelude.at 6 x@1 fresh:x#58 5 ]
sawscript> rewrite (addsimp t empty_ss) lhs
[20:21:13.042] cryptol:f#4675 fresh:x#58

[msaaltink]

This will make those rules considerably easier to write, avoiding parse_core entirely. Very neat.

This works for me even if I skip rewriting with basic_ss and go straight to cryptol_ss ().