Normalizing script evaluation with knowledge from the environment

[azike]

Hi!
I try to execute a stack-based parser implementation for a scripting language in F*. Scripts are given as lists of opcodes. For that matter, I have a recursive evaluation function that calls a step function for each opcode in the script.
When evaluating the function using normal assert the smt solver fails as expected, due to the deeply nested recursion.
However, it works when calling the normalizer first, e.g. assert_norm.
Now I want to be able to evaluate the script, based on knowledge I have in my current environment.
To be more precise, the parser supports verification of signatures using a function called verify. If I am in a context where I know that a given key verifies a specific signature, I would like to apply that knowledge during evaluation.
Based on that I have two questions:

1. During normalization the definition of verify gets unfolded (checking the type the key and the signature), however I'd like to prevent normalization of verify and apply grewrite_eq given my current assumptions.
   I found out that I can use norm norm_steps to guide the normalization process. The options for delta rule application (delta, delta_attr, delta_only,...) allow to specify which definitions get unfolded, but there is no rule to specify a marker that prevents unfolding (e.g. unfold everything except definitions annotated with [@@do_not_norm]).
   I don't want to annotate verify with irreducible, as this proof is a special case and the annotation would break other proofs.
   Is there any other way I could tackle this problem?

2. Is it possible to search for a specific equality term in the current environment and then apply it to the goal using grewrite_eq?
   Currently, I got access to the right binder by asserting the implication of my goal given the context and using implies_intro:

let verify_script pk signature = 
	let script = some_predefined_script in
	if verify pk signature then
	        assert (verify pk signature);  (*can assert verification here*)
		assert ((verify pk signature) ==> (eval script)) by (
			compute (); (*do not unfold definition of verify*)
			let b = implies_intro () in
			grewrite_eq b);
		...
	else ...

Overall I would like to normalize the script evaluation as much as possible until I can apply knowledge of my environment to the current goal with rewrite_eq and then continue with normalization.

Thank you in advance for any hints.

[nikswamy]

hi @azike

For your question 1:

We do not have a way of excluding specific symbols from unfolding while unfolding everything else. Our general philosophy around this has been that if you want this level of precise control over which symbols are unfolded, then it's better to explicitly list all the things you want to unfold, rather than specifying a mixture of things that should and should not be unfolded. It takes a bit of discipline, but we often add attributes to the symbols that we want to unfold, sometimes even grouping related symbols by tagging them with the same attribute. See this, for example: https://github.com/project-everest/everparse/blob/master/src/3d/prelude/EverParse3d.Interpreter.fst#L1341-L1357

Note, you've probably seen this already, in addition to requesting unfolding of things marked with attributes, we also have delta_qualifier and delta_namespace: https://github.com/FStarLang/FStar/blob/master/ulib/FStar.Pervasives.fsti#L277-L279

For your question 2:

Mixing reduction and rewriting is delicate and there are potentially many ways to do it, with various tradeoffs. If the term you're trying to reduce is large, then bouncing back and forth between reduction and rewriting can quickly become very inefficient. If you can say a bit more about the style of proof you're doing, I can probably suggests some options.

As for getting your hands on the equality: Is verify_script meant to be a lemma about some_predefined_script? Control flow hypothesis such as those that arise from conditionals in a lemma are not directly in the environment, rather in the verification condition produced for this block of code. So, getting access to that equality hypothesis is a bit indirect. E.g., you could also do something like this, which is roughly equivalent:

if verify pk signature then
  let hyp:squash (verify pk signature==true) = () in
  assert (eval script) by (  ... you can find hyp in the environment now and rewrite with it.. )

There might be a nicer way ... @mtzguido, this reminds me of a recent conversation we had. Any other tips?

[azike]

Thank you for your fast response @nikswamy!

1. I understand your intuition behind that design choice. Maybe using delta_namespace will make things easier.
   A small remark: When looking at the implementation of Pervasives.fst the definition of delta_qualifier is not UnfoldQualifier but UnfoldAttr, see https://github.com/FStarLang/FStar/blob/master/ulib/FStar.Pervasives.fst#L113 .

2. It's a bit hard to describe. In essence, we are interested in evaluating scripts, or more or less proving that a specific script will run successfully given some conditions hold (e.g. verify pk signature == true).
   The example I posted verify_script is not directly meant to be a lemma, but some function. In our real use, its within an effect and the script evaluation is part of proofing the postcondition.
   In the best case we would simply like to assert_norm (eval script) and just do plain evaluation, but because we are depending on hypotheses (e.g. through branching) this doesn't work.
   So, our next idea is to provide lemmas for each script we want to evaluate, stating in the required clause our hypotheses and then ensure correct evaluation.
   The proof would be then performed within the lemma and we only need to proof it once, and later on rely on our preconditions.
   Still, we depend on the same "normalize and rewrite" problem, as the normalizer can not unfold definitions he does not know.
   I would consider the term to be reduced in moderate size, but it also depends on the script.
   The parser is implemented as state monad, causing some big unfolding.

3. I will definitely try out your recommendation regarding getting access to the hypothesis.
   Just a quick followup question: by defining hyp this way (with squash), will it be introduced as a binder with the name hyp in the proof environment?

EDIT: I tried the squash thing with let hyp : squash (verify pk signature == true) = () in ... , but I can't find hyp in the environment.

EDIT2: I am running FStar version F* 2023.04.26~dev and use FStar.Tactics