Add lift_functional_correctness

This lemma makes proving simple properties about the deployed contract
state of a contract easier.

theories/Automation.v

@@ -79,6 +79,12 @@ Ltac destruct_match :=
   | [H: context [ match ?x with _ => _ end ] |- _] => destruct x eqn:?
   end.
 
+Ltac destruct_if :=
+  match goal with
+  | [|- context [ if ?x then _ else _ ]] => destruct x eqn:?
+  | [H: context [ if ?x then _ else _ ] |- _] => destruct x eqn:?
+  end.
+
 Ltac destruct_units :=
   repeat
     match goal with

theories/Blockchain.v

@@ -1146,6 +1146,86 @@ Proof.
     auto.
 Qed.
 
+Lemma lift_functional_correctness
+      {Setup Msg State : Type}
+      `{Serializable Setup}
+      `{Serializable Msg}
+      `{Serializable State}
+      (contract : Contract Setup Msg State)
+      (DeployFacts : Chain -> ContractCallContext -> Prop)
+      (CallFacts : Chain -> ContractCallContext -> Prop)
+      (P : State -> Prop) :
+  (forall chain ctx setup result,
+    DeployFacts chain ctx ->
+    init contract chain ctx setup = Some result ->
+    P result) ->
+  (forall chain ctx prev_state msg new_state new_acts,
+      CallFacts chain ctx ->
+      P prev_state ->
+      receive contract chain ctx prev_state msg = Some (new_state, new_acts) ->
+      P new_state) ->
+  (forall (prev_bstate : ChainState) act new_env new_acts
+          (eval : ActionEvaluation prev_bstate act new_env new_acts),
+      reachable prev_bstate ->
+      match eval with
+      | eval_deploy from to amount _ _ _ _ _ _ _ _ _ _ _ =>
+        DeployFacts (transfer_balance from to amount prev_bstate)
+                    (build_ctx from to amount)
+      | eval_call from to amount _ _ _ _ _ _ _ _ _ _ _ _ _ =>
+        CallFacts (transfer_balance from to amount prev_bstate)
+                  (build_ctx from to amount)
+      | _ => True
+      end) ->
+  forall bstate caddr,
+    reachable bstate ->
+    env_contracts bstate caddr = Some (contract : WeakContract) ->
+    exists cstate,
+      contract_state bstate caddr = Some cstate /\
+      P cstate.
+Proof.
+  intros init_case call_case establish_facts
+         bstate caddr [trace] contract_deployed.
+  destruct (deployed_contract_state_typed contract_deployed ltac:(auto))
+    as [cstate cstate_stored].
+  exists cstate; split; auto.
+  revert cstate cstate_stored.
+  unfold contract_state in *.
+  remember empty_state; induction trace as [|? ? ? ? IH];
+    intros; subst; cbn in *; try congruence.
+  destruct_chain_step.
+  - (* New block *)
+    rewrite_environment_equiv; auto.
+  - (* Evaluation *)
+    specialize (establish_facts _ _ _ _ eval).
+    destruct_action_eval; subst; rewrite_environment_equiv; cbn in *.
+    + (* Transfer, just use IH directly. *)
+      auto.
+    + (* Deployment *)
+      destruct_address_eq; subst; auto.
+      (* Of this contract. *)
+      replace wc with (contract : WeakContract) in * by congruence.
+      destruct (wc_init_strong ltac:(eassumption))
+        as [setup_strong [result_strong [? [<- init]]]].
+      cbn in *.
+      rewrite deserialize_serialize in cstate_stored.
+      replace result_strong with cstate in * by congruence.
+      eauto using init_case.
+    + (* Call *)
+      destruct_address_eq; subst; auto.
+      replace wc with (contract : WeakContract) in * by congruence.
+      destruct (wc_receive_strong ltac:(eassumption))
+        as [prev_state_strong [msg_strong [resp_state_strong [? [? [<- receive]]]]]].
+      cbn in *.
+      rewrite deserialize_serialize in cstate_stored.
+      replace resp_state_strong with cstate in * by congruence.
+      specialize (IH eq_refl ltac:(auto) prev_state_strong).
+      replace (env_contract_states prev to) with (Some prev_state) in * by auto.
+      cbn in *.
+      specialize (IH ltac:(auto)).
+      eauto using call_case.
+  - (* Permutation *)
+    rewrite prev_next in *; auto.
+Qed.
 End Theories.
 End Trace.
 End Semantics.

theories/Congress.v

@@ -379,6 +379,50 @@ Definition contract : Contract Setup Msg State :=
 Section Theories.
 Local Open Scope nat.
 
+(* The rules stored in the blockchain's state are always valid *)
+Lemma rules_valid bstate caddr :
+  reachable bstate ->
+  env_contracts bstate caddr = Some (Congress.contract : WeakContract) ->
+  exists cstate,
+    contract_state bstate caddr = Some cstate /\
+    validate_rules cstate.(state_rules) = true.
+Proof.
+  apply lift_functional_correctness with (DeployFacts := fun _ _ => True)
+                                         (CallFacts := fun _ _ => True).
+  - intros chain ctx setup result _ init.
+    cbn in *.
+    unfold Congress.init in init.
+    destruct_if; try congruence.
+    now inversion_clear init.
+  - intros chain ctx prev_state msg new_state new_acts _ prev_valid receive.
+    cbn in *.
+    destruct msg as [[]|]; cbn in *;
+      try solve [
+            repeat
+              match goal with
+              | [H: Some ?x = Some ?y |- _] => inversion_clear H; auto
+              | _ => try congruence; destruct_if
+              end].
+    + destruct_if; try congruence.
+      unfold vote_on_proposal in receive.
+      destruct (FMap.find _ _); cbn in *; try congruence.
+      now inversion_clear receive.
+    + destruct_if; try congruence.
+      unfold vote_on_proposal in receive.
+      destruct (FMap.find _ _); cbn in *; try congruence.
+      now inversion_clear receive.
+    + destruct_if; try congruence.
+      unfold do_retract_vote in receive.
+      destruct (FMap.find _ _); cbn in *; try congruence.
+      destruct (FMap.find _ _); cbn in *; try congruence.
+      now inversion_clear receive.
+    + unfold do_finish_proposal in receive.
+      destruct (FMap.find _ _); cbn in *; try congruence.
+      destruct_if; cbn in *; try congruence.
+      now inversion_clear receive.
+  - now destruct eval.
+Qed.
+
 Definition num_acts_created_in_proposals (txs : list Tx) :=
   let count tx :=
       match tx_body tx with