Jannik Mähn (Sep 01 2023 at 09:12): Jannik Mähn (Sep 01 2023 at 09:12):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?
Paolo Giarrusso (Sep 01 2023 at 18:55):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
Paolo Giarrusso (Sep 01 2023 at 18:56):(not sure if this helps at all, I lack context for a more helpful answer)
Théo Winterhalter (Sep 01 2023 at 19:30):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.
Théo Winterhalter (Sep 01 2023 at 19:31):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).
Théo Winterhalter (Sep 01 2023 at 19:32):Also we have handy tactics like ssprove_sync for when two programs start the same way.
Théo Winterhalter (Sep 01 2023 at 19:33):Have you had a look at https://github.com/SSProve/ssprove/blob/main/DOC.md#proving-relational-judgments ?
Sebastian Ertel (Sep 03 2023 at 11:47):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?
Théo Winterhalter (Sep 03 2023 at 12:13):What does the goal look like?
Sebastian Ertel (Sep 03 2023 at 18:24):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?
Théo Winterhalter (Sep 03 2023 at 18:27):Or maybe apply rpost_weaken_rule before.
Last updated: Oct 13 2024 at 01:02 UTC