Finalizing Proof of Lemma using the Invariant

[JaMaeh]

Due to changes in the protocols/ primitives, the proof of the main invariant Lemma in RA.v does not go through.

The old goal looks like this:

x: 'unit
hin: (get_pk_att, ('unit, 'pubkey)) \in Att_interface
___________________________________________________
(1/1)
⊢ ⦃ full_heap_eq' ⦄
   x0 ← get pk_loc ;;
   ret x0 
≈
   v ← get pk_loc ;;
   ret v 
⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ /\ full_heap_eq' (s₀, s₁) ⦄

and is solved like this:

sync_sig_att. 1: { auto_in_fset. }
      move => a; by [apply r_ret].

Now, due to the changes, the code looks as follows:

x: 'unit
hin: (get_pk_att, ('unit, 'pubkey)) \in Att_interface
____________________________________________________
(1/1)
⊢ ⦃ full_heap_eq' ⦄
   #put sk_loc := nfst KeyGen ;;
   #put pk_loc := nsnd KeyGen ;;
   x0 ← get pk_loc ;;
   ret x0 
≈
   #put sk_loc := nfst KeyGen ;;
   #put pk_loc := nsnd KeyGen ;;
   v ← get pk_loc ;;
   ret v 
⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ /\ full_heap_eq' (s₀, s₁) ⦄

Common ways to remove the puts such as eapply r_put_vs_put or ssprove_sync_eq => sk_loc. do not work.

[sertel]

But you cannot use ssprove_sync_eq because our invariant is not an equality.
But I believe that ssprove_sync should actually do the job.

[JaMaeh]

ssprove_sync throws the following error:

Error: In environment
x : 'unit
hin : (get_pk_att, ('unit, 'pubkey)) \in Att_interface
Unable to unify
 "⊢ ⦃ λ '(s₀, s₁), ?M5596 (s₀, s₁) ⦄ x ← cmd cmd_put ?M5594 ?M5595 ;;
                                     ret x ≈ x ← cmd 
                                             cmd_put ?M5594 ?M5595 ;;
                                             ret x ⦃ λ '(a₀, s₀) '(a₁, s₁),
                                                ?M5596 (s₀, s₁) /\ a₀ = a₁ ⦄"
with
 "⊢ ⦃ full_heap_eq' ⦄ x ← cmd cmd_put sk_loc (nfst KeyGen) ;;
                      ret x ≈ x ← cmd cmd_put sk_loc (nfst KeyGen) ;;
                              ret x ⦃ λ '(a₀, s₀) '(a₁, s₁),
                                        full_heap_eq' (s₀, s₁) /\ a₀ = a₁ ⦄".

[sertel]

Ah ok.
This actually would work if the precondition would have the right shape. This really is problem in SSProve that we should also provide a fix for.

Thanks for the description. I will take care of that.