Interaction between Time and Datarefinement

[maxhaslbeck]

A subtle problem occured concerning the interaction between data refinement and time. Here I will summarize what we tried, what does not work, and what a possible solution is.
At the moment I'm too lost in details, that I can judge whether the solution is viable, but I'm quite confident. Here we go:

The problem

We identified that with the normal definition of Data refinement:

isabelle_llvm_time/thys/nrest/Data_Refinement.thy

Lines 8 to 9 in 5accf6c

	definition conc_fun ("\<Down>") where
	"conc_fun R m \<equiv> case m of FAILi \<Rightarrow> FAILT | REST X \<Rightarrow> REST (\<lambda>c. Sup {X a| a. (c,a)\<in>R})"

we get a problem when proving the Data refinement rule for hn_refine:

isabelle_llvm_time/thys/sepref/Hnr_Primitives_Experiment.thy

Lines 130 to 134 in 5accf6c

	apply fri
	done
	lemma SomeSup_D: "Some y \<le> Sup {M' a |a. (r, a) \<in> RR} \<Longrightarrow> (\<exists>a. (r, a) \<in> RR)"
	unfolding Sup_option_def by (auto split: if_splits)

The problem here is, that the supremum in Data refinement may overapproximate too much, i.e. the supremum over the costs of all the abstract results that refine a certain concrete result may not be a cost actually attained by some abstract result.
Consequently, it is possible that one cannot find such an abstract element after data refinement. But one needs such an element ra for hnr:

isabelle_llvm_time/thys/sepref/Sepref_Basic.thy

