Constants involving ExtCns

[robdockins]

The following operation makes sure to abstract a constant over any ExtCns values it mentions. As I recall, this is done to make sure that the bodies of constants are in some sense "totally closed". Is this restriction actually important/relied upon for anything we are doing? Would anything go wrong if we relaxed it? @brianhuffman

saw-script/saw-core/src/Verifier/SAW/SharedTerm.hs

Lines 1453 to 1471 in 4222c6e

	-- | Create an abstract constant with the specified name, body, and
	-- type. The term for the body must not have any loose de Bruijn
	-- indices. If the body contains any ExtCns variables, they will be
	-- abstracted over and reapplied to the resulting constant.
	scConstant :: SharedContext
	-> Text -- ^ The name
	-> Term -- ^ The body
	-> Term -- ^ The type
	-> IO Term
	scConstant sc name rhs ty =
	do unless (looseVars rhs == emptyBitSet) $
	fail "scConstant: term contains loose variables"
	let ecs = getAllExts rhs
	rhs' <- scAbstractExts sc ecs rhs
	ty' <- scFunAll sc (map ecType ecs) ty
	ec <- scFreshEC sc name ty'
	t <- scTermF sc (Constant ec rhs')
	args <- mapM (scFlatTermF sc . ExtCns) ecs
	scApplyAll sc t args

I ask because it would be nice if we could allow Cryptol primitive declarations to be ultimately translated into Coq Parameter declarations, which would allow us to do proofs about operations that are held totally abstract. I have a branch that works in this direction and translates Cryptol primitive terms into ExtCns, which are then translated to Coq Parameter declarations. So far so good. However, any declarations that mention these primitives get turned into Constant terms which then are abstracted over all the ExtCns that they mention, and the declarations I wanted are now lambda-abstracted over the primitives instead of referencing them the way I wanted.

[brianhuffman]

As I recall, the abstracting over ExtCns variables was done to deal with a certain confusing situation that @atomb had encountered in some actual SAW proofs. What happened was that we had an LLVMSetup block that introduced some variables with llvm_fresh_var (thus producing Term values represented as ExtCns) and then within the same LLVMSetup block there was a let {{ lhs = rhs }} declaration that defined some other constants in terms of those variables.

Not only was this situation confusing, but I believe that it was actually unsound because when the override from such a proof was applied, it's supposed to do a substitution to replace the ExtCns variables from the crucible_fresh_var bindings with the values it was matched against. But they weren't being substituted because the occurrences were hidden inside a Constant. This led later to things being proved equal when they shouldn't have been.

[robdockins]

I see, so there's some mismatch between the contract of the Constant constructor (which is that terms with the same name are identical) and having ExtCns inside that are subject to substitution.

OK, I'll have to think some more about what is a good way to achieve what I want.

[brianhuffman]

We might be able to just split ExtCns into two flavors:

• free variables, which are implicitly quantified over (although the quantifier itself is outside the term) and you might want to substitute for other terms within SAW
• actual "external constants", which are effectively fixed constants as far as SAW is concerned, but which might have special meanings in certain SAW backends

Defined Constants in SAW would be allowed to contain the 2nd flavor, but not the 1st.

Actually it seems like the second flavor is basically like Primitive, isn't it?

[robdockins]

Currently Primitive nodes are only used for things arising from saw-core modules, and are required to have saw-core identifiers. I think this is an OK restriction.

An idea I have a prototype implementation of is to allow Constant nodes that have no definition. They behave a lot like ExtCns, but are not subject to substitution. In the evaluator, they can be provided with alternative realizations (just like other constants), and produce a new kind of neutral term otherwise.