Commit fcfb8db4 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

indentation

parent 9ff4791e
...@@ -56,13 +56,13 @@ module Bitwalker ...@@ -56,13 +56,13 @@ module Bitwalker
<-> BV64.ult x (maxvalue len) } <-> BV64.ult x (maxvalue len) }
(** return [value] with the bit of index [left] from the left set to [flag] *) (** return [value] with the bit of index [left] from the left set to [flag] *)
let poke_64bit_bv (value : BV64.t) (left : BV32.t) (flag : bool) let poke_64bit_bv (value : BV64.t) (left : BV32.t) (flag : bool) : BV64.t
requires { BV32.to_uint left < 64 } requires { BV32.to_uint left < 64 }
ensures { forall i. 0 <= i < 64 /\ i <> 63 - BV32.to_uint left -> ensures { forall i. 0 <= i < 64 /\ i <> 63 - BV32.to_uint left ->
BV64.nth result i = BV64.nth value i } BV64.nth result i = BV64.nth value i }
ensures { flag = BV64.nth result (63 - BV32.to_uint left) } ensures { flag = BV64.nth result (63 - BV32.to_uint left) }
= =
assert {BV32.ult left (BV32.of_int 64) }; assert { BV32.ult left (BV32.of_int 64) };
abstract abstract
ensures { forall i:BV32.t. i <> BV32.sub (BV32.of_int 63) left -> ensures { forall i:BV32.t. i <> BV32.sub (BV32.of_int 63) left ->
BV64.nth_bv result (C32_64.toBig i) = BV64.nth_bv result (C32_64.toBig i) =
...@@ -81,7 +81,7 @@ module Bitwalker ...@@ -81,7 +81,7 @@ module Bitwalker
(* return the bit of [byte] at position [left] starting from the left *) (* return the bit of [byte] at position [left] starting from the left *)
let peek_8bit_bv (byte : BV8.t) (left : BV32.t) let peek_8bit_bv (byte : BV8.t) (left : BV32.t) : bool
requires { 0 <= BV32.to_uint left < 8 } requires { 0 <= BV32.to_uint left < 8 }
ensures { result = BV8.nth byte (7 - BV32.to_uint left) } ensures { result = BV8.nth byte (7 - BV32.to_uint left) }
= =
...@@ -97,27 +97,27 @@ module Bitwalker ...@@ -97,27 +97,27 @@ module Bitwalker
end end
(* return the bit of the [left]/8 element of [addr] at position mod [left] 8 starting from the left *) (* return the bit of the [left]/8 element of [addr] at position mod [left] 8 starting from the left *)
let peek_8bit_array (addr : array BV8.t) (left : BV32.t) let peek_8bit_array (addr : array BV8.t) (left : BV32.t) : bool
requires{ 8 * (length addr) < BV32.two_power_size } requires { 8 * (length addr) < BV32.two_power_size }
requires{ BV32.to_uint left < 8 * length addr } requires { BV32.to_uint left < 8 * length addr }
ensures{ result = nth8_stream addr (BV32.to_uint left) } ensures { result = nth8_stream addr (BV32.to_uint left) }
= =
peek_8bit_bv (addr[ BV32.to_uint (BV32.udiv_check left (BV32.int_check 8)) ]) (BV32.urem_check left (BV32.int_check 8)) peek_8bit_bv (addr[ BV32.to_uint (BV32.udiv_check left (BV32.int_check 8)) ]) (BV32.urem_check left (BV32.int_check 8))
(* return a bitvector of 64 bits with its [len] bits of the right (* return a bitvector of 64 bits with its [len] bits of the right
set to the bits between [start] and [start] + [len] of [addr] *) set to the bits between [start] and [start] + [len] of [addr] *)
let peek (start : BV32.t) (len : BV32.t) (addr : array BV8.t) : BV64.t let peek (start : BV32.t) (len : BV32.t) (addr : array BV8.t) : BV64.t
requires{ BV32.to_uint len <= 64 } requires { BV32.to_uint len <= 64 }
requires{ BV32.to_uint start + BV32.to_uint len < BV32.two_power_size } requires { BV32.to_uint start + BV32.to_uint len < BV32.two_power_size }
requires{ 8 * length addr < BV32.two_power_size } requires { 8 * length addr < BV32.two_power_size }
ensures{BV32.to_uint start + BV32.to_uint len > (8 * length addr) -> result = BV64.zero} ensures { BV32.to_uint start + BV32.to_uint len > (8 * length addr) ->
ensures{BV32.to_uint start + BV32.to_uint len <= (8 * length addr) -> result = BV64.zero }
(forall i:int. 0 <= i < BV32.to_uint len -> ensures { BV32.to_uint start + BV32.to_uint len <= (8 * length addr) ->
BV64.nth result i (forall i:int. 0 <= i < BV32.to_uint len ->
= nth8_stream addr (BV32.to_uint start + BV32.to_uint len - i - 1)) BV64.nth result i
/\ (forall i:int. BV32.to_uint len <= i < 64 -> = nth8_stream addr (BV32.to_uint start + BV32.to_uint len - i - 1))
BV64.nth result i /\
= False)} (forall i:int. BV32.to_uint len <= i < 64 -> BV64.nth result i = False) }
= =
if (BV32.to_uint (BV32.add_check start len) > ( 8 *length addr )) if (BV32.to_uint (BV32.add_check start len) > ( 8 *length addr ))
then then
......
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