Big-step lemmas for invariant framework

[jadephilipoom]

@blaxill and @fshaked , here's the lemmas I think you will need for the HMAC proof strategy we discussed just now. Basically, if you have a function that can turn a list of HMAC inputs into a list of SHA inputs, then you can feed the SHA inputs into these lemmas (particularly postcondition_holds_big_step and invariant_holds_big_step) in order to prove that e.g. the SHA postcondition holds on the latest output.

This way, the HMAC representation can be the list of HMAC inputs so far. In the invariant, you'd get the SHA inputs from the HMAC inputs, and the invariant would be something like:

fun hmac_inputs '(_, ... , _, sha_state) =>
  let sha_inputs := sha_inputs_from_hmac_inputs hmac_inputs in
  (* sha circuit state matches inputs *)
  sha_state = snd (simulate' sha256 sha_inputs (reset_state sha256))
  (* SHA precondition holds on all inputs so far *)
  /\ precondition_holds_big_step (c:=sha256) reset_repr sha_inputs
  /\ sha256_invariant sha_state (repeat_update_repr reset_repr sha_inputs)

In order to get a useful postcondition based on whether the inner SHA circuit is done, you can define a function that looks at the SHA higher-level representation plus SHA input and decides whether the SHA circuit is done using logic similar to the SHA postcondition (basically duplicate the logic in the SHA postcondition for that specific bit of output). If that function is called get_sha_done_bit, then the postcondition would look something like:

fun new_input hmac_inputs out =>
  let sha_inputs := sha_inputs_from_hmac_inputs hmac_inputs in
  let new_sha_input := last default (sha_inputs_from_hmac_inputs (hmac_inputs ++ new_input)) in
  let sha_repr := (repeat_update_repr reset_repr sha_inputs) in
  if get_sha_done_bit sha_repr new_sha_input
  then <...the output is the expected hash, you can get the message from sha_repr...>
  else <...the output says we're still processing...>

This isn't necessarily the strategy I'd recommend if there was unlimited time, but I think this might be the shortest path to getting the paper-essential proofs done.

[blaxill]

This isn't necessarily the strategy I'd recommend if there was unlimited time, but I think this might be the shortest path to getting the paper-essential proofs done.

FWIW HMAC inputs -> SHA inputs is the hmac_inner component, so it would be a replacement (simpler) proof for the hmac_inner. The hmac and hmac_top don't directly translate to a fold on their inputs because their output (eventually into SHA) is influenced by why the SHA module is ready (so for those circuits repeat_update_repr would need additional logic).

[jadephilipoom]

influenced by why the SHA module is ready (so for those circuits repeat_update_repr would need additional logic).

The SHA postcondition fully specifies the is_ready bit, so it might be easier to use repeat_update_repr as-is and then duplicating the logic from the SHA postcondition that corresponds to the is_ready signal. Then, in your hmac_top postcondition or wherever, you can compute the SHA representation with repeat_update_repr and then just do get_sha_ready_bit just like I've illustrated with get_sha_done_bit above to make your postcondition depend on it.