Uninterpret functions from a Term

[weaversa]

Here is an idea for a new saw command that uninterprets a function (or a sequence of functions) in a Term. To provide an example, below we have a function f that calls g, I then manually uninterpreted g, creating f'. The basic mechanism is to untether the inputs and outputs to the function being uninterpreted, then pull those inputs and outputs up to the top-level Term's entry point. Inputs to the uninterpreted function become new outputs and outputs of the uninterpreted function become new inputs.

In the case where the uninterpreted function is called multiple times, the end user could layer equality (by that I mean EUF) on top manually...or any other constraints really. This would allow one to, for example, use SAT rather than SMT in the presence of uninterpreted functions (which is beneficial for tying into work on UNSAT cores, which SAT solvers support but that there is lax support in SMT solver). This also allows one to transform functions with inverses, for example, an encrypt function (encrypt k p == c) into a decrypt (p == decrypt k c), which would enable more efficient solving because the SAT/SMT solver will unit propagate through the decrypt function (with a known key), where it would normally have to invert the encrypt function (which may be possible, but is certainly much slower than unit propagation).

let {{
f : [32] -> [32] -> [32]
f a b = e
  where
    c = a + b
    d = g c b
    e = a + d

g : [32] -> [32] -> [32]
g a b = b - a

f' : [32] -> [32] -> [32] -> ([32], ([32], [32]))
f' a b d = (e, (c, b))
  where
    c = a + b
    //d = g c b  // uninterpreting `g`
    e = a + d

equals : [32] -> [32] -> [32] -> Bit
equals a b d = (d == g c b) ==> e == e'
  where
    e            = f a b
    (e', (c, _)) = f' a b d
}};

r <- prove (w4_unint_z3 []) {{ \a b d -> equals a b d }};
print r;

[brianhuffman]

What does "EUF" mean?

[weaversa]

Equalities + Uninterpreted Functions. Essentially, if we uninterpret multiple instances of a function, we also want to say that they are all the same function, that is, they all return the same output if given the same input.

[robdockins]

In general, I feel like it would be pretty hard to predict the output of this procedure... if more than one occurrence of the function appears, what order will the inputs/outputs be generated? What if we want to do this with more than one function? Should we unfold definitions to find more occurrences to uninterpret?

I think there's a neat idea here, but I'm not sure how to expose it in a way that I could confidently explain in a user manual. Is this a technique that's implemented in another system already?

[weaversa]

if more than one occurrence of the function appears, what order will the inputs/outputs be generated?

The list of input/output pairs should be treated as unordered. One would necessarily use 'map' to levy extra constraints on them.

What if we want to do this with more than one function?

There would be new input/output sequences, one for each function uninterrupted, in the order given by the sequence of function names in the command.

Should we unfold definitions to find more occurrences to uninterpret?

Yes. It should work just like the smt-based unint commands.

Is this a technique that's implemented in another system already?

I don't know.

[robdockins]

So, if we imagine that two calls to g occurred inside f, you'd want the transformed function to have a type like:

f' : [32] -> [32] -> [2][32] -> ([32], [2]([32],[32]))

Is that right? Then proving something about f "up to uninterpreted g" would look something like:

property fspec a b gouts =
   (and [ gins[i] == gins[j] ==> gouts[i] == gouts[j]  | i <- [0,1], j <- [0,1] ]) => somethingAbout a b e
  where (e, gins) = f' a b gouts

I guess, very broadly, we can think about this as a manual process of doing quantifier elimination of the statement that the inputs and outputs of g have a functional relation. Have I understood the use case right?

If there are interesting data-dependencies flowing from the output of one "uninterpreted" function into another, I think this transformation will force you to prove a different statement than the one you'd get from a standard uninterpreted theory. Maybe that's OK, though; I think the statement you need to prove then is strictly stronger (although I'll have to think pretty hard to convince myself of that).

[weaversa]

@robdockins That seems about right -- though, because of polymorphism, g may be called at multiple types inside f. So, uninterpreting the function name g may result in f' having multiple input/output sequences of uses, each at a different type. (similar to how saw needs function overrides supplied for each monomorphized call)

I'm trying to get to a command where a vanilla SAT solver produces results that are identical (logically) to what an SMT solver would produce using the current SMT unint mechanism. If we produce something that's strictly weaker but easy to strengthen (by manually layering some constraints on top, such as the cartesian equality you have above) then that is a solution to me.

[robdockins]

From a purely user-interface point of view, how do you feel about flattening the function structure using fresh variables? I think it will make the transformation easier to understand and use. For example, the following is an interface I'm thinking about, using the f and g example from above:

x <- fresh_symbolic "x" {| [32] |};
y <- fresh_symbolic "y" {| [32] |};

(t,repls) <- extract_uninterp ["g"] {{ f x y }};

Here t will be a new term of type [32] where all occurences of g have been replaced and repls is something of SAWScript type [(String, (Term,Term))], where the outer list follows the names of the functions requested to be uninterpreted, and the inner lists are pairs where the first Term is the fresh variable that replaced the occurrence of the function, and the second Term is a tuple of the arguments to that function corresponding to that occurrence.

When you're done with manipulating the variable occurrences, you can abstract over them all again with lambdas or abstract_symbolic if necessary.

[weaversa]

@robdockins I like your proposal and the idea of using lambdas to allow the user to control the function type.

It occurred to me that this functionality could also be used to apply function overrides to terms (what we earlier called "grafting").

[robdockins]

OK, I'll work in that direction and see how it goes. I think the result might get a little complicated if g is actually polymorphic as you suggest above, but I think this is a good start.

Indeed, I think it would be pretty easy to do grafting, or general pre/post verification using something like this. The downside is that it adds this term transformation to your trusted base. Maybe that's not too bad, especially if you prove that "grafting" the original function back into the extracted call sites is equal to the original term.

[robdockins]

I've opened a draft PR with an experimental command that implements the idea discussed above: #1185. A quick example follows. I haven't done a lot of testing yet, but if this basic design will suit your use case @weaversa, then I'll keep working along these lines.

let {{
f : [32] -> [32] -> [32]
f a b = e
  where
    c = a + b
    d = g c b
    e = a + g d d

g : [32] -> [32] -> [32]
g a b = b - a

}};

enable_experimental;

print_term (unfold_term ["f"] {{ f }});

x <- fresh_symbolic "x" {| [32] |};
y <- fresh_symbolic "y" {| [32] |};

trs <- extract_uninterp ["g"] {{ f x y }};
let t = trs.0;
let rs = trs.1;

print t;
print rs;

[16:44:38.099] Loading file "/Users/rdockins/code/saw-script/issue1170/test.saw"
[16:44:38.197] let { x@1 = Vec 32 Bool
      x@2 = PRingSeqBool (Cryptol.TCNum 32)
    }
 in \(a : x@1) ->
      \(b : x@1) ->
        let { x@3 = g (ecPlus x@1 x@2 a b) b
            }
         in ecPlus x@1 x@2 a (g x@3 x@3)
[16:44:38.289] let { x@1 = Prelude.Nat
      -> sort 0
      -> sort 0
      x@2 = Prelude.Vec 32 Prelude.Bool
    }
 in Prelude.bvAdd 32 fresh:x#639 fresh:g#642
[16:44:38.289] [("g",[(fresh:g#642,(fresh:g#641,fresh:g#641)),(fresh:g#641,let { x@1 = Prelude.Nat
      -> sort 0
      -> sort 0
      x@2 = Prelude.Vec 32 Prelude.Bool
    }
 in (Prelude.bvAdd 32 fresh:x#639 fresh:y#640,fresh:y#640))])]

[robdockins]

PR #1310 is now merged, which incorporates the new experimental extract_uninterp function.

I'm going to leave this ticket open for now as we continue to experiment with the design, and to remind myself to add tests.

[weaversa]

This works pretty well. One issue I'm having is that this does not seem to be able to uninterpret a primitive such as sortBy or error (which means all built-in functions SuiteB etc. are not usable).

[eddywestbrook]

FWIW, I had to change the above example slightly to get it to work with the current version of SAW. Here is my updated version:

let {{
f : [32] -> [32] -> [32]
f a b = e
  where
    c = a + b
    d = g c b
    e = a + g d d

g : [32] -> [32] -> [32]
g a b = b - a

}};

enable_experimental;

print_term (unfold_term ["f"] {{ f }});

x <- fresh_symbolic "x" {| [32] |};
y <- fresh_symbolic "y" {| [32] |};

trs <- extract_uninterp ["g"] [] {{ f x y }};
let t = trs.0;
let rs = trs.1;

print_term t;
print rs;

[weaversa]

@eddywestbrook Thanks for reworking the example. The issue we were experiencing was on our end.

[weaversa]

Here's the issue (and a potential solution!)

Say we have the following sawscript file that contains a definition that sometimes calls error:

let {{
f : [32] -> [32]
f x = assert (x*x != 16) "oh no!" (x*x)

f_guard : [32] -> Bit
f_guard x = if (x*x) == 16 then False else True
}};

x <- fresh_symbolic "x" {| [32] |};
y <- fresh_symbolic "y" {| [32] |};
let prop = {{ if f_guard x then (f x == y) else False }};

let prop' = lambdas [x, y] {{ prop }};
sat_print z3 {{ \a -> prop' a 625 }};

Even though error in f is guarded by g (it will never be called on any concrete inputs), the symbolic execution process bails:

Run-time error: encountered call to the Cryptol 'error' function

This alone makes use of error (and assert, undefined, etc.) less useful than they could be, as we sometimes need to avoid their use to get proofs to go through. This may be worthy of it's own issue (maybe there already is one?)

It would be nice to replace the error function with something innocuous, but I'm unsure that's possible given the current tools we have. However, we can (with surgical precision) replace the assert function with something meaningful at the term level, namely, the identify function. This is safe to do if prop is safe, meaning it has no undefined behavior (does not error) which is testable using the :safe command in Cryptol:

Cryptol> let f (x : [32]) = assert (x*x != 16) "oh no!" (x*x)
Cryptol> let f_guard x = if (x*x) == 16 then False else True
Cryptol> :safe \x y -> if f_guard x then (f x == y) else False
Safe
(Total Elapsed Time: 0.028s, using "Z3")

Now we can use extract_uninterp to replace assert in prop with the identity function (which I named assert_in_term below).

let {{
f : [32] -> [32]
f x = assert (x*x != 16) "oh no!" (x*x)

f_guard : [32] -> Bit
f_guard x = if (x*x) == 16 then False else True
}};

x <- fresh_symbolic "x" {| [32] |};
y <- fresh_symbolic "y" {| [32] |};
let prop = {{ if f_guard x then (f x == y) else False }};

// let prop' = lambdas [x, y] {{ prop }};
// sat_print z3 {{ \a -> prop' a 625 }};
// Run-time error: encountered call to the Cryptol 'error' function

include "uninterpret_and_replace_in_term.saw";

let {{
assert_in_term : {a, n} (fin n, Eq a) => (Bit, String n, a) -> a -> Bit
assert_in_term (_, _, value) value' = value == value'
}};

prop_no_assert <- uninterpret_and_replace_in_term "assert" {{ assert_in_term }} {{ prop }} [x, y];
sat_print z3 {{ \a -> prop_no_assert a 625 }};  // Sat
sat_print z3 {{ \a -> prop_no_assert a 16 }};   // Unsat

$ saw file.saw
Loading file "file.saw"
Loading file "uninterpret_and_replace_in_term.saw"
Sat: [x = 4294967271, assert = 625]
Unsat
$ cryptol
Cryptol> 4294967271 * 4294967271 : [32]
625

It would be useful to be able to do this w/out having to write an explicit guard...but I don't think it's possible with the tools we have currently.

Contents of uninterpret_and_replace_in_term.saw:

enable_experimental;

rec swapargs_list (func : Term) (hooks : [(Term, Term)]) : TopLevel Term = do {
  trec <- if (null (tail hooks))
          then (do { return {{ True }}; })
          else swapargs_list func (tail hooks);
  let (outputs, inputs) = head hooks;
  return {{ trec /\ (func inputs outputs) }};
};

rec collect_outputs (hooks : [(Term, Term)]) : TopLevel [Term] = do {
  trec <- if (null (tail hooks))
          then (do { return []; })
          else collect_outputs (tail hooks);
  let (outputs, inputs) = head hooks;
  return (concat [ outputs ] trec);
};

let uninterpret_and_replace_in_term (unint_name : String) (replacement_term : Term) (t : Term) (symbolic_vars : [Term]) : TopLevel Term = do {
  a <- extract_uninterp [unint_name] [] t;
  let a_term = a.0;
  let a_hooks = (nth a.1 0).1;

  a_term_swapargs <- swapargs_list replacement_term a_hooks;
  a_outputs <- collect_outputs a_hooks;
  let syms = concat symbolic_vars a_outputs;
  return (lambdas syms {{ a_term_swapargs /\ a_term }});
};

let uninterpret_in_term (unint_name : String) (t : Term) (symbolic_vars : [Term]) : TopLevel Term = do {
  a <- extract_uninterp [unint_name] [] t;
  let a_term = a.0;
  let a_hooks = (nth a.1 0).1;

  a_outputs <- collect_outputs a_hooks;
  let syms = concat symbolic_vars a_outputs;
  return (lambdas syms {{ a_term }});
};