[isabelle] Code generation for compound types with invariant · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation for compound types with invariant

Email Gateway (Jan 14 2024 at 05:51):

This is a question on code generation for types with invariants.

If I understand correctly, Section 3.2 in
https://isabelle.in.tum.de/~haftmann/pdf/data_refinement_in_isabelle_hol_haftmann_krauss_kuncar_nipkow.pdf
(2013) explains that code generation does not support code equations for
lifted definitions targeting compound types where the abstract type does
not appear at the top level.

Here's a simple example where the target type is _ option. One can
similarly construct examples for _ + _ or _ * _.

typedef nat_pos = ‹{ n :: nat . n > 0 }›
   by (simp add: gt_ex)
setup_lifting nat_pos.type_definition_nat_pos

definition nat_minus_one :: ‹nat ⇒ nat option›
   where ‹nat_minus_one n ≡ if n - 1 > 0 then Some (n - 1) else None›

lift_definition nat_pos_minus_one :: ‹nat_pos ⇒ nat_pos option›
   is ‹nat_minus_one› by (auto simp add: nat_minus_one_def)

(* No code equations for nat_pos_minus_one *)
export_code nat_pos_minus_one in OCaml

I am aware that this limitation can be worked around by realizing
nat_pos option as a subtype of nat option. However, while it works
for this toy example, the need to introduce such helper types seems
impractical in general.

Question 1:

Is there a sound way to obtain code equations for examples as above,
without using intermediate types?

Working at the SML-level is fine, so long as it builds atop of existing
code generator interfaces and doesn't require fiddling with the shipped
sources.

Question 2:

Why does the code generator not generate code equations here, even
though lift_definition has generated the correct proof obligations?
What is the soundness risk?

I gather that the soundness of the code generator requires meta-proof
that Abs_C is only used on terms satisfying the invariant. However,
that's exactly what lift_definition asks us to prove. So, it would
seem to me that the following hack would be sound, despite using the
generally unsound code_printing:

definition [code del]: ‹Abs_nat_pos' ≡ Abs_nat_pos›
code_printing constant Abs_nat_pos' ⇀ (OCaml) "Abs'_nat'_pos"

declare nat_pos_minus_one_def[folded Abs_nat_pos'_def, code]
export_code nat_pos_minus_one in OCaml

(*
let rec nat_pos_minus_one
   x = Fun.map_fun rep_nat_pos (Option.map_option Abs_nat_pos)
nat_minus_one x;;
*)

I would be grateful for thoughts on whether this is indeed a sound
workaround for the current limitations.

Thank you,
Hanno

Email Gateway (Jan 14 2024 at 06:50):

From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Hanno,

While not an answer to your questions about the soundness boundaries of the code generator, let me point you to the code_dt feature of lift_definition, which automates the "intermediate type" construction.

Best wishes,
Dmitriy

Email Gateway (Jan 14 2024 at 07:03):

From: hannobecker@posteo.de
Hi Dmitriy,

Oof, I really ought to have noticed this - it's also clearly documented
in the Isabelle Reference Manual. Thanks a lot.

I am still interested in the 2nd question, but the immediate issue is
solved.

All the best,
Hanno

Email Gateway (Jan 15 2024 at 20:15):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Hanno,

Question 1:

Is there a sound way to obtain code equations for examples as above,
without using intermediate types?

see Dmitriy’s answer. It is an omission that code_dt is not mentioned
in the tutorial on code generation, I will take a look at it.

Question 2:

Why does the code generator not generate code equations here, even
though lift_definition has generated the correct proof obligations?
What is the soundness risk?

I gather that the soundness of the code generator requires meta-proof
that Abs_C is only used on terms satisfying the invariant. However,
that's exactly what lift_definition asks us to prove.

Logically, there is no issue concerning that. But technically: the
syntactic requirements for abstract code equations need to be checked,
cf.
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/Isar/code.ML$697
– extending that check to nested types would result in a considerable
amount of additional extra-logical trusted code for things which can be
done inside the logic.

Hope this helps,
Florian

Email Gateway (Jan 16 2024 at 08:11):

From: hannobecker@posteo.de
Hi Florian,

Thank you for your reply. It makes sense to prefer a solution which
builds on top of the existing trusted code base, rather than extending
it.

All the best,
Hanno

Email Gateway (Jan 18 2024 at 05:12):

From: hannobecker@posteo.de
Hi Florian, all,

Quick follow-up: code_dt does not seem to work with compound
invariants. Here is a minimal example:

typedef nat_pos = ‹{ n :: nat . n > 0 ∧ n > 0 }›
   by (simp add: gt_ex)
setup_lifting nat_pos.type_definition_nat_pos

definition nat_minus_one :: ‹nat ⇒ nat option›
   where ‹nat_minus_one n ≡ if n - 1 > 0 then Some (n - 1) else None›

lift_definition (code_dt) nat_pos_minus_one :: ‹nat_pos ⇒ nat_pos
option›
   is ‹nat_minus_one› by (auto simp add: nat_minus_one_def)

(* Tactic failed
The error(s) above occurred for the goal statement⌂:
rel_fun (eq_onp (pred_option (λn. 0 < n ∧ 0 < n))) (eq_onp (λn. 0 < n ∧
0 < n))
  (case_option (Rep_nat_pos undefined) (λx2. x2)) (case_option
(Rep_nat_pos undefined) (λx2. x2)) *)

This can be worked around by wrapping the invariant into a definition.

Best,
Hanno

Email Gateway (Feb 10 2024 at 08:03):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
For the record: In the tutorial on code generation I have added a
reference to lift_definition (which was missing so far). Hopefully this
clarifies the situation.

This refers to rev. 82fbd5919f24 and will be part of the next Isabelle
release.

Cheers,
Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: Apr 29 2024 at 01:08 UTC