[CakeML-dev] Naming of split ...ProofScript.sml files

[Magnus Myreen]

Hi dev,

The proofs for data_to_word are currently in two large files:

  0) data_to_wordPropsScript.sml is 8300 lines
  1) data_to_wordProofScript.sml is 15600 lines

I propose that (1) is split into separate files as follows.

  a) a file that defines state_rel and GC, verifies the GC
  b) a file that proves the bignum lemmas
  c) a file that proves the Assign case of data_to_word
  d) a file that verifies compile_def

I would prefer to keep (0) intact. Its purpose is to define memory_rel
and prove reusable lemmas about it. Policy: (0) should be as
independent as possible from the definition of wordLang and its
semantics.

I suspect that there isn't much resistance to splitting large files as
outlined above. So my question is mostly about how the separate files
should be named. Here's a suggestion:

 0) data_to_word_memoryProofScript.sml
 a) data_to_word_gcProofScript.sml
 b) data_to_word_bignumProofScript.sml
 c) data_to_word_assignProofScript.sml
 d) data_to_wordProofScript.sml

Any comments / concerns?

If no one objects, I'll make these changes on the clos_stub branch
where I'm currently working in (c) for ConsExtend.

Cheers,
Magnus