Prev: SPARK: What does it prove?
Next: Child vs nested package : efficiency matter
From: Yannick Duchêne (Hibou57) on 29 May 2010 08:06
Hello happy novellers,


I have found some tips which shows to be useful when working with proofs
on program involving modular types.

1) First of all, one you may have seen in a previous thread I've opened,
is the use of Type'Pos. Many times, working with modular types, involves
power of twos. The Ada's exponent operator, expect either a type Natural,
or an Universal_Integer, which can come as you know, where a Natural type
is expected. I feel using an Universal_Integer is more clean, and it can
serves more purpose than Natural can do (see next).

2) Second reason to use a Type'Post to get an Universal_Integer, is when a
classic mathematical proof is to be done on modular types. Modular types
has no associated RTC (RunTime Check), while it is sometime required, if
one want to be sure no significant bits are lost in an operation, to prove
the result would be the same in the infinite set of Universal_Integer. An
example below, shows you a case where an overflow may potentially occurs,
and some Check using Universal_Integer, prove the result is still
meaningful.

3) Third tip, is the usage of user rule to help with the multiple "mod N"
the Examiner adds in expressions involving modular types, to ensure a
conclusion is meaningfully applied to a modular type. This is expected,
while these implicit "mod N" every where, can turns your adventure into a
nightmare when come the time to make some proof. This rule user rule, is a
rewrite rule, used as a simplification rule: “my_mod(1): (X mod M)
may_be_replaced_by X if [ X < M, X >= 0, M > 0 ].”

4) As there is no RTC associated to modulars, take care of cases where no
significant bits must be lost: when so, you must add Check clauses
yourself, which would otherwise not be added by the Examiner.

Now a very simple, while still real life example, which involves all of
these four tips, which comes from a package simply named Bytes (child of a
package Binary).

Note about missing definitions: Instance_Type is mod (2 ** 8), Index_Type
is range 0 .. 7, and Length_Type is range 1 .. 8, Base is constant whose
value is 2.

function Bits_Low_To_High
(Instance : Instance_Type;
First : Index_Type;
Length : Length_Type)
return Instance_Type;
--# pre
--# Length <= Length_To_Last (First);
--# return Result =>
--# Result <= Instance_Type ((2 ** Length_Type'Pos (Length)) - 1);
-- + Provided to help efficiency over function Bit.
-- + Returns a substring of bits from Instance, of
-- Length bits starting at First.
-- + Example:
-- Instance => 2#00101100#
-- First => 2
-- Length => 4
-- return => 2#00001011#


function Bits_Low_To_High
(Instance : Instance_Type;
First : Index_Type;
Length : Length_Type)
return Instance_Type
is
Index_Factor : Instance_Type;
-- + The power of 2 associated with First.
-- + Used to shift Instance to the right.

Length_Factor : Instance_Type;
-- + The power of 2 associated with Length.
-- + Used to generated a bits mask (Mask),
-- i.e. a sequence of Length bits set to 1.

Mask : Instance_Type;
-- + Use to select relevant bits only with a Bitwise-And.

R1 : Instance_Type; -- Result step #1.
R2 : Instance_Type; -- Result step #2.

subtype T is Instance_Type;
-- + Short name to handily get access to T'Pos in proofs.

subtype U is Index_Type;
-- + Short name to handily get access to U'Pos in proofs.

subtype V is Length_Type;
-- + Short name to handily get access to U'Pos in proofs.

begin
-- + Ensure Index_Factor is valid. This would not be otherwise
-- required by an RTC VC, as this is a mod type.
Index_Factor := Base ** Natural (First);
--# check First <= U'Pos (U'Last);
--# check (Base ** Natural (First)) < (T'Pos (T'Last) + 1);
--# check (Base ** Natural (First)) <= T'Pos (T'Last);
--# check T'Pos (Index_Factor) = (Base ** Natural (First));

Length_Factor := Base ** Natural (Length);

Mask := Length_Factor - 1;
-- + Create a string of Length bits set to 1, starting at #0.
-- This is used to delete non-meaningful bits.
-- + If Length = Length_Type'Last, then Length_Factor commits
-- an overflow (which is not an RTC error, as this is a mod type).
-- However, the later checks, which involves Universal_Integer,
-- shows that the final result is still valid and is still
-- the mathematically expected one when computed with Mask,
although
-- Mask may still be computed from a Length_Factor in overflow.

R1 := Instance / Index_Factor;
-- + Move bits #First .. #Index_Type'Last to
-- #0 .. #(Index_Type'Last - First).

R2 := R1 and Mask;
-- + Erase all bits outside of #0 .. #(Length - 1).

--# check T'Pos (R1 and Mask) = T'Pos (R1 mod (Base ** V'Pos
(Length)));
--# check T'Pos (R1 and Mask) < (Base ** V'Pos (Length));
--# check T'Pos (R1 and Mask) <= ((Base ** V'Pos (Length)) - 1);
--# check R2 = (R1 and Mask);
--# check T'Pos (R2) <= ((Base ** V'Pos (Length)) - 1);

return R2;

end Bits_Low_To_High;


Length_Factor, is on overflow when Length is 8, while the mask is still
valid. Every one familiar with bitwise manipulation know that, while this
is still nice to prove things when possible. Here, the last set of Check
clauses, shows that the result computed is still valid, and this proof is
done in the set of Universal_Integer, which is a pure mathematical set.
Without this proof relying on Universal_Integer, one could not formally
assert the Mask is still valid.

Further more, this set of Check clauses, cannot be simplified without the
latter suggested rewrite rule, which is recalled here:


my_mod(1): (X mod M) may_be_replaced_by X if
/* This rule was introduced to help with use of rules applying */
/* to modulars types. */
[ X < M,
X >= 0,
M > 0 ].


Some last and more personal words.

There is something I don't understand with the *.SLG files produced by the
Simplifier: the name “my_mod(1)” rule never appears in *..SLG files, while
it is used. I know it is used, because if I remove it, then it fails to
simplify and prove all VC.

Have a nice day/night.
 | 
Pages: 1
Prev: SPARK: What does it prove?
Next: Child vs nested package : efficiency matter