Lines 186 to 193 in 5accf6c

	definition "hn_refine \<Gamma> c \<Gamma>' R m \<equiv>
	nofailT m \<longrightarrow>
	(\<forall>F s cr M. m = REST M \<longrightarrow>
	llSTATE (\<Gamma> \<and>* F) (s,cr) \<longrightarrow>
	(\<exists>ra Ca. M ra \<ge> Some Ca
	\<and> wp c (\<lambda>r. llSTATE (\<Gamma>' \<and>* R ra r \<and>* F \<and>* GC)) (s, cr+Ca)
	)
	)"

First approach: use abs_fun

First thing we tried is to use abs_fun instead of conc_fun:

isabelle_llvm_time/thys/nrest/Data_Refinement.thy

Lines 11 to 13 in 5accf6c

	definition abs_fun ("\<Up>") where
	"abs_fun R m \<equiv> case m of FAILi \<Rightarrow> FAILT
	| REST X \<Rightarrow> if dom X\<subseteq>Domain R then REST (\<lambda>a. Sup {X c| c. (c,a)\<in>R}) else FAILT"

The good thing is, that \<Up> RR m ≤ m' implies, that there exists an abstract element in m', and we are happy. We can prove

isabelle_llvm_time/thys/sepref/Hnr_Primitives_Experiment.thy

Lines 109 to 112 in 5accf6c

	using assms aux[of RR M M']
	by fastforce
	lemma hn_refine_result':

with this.
Also we can prove other important facts about data refinement:

• monotonicity: `m ≤ m' ==> <Up> RR m ≤ <Up> RR m'"
• give a meaning with inresT
• chain: abs_fun (S O R) M ≤ abs_fun R (abs_fun S M)

But the rule for RETURN as well as WHILE needs the side condition Single Valued!

isabelle_llvm_time/thys/nrest/Data_Refinement.thy

Lines 426 to 427 in 5accf6c

	lemma RETURNT_SV_refine: "single_valued R \<Longrightarrow> (x,x')\<in>R \<Longrightarrow> \<Up> R (RETURNT x) \<le> (RETURNT x' :: ('a,('b,enat)acost) nrest)"
	by(auto simp: pw_acost_le_iff refine_pw_simps inresT_abs_fun dest: single_valuedD)

So this is far from ideal. We could live with it, but would not be able to use multi-valued relations

The canonical counter example:

The counter example that emerged is the following:

say in the abstract m'there are results a1 and a2, and there are two currency components.
Let m' a1 = Some (0,1) and m' a1 = Some (1,0). now let a1 and a2 be abstractions of some concrete value c: R=(c,a1),(c,a2). now data refinement would lead to conc_fun R m' = [c|->(1,1)].
and we would have [c|->(1,1)] <= conc_fun R m' but no abstract value that can serve as a justification for the concrete cost (1,1).

While this problem here is just an illustration, the real problem occurs whenever the Supremum is not attained:
X ≠ {} --> Sup X ∉ X

In the following I call this sup-non-attainment.

What are we looking for?

We are looking for some a definition of conc_fun that implies that, data refinement makes sure that the supremum is attained.
Something like:

SPECT m <= conc_fun R (SPECT m') --> c \in dom m --> Sup {m' a| a. (c,a)∈R} \in {m' a| a. (c,a)∈R}

And here are the properties we need:

• monotonicity
• chaining (at least one direction)
• bind rule must hold
• rule for RETURN should not involve Single_valued side condition

Another approach: penalise sup-non-attainment

Another idea is to penalise when the Sup is not attained:

Penalise with None

definition conc_fun'' where
  "conc_fun'' R m ≡ case m of FAILi ⇒ FAILT | REST X ⇒
           REST (λc. if Sup {X a| a. (c,a)∈R} ∈ {X a| a. (c,a)∈R} then Sup {X a| a. (c,a)∈R} else None)"

with this we can prove

lemma aux'':
  fixes M :: "_ ⇀ _" 
  assumes "SPECT M ≤ conc_fun'' RR (SPECT M')"
  shows "∀r∈dom M. ∃r'. (r,r')∈RR ∧ M r ≤ M' r'" 

And with it, also hn_refine_result.

Unfortunately, chaining conc_fun R1 (conc_fun R2 m') <= conc_fun (R1 O R2) m' does not hold:
say we have 3 abstract values a1,a2,a3, the abstract program m' assigns [a1|->(0,1), a2|->(1,0), a3|->(1,0)]. then say we have R1 = {(c,b1), (c,b2)} and R2 = {(b1,a1), (b1,a2), (b2,a3)}.
then morally (conc_fun R2 m') b1 = None and (conc_fun R2 m') b2 = Some (1,0), and thus conc_fun R1 (conc_fun R2 m') b1 = Sup { None, Some (1,0) } = Some (1,0). So the "bad" part is penalized by None which does not hurt and is superseeded by the Some (1,0).
On the other hand, R1 O R2 = {(c,a1), (c,a2), (c,a3)}, and conc_fun (R1 O R2) m' c = None because the Sup would be (1,1) and is not attained.

Penalise with FAILT

Now it starts to get ugly, you can savely skip this.
We now penalise with FAILT, as it is propagated through the Sup:

definition conc_funF where
  "conc_funF R m ≡ case m of FAILi ⇒ FAILT | REST X ⇒
           Sup {( if {X a| a. (c,a)∈R}≠{} ⟶ Sup {X a| a. (c,a)∈R} ∈ {X a| a. (c,a)∈R} then REST ((λ_.None)(c:= Sup {X a| a. (c,a)∈R})) else FAILT)|c. True}"

we can then prove:

lemma auxF:
  fixes M :: "_ ⇀ _" 
  assumes "SPECT M ≤ conc_funF RR (SPECT M')"
  assumes *: "conc_funF RR (SPECT M') ≠ FAILT"
  shows "∀r∈dom M. ∃r'. (r,r')∈RR ∧ M r ≤ M' r'" 

but only with the side condition *. Which might be fine to show that in a last step.

Also we can get around the counter example from above.

But it already gets ugly when concerning monotonicity:
imagine conc_funF RR (SPECT M') = SPECT MM' is fine, because all the abstract values in M' for example have cost (1,1).
now consider an M that assigns to some abstract values (1,0) and to some (0,1). Then certainly M<= M' but `conc_funF RR (SPECT M)=FAILT.

Okay, at this point I gave up, and had a sleep.

Attack the Problem where it occurs (A solution?)

After a night's sleep and some good rest, I figured that everything works out with the original conc_fun if we have single valued data Refinement. But we want more. Just more enough that we can model eo_array, which is intrinsically multi-valued.
We identified that the sup-non-attainment is the problem. And that might just be the characterization of when things work and when not.

One way we could do is: use the normal conc_fun and get all the nice properties (monotonicity, chaining, bind-rule, RETURNT-rule) and only add a side condition (weaker than SV, but strong enough to imply sup-attainment) to hn_refine_result:

isabelle_llvm_time/thys/sepref/Hnr_Primitives_Experiment.thy

Lines 182 to 186 in 5accf6c

	lemma hn_refine_result_loose:
	assumes R: "hn_refine P c Q R m"
	assumes LE: "m\<le>\<Down>RR m'"
	assumes WB: "\<And>r M' M. m=SPECT M \<Longrightarrow> m'=SPECT M' \<Longrightarrow> r\<in>dom M \<Longrightarrow> (\<exists>a. (r,a)\<in>RR) \<Longrightarrow> Sup {M' a| a. (r,a)\<in>RR} \<in> {M' a| a. (r,a)\<in>RR}"
	shows "hn_refine P c Q (hr_comp R RR) m'"

Single_valued implies the sup-attainment:

isabelle_llvm_time/thys/sepref/Hnr_Primitives_Experiment.thy

Lines 159 to 161 in 5accf6c

	lemma single_valued_SupinSup:
	fixes M' :: "_ \<Rightarrow> (_::complete_lattice) option"
	shows "single_valued RR \<Longrightarrow> (\<exists>a. (r,a)\<in>RR) \<Longrightarrow> Sup {M' a| a. (r,a)\<in>RR} \<in> {M' a| a. (r,a)\<in>RR}"

It might be the case, that sup-attainment even is too strong.

And I guess we are fine. We can use the plain conc_fun and all its nice properties to reason about abstract programs, without worrying about tomorrow when we actually want to implement it with Sepref.
Even while using sepref on the a concrete program in NREST we do not see the problem. Only when we want to materialize a Hoare Triple or pull together a hn_refinement and a Data Refinement we have to make sure that the Sup is attained.

I'm quite confident that all of this makes sense, but maybe I miss some important point
Please check what I wrote at least in this section.

TODO: check whether the algorithm with data refinement sd23_relin Sorting_Heapsort does fullfill the sup-attainment property. But I guess, it does, as long as the abstract algorithm M assignes all every abstract value, either the same cost, or a chain.

Yeah, what we have to test in hn_refine_result is, that RR and abstract M' have the sup-attainment property.

Why did I not see the problem before

I think I just did not try to prove hn_refine_result yet for multi-currency NREST.

For the single currency in the framework for ITP19 the problem seems not to occur, as we do not use infinite Time Credits. I think when asking for an abstract result that has more cost than a finite number, either the aggregated cost is finite and bigger, or it's infinity. If it's infinity, either because there is an abstract result with infinite cost (then we're done) or the Sup is infinite (but infinity not in the set), then we can always find an abstract element whose cost is bigger than the constant concrete cost. and we're good.
Only asking for a justification for an infinite concrete time, with an abstract result, where all the results are finite, but the Supremum is infinite would have failed. As we only modeled finite Time credits this problem did not occur.

The theorem is hnr_comp in Sepref_Rules of Sepreftime, and it has a quite involved and ugly proof :D.