Commit 5c794073 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Fix session

parent 5804ead8
......@@ -41,9 +41,9 @@ module N
lemma limb_max_bound: 1 <= max_uint64
function l2i (x:limb) : int = Limb.to_int x
let ghost function l2i (x:limb) : int = Limb.to_int x
function p2i (i:int32) : int = Int32.to_int i
let ghost function p2i (i:int32) : int = Int32.to_int i
exception Break
exception Return32 int32
......@@ -182,7 +182,7 @@ module N
use import mach.c.C
type t = ptr limb
function value (x:t) (sz:int) : int =
let ghost function value (x:t) (sz:int) : int =
value_sub (pelts x) x.offset (x.offset + sz)
function compare_int (x y:int) : int =
......@@ -1616,12 +1616,14 @@ module N
let ghost q = power 2 (Limb.length - p2i r) in
assert { p * x <= radix - p
by
p * q = radix
p * q = radix
so mod radix p = mod (q * p) p = 0
so mod (p * x) p = 0
so p * x < radix
so mod (radix - p) p = mod (p * (-1) + radix) p
= mod radix p = 0
so p * x < radix = p * q
so (x < q by p > 0)
so radix - p = p * (q - 1)
so x <= q - 1
so p * x <= p * (q - 1)
};
r
......@@ -3382,7 +3384,14 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
* vy * power radix !i
+ value x sx
so sx = sy + !i
so (pelts x)[x.offset + sy + !i - 1] = !x1
so x.offset + sy + !i - 1 = !xp.offset + 1
so (pelts x)[x.offset + sy + !i - 1] =
(pelts x)[!xp.offset + 1]= !x1
so value x sx
= value x (sx - 1)
+ power radix (sx -1) * (pelts x)[x.offset + sx - 1]
= value x (sy + !i - 1)
+ power radix (sy + !i - 1) * (pelts x)[x.offset + sy + !i - 1]
so value x (sy + !i - 1)
+ power radix (sy + !i - 1) * !x1
= value x sx
......
......@@ -20,10 +20,10 @@ module C
}
(*invariant { in_us_bounds data.length, offset }*)
function plength (p:ptr 'a) : int
let ghost function plength (p:ptr 'a) : int
= p.data.length
function pelts (p:ptr 'a) : int -> 'a
let ghost function pelts (p:ptr 'a) : int -> 'a
= p.data.elts
val p2i (n:int32):int
......
......@@ -217,7 +217,7 @@ module UInt32
let constant max_uint32 : int = 0xffff_ffff
let constant length : int = 32
constant radix : int = max_uint32 + 1
let constant radix : int = max_uint32 + 1
(*lemma pow2_length : radix = power 2 32*)
......@@ -443,7 +443,7 @@ module UInt64
let constant max_uint64 : int = 0xffffffffffffffff
let constant length : int = 64
constant radix : int = max_uint64 + 1
let constant radix : int = max_uint64 + 1
(*lemma pow2_length : radix64 = power 2 64*)
......
......@@ -1279,19 +1279,12 @@ module MLToC = struct
begin
match idef with
| Some (Dalias ty) -> Some (C.Dtypedef (ty_of_mlty info ty, id))
| Some _ -> if debug then Format.printf "Ddata/Drecord@.";
None (*FIXME unsupported*)
| Some _ -> raise (Unsupported "Ddata/Drecord@.")
| None ->
begin match query_syntax info.syntax id with
| Some _ -> None
| None ->
if debug
then
Format.printf
"type declaration without syntax or alias: %s@."
id.id_string;
None (*FIXME*)
(* raise (Unsupported ("type declaration without syntax or alias: "^id.id_string)) *)
raise (Unsupported ("type declaration without syntax or alias: "^id.id_string))
end
end
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment