Missing llvm_assert

[robdockins]

We have llvm_precond and llvm_postcond, which allow users to state arbitrary logical conditions to be added to the pre or post condition of a function specification. However, there is no agnostic llvm_assert, which will work in either the pre or postcondition. Although the llvm_precond and llvm_postcond operators are nice to allow users to state their intentions clearly, a phase agnostic operator is also useful when writing higher-level helpers, that e.g, specify the state of an entire data structure and make sense in both pre and post conditions. In these situations, we might wish to state invariants about the datastructure (e.g., relating different values appearing in it) that make sense in both pre and post phases.

Similar considerations apply to jvm_precond and jvm_postcond.

[RyanGlScott]

Are the intended semantics of llvm_assert that it will behave like llvm_precond or llvm_postcond depending on where in a specification it gets used during runtime? (This is basically how it's done in the Python bindings.)

[robdockins]

Are the intended semantics of llvm_assert that it will behave like llvm_precond or llvm_postcond depending on where in a specification it gets used during runtime? (This is basically how it's done in the Python bindings.)

Indeed. I'm pretty sure we used to basically have this, and it got replaced by the precond/postcond pair.

[smithnormform]

Is there any progress on this? I think this would substantially reduce code duplication in helper functions.

[smithnormform]

Don't contracts already support this with the proclaim method in Python? I think removing the @deprecated in the code below and renaming proclaim to assert (or just making a new non-deprecated method with the same definition called assert) would resolve this issue for the Python API. It would be nice to have an assert_f method as well.

saw-script/saw-remote-api/python/saw_client/crucible.py

Lines 495 to 508 in 7a8fc9a

	@deprecated
	def proclaim(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None:
	"""DEPRECATED: Use ``precondition`` or ``postcondition`` instead. This method will
	eventually be removed."""
	if not isinstance(proposition, CryptolTerm):
	condition = Condition(CryptolTerm(proposition))
	else:
	condition = Condition(proposition)
	if self.__state == 'pre':
	self.__pre_state.conditions.append(condition)
	elif self.__state == 'post':
	self.__post_state.conditions.append(condition)
	else:
	raise Exception("wrong state")

[weaversa]

From #196 we have:

let llvm_assert (t : Term) =
  llvm_equal (llvm_term {{ if t then 0b1 else 0b0 }}) (llvm_term {{ 0b1 }});

What would that look like in Python?

[weaversa]

sawscript> :h llvm_equal
Description
-----------

    llvm_equal : SetupValue -> SetupValue -> LLVMSetup ()

State that two LLVM values should be equal. Can be used as either a
pre-condition or a post-condition. It is semantically equivalent to
an `llvm_precond` or `llvm_postcond` statement which is an equality
predicate, but potentially more efficient

[robdockins]

That might work, although it's a bit clunky.

I think it would be pretty easy to add a primitive llvm_assert, and I'm planning to work on it this week.

[smithnormform]

Could this also be added to the Python API?

[RyanGlScott]

Yes, we should. As you've noted, the already-existing proclaim function basically serves the same role as llvm_assert, so the most straightforward way to make this available in Python is to undeprecate proclaim. I've filed #1676 as a reminder to do this.