Code assertions: mechanism to support maintenance of big abstract excutable developments

[fhaftmann]

Description of changes:

Code setups stemming from locales via global interpretation may be brittle.

Code assertions may check global interpretations immediately.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[hanno-becker]

Thank you very much @fhaftmann. We will check this on some larger internal development as well before merging.

[hanno-becker]

@fhaftmann General question: How should one think about the syntax and pervasive options?

The Isabelle reference manual notes

If the (pervasive) option is given, the corresponding declaration is applied to all possible contexts involved, including the global background theory.

but this isn't quite enough for me to understand when/how to use this option.

[fhaftmann]

Such corner cases can often only be examined by looking at the sources.

Here my (opinionated) answer:

• Locales support syntax, which is maybe a historic accident – syntax is so intricate that it is difficult to maintain along arbitrary interpretations except rather »canonical« ones. Nevertheless it is there, and in some situations syntax declarations needs to be treated differently from other declarations using syntax to distinguish both.
• pervasive means the declaration is also applied to the background theory (after applying a suitable morphism); this is for declarations which require some kind of permanent »trace« beyond the current (bounded) local theory.

(btw. questions which go beyond the scope of this PR can be asked best on the Isabelle mailing list.)

[hanno-becker]

Could we add a concrete example here? Something like

               
section ‹Example›

locale Code_Assertion_Test_Locale = 
  fixes f g :: ‹'a ⇒ 'a›
  assumes f4_id: ‹f ∘ f ∘ f ∘ f = id›
      and g_id: ‹g = id›
begin

definition f2 :: ‹'a ⇒ 'a› where
  ‹f2 x ≡ f (f x)›

definition f3 :: ‹'a ⇒ 'a› where
  ‹f3 x ≡ f (f2 x)›

definition f3' :: ‹'a ⇒ 'a› where
  ‹f3' x ≡ g (f2 x)›

code_assertion f2 f3 in OCaml

text‹If you comment in the following, then ▩‹global_interpretation› will fail below,
because the concrete instantiation for ▩‹g› has no code equation.›
(* code_assertion f3' in OCaml *)

end

consts int_id_in_disguise :: ‹int × int ⇒ int × int›
lemma int_id_in_disguise: ‹int_id_in_disguise x = x› sorry

definition int_rotate90 :: ‹int × int ⇒ int × int› where
  ‹int_rotate90 t ≡ let (x,y) = t in (-y, x)›

global_interpretation Code_Assertion_Test_Locale_Global: Code_Assertion_Test_Locale int_rotate90 int_id_in_disguise
  defines f22 = ‹Code_Assertion_Test_Locale_Global.f2›
       and f3 = ‹Code_Assertion_Test_Locale_Global.f3›
       and f3' = ‹Code_Assertion_Test_Locale_Global.f3'›
  by standard (auto simp add: comp_def int_rotate90_def int_id_in_disguise split!: prod.splits)

but happy about other ideas.

[fhaftmann]

Good idea, I will take care of it.

[hanno-becker]

Could we add some log output showing that the code extraction check is happening? Something like

fun assert_code_for thy target_name consts =
  let val lthy : local_theory = Named_Target.theory_init thy
    val consts' = consts |> Syntax.read_terms lthy |> List.map (Syntax.pretty_term lthy)
  in
    tap (fn _ => consts' |> Pretty.big_list "Code_Assertion: Checking code-extraction for the following constants: " |> Pretty.writeln)
    Code_Target.produce_code (Proof_Context.init_global thy) false consts target_name Code_Target.generatedN NONE []
  end

but there may be better ways.

[fhaftmann]

Something like this can surely be done, yes.

[hanno-becker]

@fhaftmann Thank you very much for this contribution.

I think the underlying idea is clever and useful. I am still in the process of evaluating the change on our internal proof base, but so far things look good from a technical perspective.

From a usability perspective, I wonder about the following:

In our internal application, we have global interpretations with hundreds of definitions being code exported. Each of those definitions already features in multiple places:

1. The actual definition in the locale.
2. The defines ... clause in the global_interpretation
3. The constant list in the final export_code ... command.

With the addition of code_assertion, a fourth list is added, which is technically benign, but yet more boilerplate and visual impediment.

The most natural place to put the code_assertions, would be after the constant definitions themselves, but that is too slow since separate calls to code_assertion lead to separate declarations.

I wonder if there is a way to add code assertions through attributes. Ideally, I'd like to do something like this:

locale foo
begin

definition bar0[code_assert] where ...
definition bar1[code_assert] where ...
...
definition barN[code_assert] where ...


end

so that when foo is globally interpreted, a single code-assertion check is performed for all declarations tagged with code_assert.

Do you think that's feasible?

EDIT: Not quite the same, but going some way, would be the following

named_theorems extractable

definition foo[extractable] ...
definition bar[extractable] ...
...

code_assertion extractable

if one accordingly modifies code_assertion so that it doesn't expect a list of constant names, but a list of definitional theorems.

[fhaftmann]

locale foo
begin

definition bar0[code_assert] where ...
definition bar1[code_assert] where ...
...
definition barN[code_assert] where ...

end

This should work and is a step into the right direction, I will take care for this.