From dd60b4a292b870e08c23ddcb363630cbb2ed1227 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 2 May 2019 08:16:37 +0200
Subject: [primitive integers] Make div21 implems consistent with its
 specification

There are three implementations of this primitive:
* one in OCaml on 63 bits integer in kernel/uint63_amd64.ml
* one in OCaml on Int64 in kernel/uint63_x86.ml
* one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h
Its specification is the axiom `diveucl_21_spec` in
theories/Numbers/Cyclic/Int63/Int63.v

* comment the implementations with loop invariants to enable an easy
  pen&paper proof of correctness (note to reviewers: the one in
  uint63_amd64.ml might be the easiest to read)
* make sure the three implementations are equivalent
* fix the specification in Int63.v
  (only the lowest part of the result is actually returned)
* make a little optimisation in div21 enabled by the proof of correctness
  (cmp is computed at the end of the first loop rather than at the beginning,
   potentially saving one loop iteration while remaining correct)
* update the proofs in Int63.v and Cyclic63.v to take into account the
  new specifiation of div21
* add a test
---
 kernel/uint63.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/uint63.mli')

diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index b5f40ca804..f25f24512d 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -40,6 +40,10 @@ val rem     : t -> t -> t
       (* Specific arithmetic operations *)
 val mulc    : t -> t -> t * t
 val addmuldiv : t -> t -> t -> t
+
+(** [div21 xh xl y] returns [q % 2^63, r]
+    s.t. [xh * 2^63 + xl = q * y + r] and [r < y].
+    When [y] is [0], returns [0, 0]. *)
 val div21   : t -> t -> t -> t * t
 
       (* comparison *)
-- 
cgit v1.2.3