lh-array-sort--Gibbon Congruence

[Mikah-Kainen]

Joseph

To maximize confidence in the correctness of our Gibbon sorting procedures, we want to edit the Gibbon compiler + standard library and this repository of verified sorts such that the essential verified sorts (DpsMerge.hs, DpsMergePar.hs, DpsMergeParSeqFallback.hs, DpsMergeSort4.hs, DpsMergeSort4Par.hs, Insertion.hs, QuickSort.hs, [CilkSortPar]) can be checked by LiquidHaskell and then compiled with Gibbon with no editing of the file. This feat is itemized into the following tasks, which may grow as new problems are encountered:

• Lemma definitions and terms must pass Gibbon static analysis
  • One solution (my preferred) is to create mock modules for the LiquidHaskell imports, though this requires rewriting lemmas to be Gibbon parseable
  • One solution is a flag-enabled Gibbon pass to delete lem_* function definitions and terms, as well as the unwanted imports
• Module systems must be Gibbon compatible
  • One solution is to admit and finalize the modules branch
  • One solution is to rewrite the sorts in this repository in unqualified style
  • In either case, we likely want to modify the Gibbon compiler to implement or throw out hiding ....
• Typeclasses in types must be removed
  • One solution is to modify all of the verified sorts to be in monomorphic style. This means changing both Haskell and Liquid types so they agree.
• Syntactic sugar must be implemented or desugared
  • where clauses must be addressed
  • Recursive let and where expressions must be moved to the top level
  • All currying must be made explicit
• Standard libraries must agree
  • An alternate Gibbon stdlib array module (and possibly beyond arrays) needs to be made that is 1-to-1 with the way we define primitives in the sorting repository. There could be subtleties with library primitives beyond arrays and with name-shadowing fundamental compiler primitives.
• Compiler bugs that cannot be worked around may need to be resolved
  • Innocuous lines such as here (when decurried) lead to erroneous Gibbon L0 typechecking errors that seem impossible to work around.
    • Following the comment in the active DpsMerge.hs, using merge_ in DpsMergeSort.hs directly yields an erroneous type error.
    • It's likely that typechecking application or arrow types is in general bugged.
  • Definitions may need to be shuffled, or Gibbon may need to be patched, due to other L0 and L1 errors.
    • Following the comment in the active DpsMerge.hs, uncommenting and moving merge_ to the bottom of the file yields an erroneous type error.

---

Copied from: https://github.com/michaelborkowski/lh-array-sort/issues/3.