Dear SSprovers,
I ran into the following error that I do not understand / cannot solve. I’ve reproduced it in the following miniature example:
From Relational Require Import OrderEnrichedCategory GenericRulesSimple.
Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import all_ssreflect all_algebra reals distr realsum
fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum
eqtype choice seq.
Set Warnings "notation-overridden,ambiguous-paths".
From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings
UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb
pkg_core_definition choice_type pkg_composition pkg_rhl
Package Prelude RandomOracle.
From Coq Require Import Utf8.
From extructures Require Import ord fset fmap.
Require Import Coq.Init.Logic.
Require Import List.
Set Bullet Behavior "Strict Subproofs".
Set Default Goal Selector "!".
Set Primitive Projections.
Import PackageNotation.
Module SignatureDefs.
Variable (n: nat).
Definition pos_n: nat := 2^n.
Definition Seed : choice_type := chFin(mkpos pos_n).
Definition SecKey : choice_type := chFin(mkpos pos_n).
Definition PubKey : choice_type := chFin(mkpos pos_n).
Parameter KeyGen : Seed -> (SecKey × PubKey).
End SignatureDefs.
Module RemoteAttestation (π : SignatureDefs).
Import π.
Notation " 'pubkey " := PubKey (in custom pack_type at level 2) : package_scope.
Notation " 'seckey " := SecKey (in custom pack_type at level 2) : package_scope.
Notation " 'seed " := Seed (in custom pack_type at level 2) : package_scope.
Definition pk_loc : Location := (PubKey ; 0%N).
Definition sk_loc : Location := (SecKey ; 1%N).
Definition key_gen : nat := 42.
Definition KeyGen_locs := fset [:: pk_loc ; sk_loc ].
Definition KG_interface := [interface #val #[key_gen] : 'seed → 'pubkey ].
Definition KG_real :
package KeyGen_locs [interface] KG_interface
:=
[package #def #[key_gen] (sd : 'seed) : 'pubkey {
let (sk,pk) := KeyGen sd in
ret pk }
].
Definition KG_ideal :
package KeyGen_locs [interface] KG_interface
:=
[package #def #[key_gen] (sd : 'seed) : 'pubkey {
let (sk,pk) := KeyGen sd in
ret pk }
].
Definition mkpair {Lt Lf E} (t: package Lt [interface] E) (f: package Lf [interface] E) : loc_GamePair E :=
fun b => if b then {locpackage t} else {locpackage f}.
Definition KG_ind := @mkpair KeyGen_locs KeyGen_locs KG_interface KG_real KG_ideal.
Lemma KG_real_vs_KG_true :
KG_ind true ≈₀ KG_ind false.
Proof.
eapply eq_rel_perf_ind_eq.
simplify_eq_rel x.
all: ssprove_code_simpl.
eapply rsame_head_alt.
I create two identical packages for a Key Generation with an input seed, KG_real
and KG_ideal
.
When trying to prove them indistignuishable, I want to eapply
the rsame_head_alt
on a parametric function KeyGen
.
Then, I get the following error:
H : ∀ (m : raw_code ?A) (f₀ f₁ : ?A -> raw_code ?B)
(pre : precond) (post : postcond ?B ?B),
ValidCode ?L (fset [::]) m ->
(∀ ℓ : Location, ℓ \in ?L -> get_pre_cond ℓ pre) ->
(∀ (ℓ : Location) (v : Value ℓ.π1),
ℓ \in ?L -> put_pre_cond ℓ v pre) ->
(∀ a : ?A, ⊢ ⦃ pre ⦄ f₀ a ≈ f₁ a ⦃ post ⦄) ->
locked r⊨ ⦃ pre ⦄ x ← m ;;
f₀ x ≈ x ← m ;;
f₁ x ⦃ post ⦄
Unable to unify
"(let 'Datatypes.tt := master_key in id)
r⊨ ⦃ ?M2595 ⦄ x ← ?M2592 ;;
?M2593 x ≈ x ← ?M2592 ;;
?M2594 x ⦃ ?M2596 ⦄",
where master_key
is defined in the SSReflect library.
Why do I get this error, and how can I resolve it?
That's only half the error, but that use of master_key looks like an use of ssreflect locking: your tactic is trying to unfold something that's designed not to be unfolded
(not sure if this helps at all, I lack context for a more helpful answer)
Yes, this is indeed what is happening, so it obfuscates the error message unfortunately. If you look at rsame_head_alt
you will see it expects a goal of the form ⊢ ⦃ pre ⦄ x ← m ;; f₀ x ≈ x ← m ;; f₁ x ⦃ post ⦄
meaning with bind
on both sides. So unification here is trying to unfold stuff to reach something of this form and it doesn't work.
This is because you do not use bind
at all in your programs. So instead, you might want to use the ret
rule (because you have returns on both sides) or the reflexivity rule (since you have the same thing on both sides).
Also we have handy tactics like ssprove_sync
for when two programs start the same way.
Have you had a look at https://github.com/SSProve/ssprove/blob/main/DOC.md#proving-relational-judgments ?
Hi @Paolo Giarrusso ,
thanks for your reply.
We had found this definition in the SSReflect documentation but could not figure out its use.
Hi @Théo Winterhalter ,
thanks also for you answer.
We apologize. The reported code is slightly inconsistent.
We already had a monadic version of KeyGen
but received the same error message.
Just to clarify:
The proof for the non-monadic version from above would look like this:
Lemma KG_real_vs_KG_true : KG_ind true ≈₀ KG_ind false.
Proof.
eapply eq_rel_perf_ind_eq.
simplify_eq_rel x.
all: ssprove_code_simpl.
Fail eapply rreflexivity_rule.
(*
The command has indeed failed with message:
In environment
x : Seed
hin : (key_gen, (Seed, PubKey)) \in KG_interface
f : src (key_gen, (Seed, PubKey)) -> raw_code (tgt (key_gen, (Seed, PubKey)))
H : {| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |} =
{| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |}
H0 : eq_rect Seed (λ x0 : choice_type, ∑ T : choice_type, x0 -> raw_code T)
(PubKey; λ sd : 'I_pos_n, ret (nsnd (KeyGen sd))) Seed
(Classes.noConfusion (Classes.noConfusion H)) = (PubKey; f)
H1 : ∀ c : raw_code ?A, locked r⊨ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄ c ≈ c ⦃ eq ⦄
Unable to unify
"(let 'Datatypes.tt := master_key in id) r⊨ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄ ?M2534 ≈ ?M2534 ⦃ eq ⦄" with
"⊢ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄ f x ≈ f x ⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ /\ s₀ = s₁ ⦄".
*)
Fail ssprove_sync.
(*
The command has indeed failed with message:
Tactic failure: No head found.
*)
Fail eapply r_ret.
(*
The command has indeed failed with message:
In environment
x : Seed
hin : (key_gen, (Seed, PubKey)) \in KG_interface
f : src (key_gen, (Seed, PubKey)) -> raw_code (tgt (key_gen, (Seed, PubKey)))
H : {| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |} =
{| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |}
H0 : eq_rect Seed (λ x0 : choice_type, ∑ T : choice_type, x0 -> raw_code T)
(PubKey; λ sd : 'I_pos_n, ret (nsnd (KeyGen sd))) Seed
(Classes.noConfusion (Classes.noConfusion H)) = (PubKey; f)
H1 : ∀ (u₀ : ?A₀) (u₁ : ?A₁) (pre : precond) (post : postcond ?A₀ ?A₁),
(∀ s₀ s₁ : heap, pre (s₀, s₁) -> post (u₀, s₀) (u₁, s₁)) ->
locked r⊨ ⦃ pre ⦄ ret u₀ ≈ ret u₁ ⦃ post ⦄
Unable to unify
"(let 'Datatypes.tt := master_key in id) r⊨ ⦃ ?M2540 ⦄ ret ?M2538 ≈ ret ?M2539 ⦃ ?M2541 ⦄" with
"⊢ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄ f x ≈ f x ⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ /\ s₀ = s₁ ⦄".
*)
Abort.
When we now add a monadic version of KeyGen
like so:
Module Type SignatureDefs.
(* ... Definitions from above ...*)
#[local] Open Scope package_scope.
Parameter KeyGenM : ∀ {L : {fset Location}} (sd : Seed),
code L [interface] (SecKey × PubKey).
End SignatureDefs.
and then reformulate the code in the packages to:
'(sk,pk) ← KeyGenM sd ;;
ret pk
then the proof would need the application of rsame_head
:
Lemma KG_real_vs_KG_true : KG_ind true ≈₀ KG_ind false.
Proof.
eapply eq_rel_perf_ind_eq.
simplify_eq_rel x.
all: ssprove_code_simpl.
Fail eapply rsame_head.
(*
The command has indeed failed with message:
In environment
x : Seed
hin : (key_gen, (Seed, PubKey)) \in KG_interface
f : src (key_gen, (Seed, PubKey)) -> raw_code (tgt (key_gen, (Seed, PubKey)))
H : {| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |} =
{| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |}
H0 : eq_rect Seed (λ x0 : choice_type, ∑ T : choice_type, x0 -> raw_code T)
(PubKey; λ sd : 'I_pos_n, x ← KeyGenM sd ;;
(let '(_, pk) := x in ret pk)) Seed (Classes.noConfusion (Classes.noConfusion H)) =
(PubKey; f)
H1 : ∀ (m : raw_code ?A) (post : postcond ?B ?B),
(∀ a : ?A, ⊢ ⦃ λ '(h₀, h₁), h₀ = h₁ ⦄ ?f₀ a ≈ ?f₁ a ⦃ post ⦄) ->
locked r⊨ ⦃ λ '(h₀, h₁), h₀ = h₁ ⦄ x ← m ;;
?f₀ x ≈ x ← m ;;
?f₁ x ⦃ post ⦄
Unable to unify
"(let 'Datatypes.tt := master_key in id)
r⊨ ⦃ λ '(h₀, h₁), h₀ = h₁ ⦄ x ← ?M2562 ;;
?f₀ x ≈ x ← ?M2562 ;;
?f₁ x ⦃ ?M2563 ⦄" with
"⊢ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄ f x ≈ f x ⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ /\ s₀ = s₁ ⦄".
*)
Fail eapply rsame_head_alt.
(*
The command has indeed failed with message:
In environment
x : Seed
hin : (key_gen, (Seed, PubKey)) \in KG_interface
f : src (key_gen, (Seed, PubKey)) -> raw_code (tgt (key_gen, (Seed, PubKey)))
H : {| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |} =
{| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |}
H0 : eq_rect Seed (λ x0 : choice_type, ∑ T : choice_type, x0 -> raw_code T)
(PubKey; λ sd : 'I_pos_n, x ← KeyGenM sd ;;
(let '(_, pk) := x in ret pk)) Seed (Classes.noConfusion (Classes.noConfusion H)) =
(PubKey; f)
H1 : ∀ (m : raw_code ?A) (f₀ f₁ : ?A -> raw_code ?B) (pre : precond) (post : postcond ?B ?B),
ValidCode ?L (fset [::]) m ->
(∀ ℓ : Location, ℓ \in ?L -> get_pre_cond ℓ pre) ->
(∀ (ℓ : Location) (v : Value ℓ.π1), ℓ \in ?L -> put_pre_cond ℓ v pre) ->
(∀ a : ?A, ⊢ ⦃ pre ⦄ f₀ a ≈ f₁ a ⦃ post ⦄) ->
locked r⊨ ⦃ pre ⦄ x ← m ;;
f₀ x ≈ x ← m ;;
f₁ x ⦃ post ⦄
Unable to unify
"(let 'Datatypes.tt := master_key in id)
r⊨ ⦃ ?M2571 ⦄ x ← ?M2568 ;;
?M2569 x ≈ x ← ?M2568 ;;
?M2570 x ⦃ ?M2572 ⦄" with
"⊢ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄ f x ≈ f x ⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ /\ s₀ = s₁ ⦄".
*)
Abort.
Is it possible that, for some reason, the tactics are trying to unfold KeyGen
/KeyGenM
?
What does the goal look like?
In the non-monadic case, it is:
x : Seed
hin : (key_gen, (Seed, PubKey)) \in KG_interface
f : src (key_gen, (Seed, PubKey)) -> raw_code (tgt (key_gen, (Seed, PubKey)))
H : {| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |} =
{| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |}
H0 : eq_rect Seed (λ x0 : choice_type, ∑ T : choice_type, x0 -> raw_code T)
(PubKey; λ sd : 'I_pos_n, ret (nsnd (KeyGen sd))) Seed
(Classes.noConfusion (Classes.noConfusion H)) = (PubKey; f)
============================
⊢ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄
f x
≈
f x
⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ /\ s₀ = s₁ ⦄
For the monadic case, it is:
x : Seed
hin : (key_gen, (Seed, PubKey)) \in KG_interface
f : src (key_gen, (Seed, PubKey)) -> raw_code (tgt (key_gen, (Seed, PubKey)))
H : {| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |} =
{| Init.pr1 := pos_n; Init.pr2 := PositiveExp2 π.n |}
H0 : eq_rect Seed (λ x0 : choice_type, ∑ T : choice_type, x0 -> raw_code T)
(PubKey; λ sd : 'I_pos_n, x ← KeyGenM sd ;;
(let '(_, pk) := x in ret pk)) Seed (Classes.noConfusion (Classes.noConfusion H)) =
(PubKey; f)
============================
⊢ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄
f x
≈
f x
⦃ λ '(b₀, s₀) '(b₁, s₁), b₀ = b₁ /\ s₀ = s₁ ⦄
Does r_reflexivity_alt
work?
Or maybe apply rpost_weaken_rule
before.
Last updated: Oct 13 2024 at 01:02 UTC