spark-bignum.git
7 years agoAdd TODO file. master
Reto Buerki [Fri, 21 Jan 2011 09:49:33 +0000 (10:49 +0100)]
Add TODO file.

8 years agoAdd simplified BSD license headers.
Adrian-Ken Rueegsegger [Fri, 8 Oct 2010 13:23:33 +0000 (15:23 +0200)]
Add simplified BSD license headers.

This is a preparatory step necessary for the inclusion of the SPARK
bignum library in libsparkcrypto.

8 years agoAdd annotations to main.adb, run SPARK tools.
Reto Buerki [Fri, 1 Oct 2010 16:28:54 +0000 (18:28 +0200)]
Add annotations to main.adb, run SPARK tools.

8 years agoUse SPARKUnit for benchmarks.
Reto Buerki [Fri, 1 Oct 2010 10:43:43 +0000 (12:43 +0200)]
Use SPARKUnit for benchmarks.

8 years agoRename function Remainder_Limb to Mod_Limb.
Adrian-Ken Rueegsegger [Tue, 24 Aug 2010 17:58:42 +0000 (19:58 +0200)]
Rename function Remainder_Limb to Mod_Limb.

8 years agoSwitch back to 32 bit Word_Size.
Reto Buerki [Tue, 24 Aug 2010 15:40:09 +0000 (17:40 +0200)]
Switch back to 32 bit Word_Size.

8 years agoLet large signed type depend on Word_Size.
Reto Buerki [Tue, 24 Aug 2010 15:11:07 +0000 (17:11 +0200)]
Let large signed type depend on Word_Size.

8 years agoLet large unsigned type depend on Word_Size.
Reto Buerki [Tue, 24 Aug 2010 15:09:31 +0000 (17:09 +0200)]
Let large unsigned type depend on Word_Size.

8 years agoUse large signed type as Integer replacement.
Reto Buerki [Tue, 24 Aug 2010 15:06:37 +0000 (17:06 +0200)]
Use large signed type as Integer replacement.

8 years agoMake Radix_Type a proper type instead of a subtype.
Reto Buerki [Tue, 24 Aug 2010 14:55:02 +0000 (16:55 +0200)]
Make Radix_Type a proper type instead of a subtype.

8 years agoLong_Div: Add another check annotation.
Reto Buerki [Mon, 23 Aug 2010 16:33:38 +0000 (18:33 +0200)]
Long_Div: Add another check annotation.

8 years agoLong_Div: Add check annotation to discharge RTC.
Reto Buerki [Mon, 23 Aug 2010 15:26:11 +0000 (17:26 +0200)]
Long_Div: Add check annotation to discharge RTC.

8 years agoAdd user-rules to prove Normalize_Divisor procedure.
Adrian-Ken Rueegsegger [Mon, 23 Aug 2010 10:52:38 +0000 (12:52 +0200)]
Add user-rules to prove Normalize_Divisor procedure.

8 years agoFactor out divisor normalization to Normalize_Divisor.
Adrian-Ken Rueegsegger [Mon, 23 Aug 2010 10:40:30 +0000 (12:40 +0200)]
Factor out divisor normalization to Normalize_Divisor.

8 years agoAdjust user-rule file handling.
Adrian-Ken Rueegsegger [Mon, 23 Aug 2010 10:39:25 +0000 (12:39 +0200)]
Adjust user-rule file handling.

8 years agoAdd 16 bit variant of modulus_property user rule.
Reto Buerki [Thu, 19 Aug 2010 09:10:20 +0000 (11:10 +0200)]
Add 16 bit variant of modulus_property user rule.

8 years agoExtend Bit_Length_Limb return annotation.
Adrian-Ken Rueegsegger [Wed, 18 Aug 2010 15:27:32 +0000 (17:27 +0200)]
Extend Bit_Length_Limb return annotation.

8 years agoExtend Bit_Length_Limb return annotation.
Reto Buerki [Wed, 18 Aug 2010 14:45:53 +0000 (14:45 +0000)]
Extend Bit_Length_Limb return annotation.

8 years agoAdd return annotation to Bit_Length_Limb function.
Reto Buerki [Wed, 18 Aug 2010 14:14:54 +0000 (14:14 +0000)]
Add return annotation to Bit_Length_Limb function.

8 years agoMake Radix_Type public.
Reto Buerki [Wed, 18 Aug 2010 14:13:46 +0000 (14:13 +0000)]
Make Radix_Type public.

8 years agoStrenghten loop assertion and add check statement.
Adrian-Ken Rueegsegger [Tue, 17 Aug 2010 13:17:31 +0000 (15:17 +0200)]
Strenghten loop assertion and add check statement.

8 years agoRename user-rule file to long_div.rlu.
Adrian-Ken Rueegsegger [Tue, 17 Aug 2010 12:58:17 +0000 (14:58 +0200)]
Rename user-rule file to long_div.rlu.

8 years agoDischarge VC related to Shift_Right_32 function.
Adrian-Ken Rueegsegger [Tue, 17 Aug 2010 12:49:04 +0000 (14:49 +0200)]
Discharge VC related to Shift_Right_32 function.

8 years agoDischarge another VC.
Adrian-Ken Rueegsegger [Tue, 17 Aug 2010 12:32:21 +0000 (14:32 +0200)]
Discharge another VC.

8 years agoRe-implement step D8 (Unnormalize).
Reto Buerki [Tue, 17 Aug 2010 10:22:34 +0000 (10:22 +0000)]
Re-implement step D8 (Unnormalize).

8 years agoUpdate Compiler_Switches in test project.
Reto Buerki [Tue, 17 Aug 2010 10:13:38 +0000 (10:13 +0000)]
Update Compiler_Switches in test project.

8 years agoRemove obsolete Big_Div procedure.
Reto Buerki [Tue, 17 Aug 2010 10:08:37 +0000 (10:08 +0000)]
Remove obsolete Big_Div procedure.

8 years agoSuppress warnings about default loop assertions.
Reto Buerki [Tue, 17 Aug 2010 10:04:33 +0000 (10:04 +0000)]
Suppress warnings about default loop assertions.

8 years agoFix Shift_Left_Plus_One implementation.
Reto Buerki [Tue, 17 Aug 2010 10:01:25 +0000 (10:01 +0000)]
Fix Shift_Left_Plus_One implementation.

8 years agoLong_Div: Make UN a Limb_Array_Plus_One array.
Reto Buerki [Mon, 16 Aug 2010 17:26:04 +0000 (17:26 +0000)]
Long_Div: Make UN a Limb_Array_Plus_One array.

Use Shift_Left_Plus_One function to normalize dividend. Improve various
loop assertions to discharge several VCs.

8 years agoLong_Div: Remove unnormalization code for now.
Reto Buerki [Mon, 16 Aug 2010 17:22:10 +0000 (17:22 +0000)]
Long_Div: Remove unnormalization code for now.

This is in preparation for the upcoming commit. UN must be of type
Limb_Array_Plus_One, there is no Short_Div for that type yet.

8 years agoAdd Shift_Left_Plus_One helper function.
Reto Buerki [Mon, 16 Aug 2010 17:13:08 +0000 (17:13 +0000)]
Add Shift_Left_Plus_One helper function.

8 years agoAdd return annotation to Shift_Right_Arithmetic.
Reto Buerki [Mon, 16 Aug 2010 17:12:03 +0000 (17:12 +0000)]
Add return annotation to Shift_Right_Arithmetic.

8 years agoFix long division assert messages.
Reto Buerki [Mon, 16 Aug 2010 16:07:05 +0000 (16:07 +0000)]
Fix long division assert messages.

8 years agoUnify limb index plus one types in private part.
Reto Buerki [Mon, 16 Aug 2010 12:29:45 +0000 (12:29 +0000)]
Unify limb index plus one types in private part.

8 years agoUse new long div procedure in division benchmark.
Adrian-Ken Rueegsegger [Fri, 13 Aug 2010 17:10:18 +0000 (19:10 +0200)]
Use new long div procedure in division benchmark.

8 years agoInitial implementation of long div according to Knuth.
Adrian-Ken Rueegsegger [Fri, 13 Aug 2010 17:09:34 +0000 (19:09 +0200)]
Initial implementation of long div according to Knuth.

8 years agoReduce word size from 32 to 16 bit.
Adrian-Ken Rueegsegger [Fri, 13 Aug 2010 17:01:16 +0000 (19:01 +0200)]
Reduce word size from 32 to 16 bit.

This is done in preparation for the long division implementation
according to Knuth, 4.3.1, algorithm D.

8 years agoUse correct loop range in Bit_Length_Limb.
Adrian-Ken Rueegsegger [Thu, 12 Aug 2010 12:26:26 +0000 (14:26 +0200)]
Use correct loop range in Bit_Length_Limb.

8 years agoUpdate test names/description.
Reto Buerki [Thu, 12 Aug 2010 12:22:04 +0000 (14:22 +0200)]
Update test names/description.

8 years agoUpdate func/proc names.
Reto Buerki [Thu, 12 Aug 2010 12:18:37 +0000 (14:18 +0200)]
Update func/proc names.

8 years agoRename Mod_Type_Size to Limb_Bit_Size.
Reto Buerki [Thu, 12 Aug 2010 12:07:09 +0000 (14:07 +0200)]
Rename Mod_Type_Size to Limb_Bit_Size.

8 years agoRename Mod_Types to Limb_Array and Data field to Limbs.
Reto Buerki [Thu, 12 Aug 2010 10:55:30 +0000 (12:55 +0200)]
Rename Mod_Types to Limb_Array and Data field to Limbs.

8 years agoRename Mod_Index to Limb_Index.
Reto Buerki [Thu, 12 Aug 2010 10:42:50 +0000 (12:42 +0200)]
Rename Mod_Index to Limb_Index.

8 years agoRename Mod_Type to Limb_Type.
Reto Buerki [Thu, 12 Aug 2010 10:30:31 +0000 (12:30 +0200)]
Rename Mod_Type to Limb_Type.

8 years agoLet Mod_Index range depend on Byte_Array length.
Reto Buerki [Thu, 12 Aug 2010 10:16:59 +0000 (12:16 +0200)]
Let Mod_Index range depend on Byte_Array length.

8 years agoAvoid temp variable in Shift_Left function.
Adrian-Ken Rueegsegger [Tue, 10 Aug 2010 14:19:42 +0000 (16:19 +0200)]
Avoid temp variable in Shift_Left function.

8 years agoAdd Min_Mod_Index function.
Adrian-Ken Rueegsegger [Tue, 10 Aug 2010 14:18:05 +0000 (16:18 +0200)]
Add Min_Mod_Index function.

8 years agoAdd benchmark for Remainder_Mod() function.
Reto Buerki [Fri, 23 Jul 2010 14:49:49 +0000 (16:49 +0200)]
Add benchmark for Remainder_Mod() function.

8 years agoAdd benchmark for Bignumber/Mod_Type multiplication.
Reto Buerki [Fri, 23 Jul 2010 14:18:13 +0000 (16:18 +0200)]
Add benchmark for Bignumber/Mod_Type multiplication.

8 years agoChange benchmark output format.
Reto Buerki [Fri, 23 Jul 2010 14:16:40 +0000 (16:16 +0200)]
Change benchmark output format.

8 years agoImplement Left (bignum) mod Right (modular type).
Reto Buerki [Fri, 23 Jul 2010 13:27:22 +0000 (15:27 +0200)]
Implement Left (bignum) mod Right (modular type).

8 years agoRemove unneeded Copy function.
Reto Buerki [Fri, 23 Jul 2010 10:13:19 +0000 (12:13 +0200)]
Remove unneeded Copy function.

8 years agoAdd Big_Unsigned_Last constant.
Reto Buerki [Fri, 23 Jul 2010 10:08:45 +0000 (12:08 +0200)]
Add Big_Unsigned_Last constant.

8 years agoChange test name of Mul_Mod_Bignums.
Reto Buerki [Fri, 23 Jul 2010 09:28:00 +0000 (11:28 +0200)]
Change test name of Mul_Mod_Bignums.

8 years agoMinor: Fix typo in bit_length_smaller_than user rule.
Reto Buerki [Fri, 23 Jul 2010 09:23:04 +0000 (11:23 +0200)]
Minor: Fix typo in bit_length_smaller_than user rule.

8 years agoImplement Big_Unsigned/Mod_Type multiplication.
Adrian-Ken Rueegsegger [Thu, 22 Jul 2010 15:53:49 +0000 (17:53 +0200)]
Implement Big_Unsigned/Mod_Type multiplication.

8 years agoAdd Bit_Length_Mod function.
Adrian-Ken Rueegsegger [Thu, 22 Jul 2010 11:57:41 +0000 (13:57 +0200)]
Add Bit_Length_Mod function.

8 years agoAdd user rule for Bit_Length and Smaller_Than relation.
Adrian-Ken Rueegsegger [Thu, 22 Jul 2010 09:47:55 +0000 (11:47 +0200)]
Add user rule for Bit_Length and Smaller_Than relation.

8 years agoUnify return annotations.
Reto Buerki [Wed, 21 Jul 2010 13:04:18 +0000 (15:04 +0200)]
Unify return annotations.

8 years agoUse 'not Less_Than' instead of 'Greater_Than'.
Reto Buerki [Wed, 21 Jul 2010 12:41:42 +0000 (14:41 +0200)]
Use 'not Less_Than' instead of 'Greater_Than'.

8 years agoAdd return annotation to Greater_Than function.
Reto Buerki [Wed, 21 Jul 2010 12:18:15 +0000 (14:18 +0200)]
Add return annotation to Greater_Than function.

8 years agoAdd benchmark for division.
Adrian-Ken Rueegsegger [Tue, 20 Jul 2010 16:35:32 +0000 (18:35 +0200)]
Add benchmark for division.

8 years agoAdd loop unrolling compiler option.
Adrian-Ken Rueegsegger [Tue, 20 Jul 2010 16:16:00 +0000 (18:16 +0200)]
Add loop unrolling compiler option.

8 years agoIgnore obj directory.
Adrian-Ken Rueegsegger [Tue, 20 Jul 2010 16:09:40 +0000 (18:09 +0200)]
Ignore obj directory.

8 years agoAdd benchmark for substraction.
Adrian-Ken Rueegsegger [Tue, 20 Jul 2010 16:08:13 +0000 (18:08 +0200)]
Add benchmark for substraction.

8 years agoAlign benchmark results.
Adrian-Ken Rueegsegger [Tue, 20 Jul 2010 16:07:09 +0000 (18:07 +0200)]
Align benchmark results.

8 years agoReturn "0" for Big_Unsigned_Zero.
Adrian-Ken Rueegsegger [Tue, 20 Jul 2010 16:06:28 +0000 (18:06 +0200)]
Return "0" for Big_Unsigned_Zero.

8 years agoAdd benchmarks for Addition and Multiplication.
Adrian-Ken Rueegsegger [Tue, 20 Jul 2010 15:52:15 +0000 (17:52 +0200)]
Add benchmarks for Addition and Multiplication.

8 years agoAdd another multiplication test.
Adrian-Ken Rueegsegger [Tue, 20 Jul 2010 15:41:53 +0000 (17:41 +0200)]
Add another multiplication test.

8 years agoAdd post condition to Set_Last_Index procedure.
Adrian-Ken Rueegsegger [Fri, 16 Jul 2010 15:12:34 +0000 (17:12 +0200)]
Add post condition to Set_Last_Index procedure.

8 years agoFix Set_Last_Index quantification annotation.
Adrian-Ken Rueegsegger [Fri, 16 Jul 2010 14:40:31 +0000 (16:40 +0200)]
Fix Set_Last_Index quantification annotation.

8 years agoAdd user-defined rule for Big_Div procedure.
Adrian-Ken Rueegsegger [Fri, 16 Jul 2010 14:26:14 +0000 (16:26 +0200)]
Add user-defined rule for Big_Div procedure.

8 years agoConvert files from dos to unix format.
Adrian-Ken Rueegsegger [Fri, 16 Jul 2010 13:22:13 +0000 (15:22 +0200)]
Convert files from dos to unix format.

8 years agoFinalize Big_Div implementation.
Reto Buerki [Fri, 16 Jul 2010 12:29:01 +0000 (14:29 +0200)]
Finalize Big_Div implementation.

8 years agoAdd quantification rule file (by Ian O'Neill).
Reto Buerki [Fri, 16 Jul 2010 12:22:47 +0000 (14:22 +0200)]
Add quantification rule file (by Ian O'Neill).

8 years agoFix quantification range in Less_Than function.
Reto Buerki [Fri, 16 Jul 2010 12:19:37 +0000 (14:19 +0200)]
Fix quantification range in Less_Than function.

8 years agoAdd Big_Unsigned_Two constant.
Reto Buerki [Fri, 16 Jul 2010 10:13:54 +0000 (12:13 +0200)]
Add Big_Unsigned_Two constant.

8 years agoAdd test for Short_Div() function.
Reto Buerki [Fri, 16 Jul 2010 09:57:15 +0000 (11:57 +0200)]
Add test for Short_Div() function.

8 years agoImplement bignumber Shift_Left function.
Reto Buerki [Fri, 16 Jul 2010 09:28:30 +0000 (11:28 +0200)]
Implement bignumber Shift_Left function.

8 years agoCreate POGS summary in toplevel directory.
Reto Buerki [Thu, 15 Jul 2010 14:03:09 +0000 (16:03 +0200)]
Create POGS summary in toplevel directory.

8 years agoSet SPARK_DIR only if it is not already set.
Reto Buerki [Thu, 15 Jul 2010 13:51:53 +0000 (15:51 +0200)]
Set SPARK_DIR only if it is not already set.

8 years agoUse sparksimp's multiprocessing option.
Adrian-Ken Rueegsegger [Thu, 15 Jul 2010 13:47:52 +0000 (15:47 +0200)]
Use sparksimp's multiprocessing option.

8 years agoTighten loop assertion of Set_Last_Index procedure.
Adrian-Ken Rueegsegger [Thu, 15 Jul 2010 12:47:14 +0000 (14:47 +0200)]
Tighten loop assertion of Set_Last_Index procedure.

8 years agoAdd for all quantification to loop in Less_Than.
Adrian-Ken Rueegsegger [Thu, 15 Jul 2010 10:10:29 +0000 (12:10 +0200)]
Add for all quantification to loop in Less_Than.

8 years agoAdd Copy function as quantification example.
Adrian-Ken Rueegsegger [Thu, 15 Jul 2010 09:35:45 +0000 (11:35 +0200)]
Add Copy function as quantification example.

8 years agoSub: Avoid copy of loop boundary to local variable.
Adrian-Ken Rueegsegger [Wed, 14 Jul 2010 13:13:46 +0000 (15:13 +0200)]
Sub: Avoid copy of loop boundary to local variable.

8 years agoAdd partial implementation of bignumber division.
Reto Buerki [Wed, 14 Jul 2010 10:25:12 +0000 (12:25 +0200)]
Add partial implementation of bignumber division.

8 years agoExtend return annotation of Less_Than() function.
Reto Buerki [Wed, 14 Jul 2010 10:24:13 +0000 (12:24 +0200)]
Extend return annotation of Less_Than() function.

8 years agoFix Greater_Than() implementation.
Reto Buerki [Wed, 14 Jul 2010 10:00:01 +0000 (12:00 +0200)]
Fix Greater_Than() implementation.

8 years agoAdd return annotations for shadowed shift functions.
Reto Buerki [Tue, 13 Jul 2010 15:17:27 +0000 (17:17 +0200)]
Add return annotations for shadowed shift functions.

8 years agoCopy user rule files to output directory.
Reto Buerki [Tue, 13 Jul 2010 14:21:35 +0000 (16:21 +0200)]
Copy user rule files to output directory.

8 years agoAdd user rule file for Short_Div (by Ian O'Neill).
Reto Buerki [Tue, 13 Jul 2010 14:11:31 +0000 (16:11 +0200)]
Add user rule file for Short_Div (by Ian O'Neill).

8 years agoMul: Use double sized Mod_Types array in loop.
Reto Buerki [Tue, 13 Jul 2010 09:33:25 +0000 (11:33 +0200)]
Mul: Use double sized Mod_Types array in loop.

This is needed because we cannot (yet) prove that our precondition
guarantees that (I + J) is within Mod_Index range.

8 years agoMinor: Fix indentation in Add() function.
Reto Buerki [Tue, 13 Jul 2010 09:29:56 +0000 (11:29 +0200)]
Minor: Fix indentation in Add() function.

8 years agoLoop until Left.Last_Index in Sub function.
Adrian-Ken Rueegsegger [Mon, 12 Jul 2010 14:08:05 +0000 (16:08 +0200)]
Loop until Left.Last_Index in Sub function.

8 years agoAdd return annotation to Less_Than() function.
Reto Buerki [Mon, 12 Jul 2010 10:36:58 +0000 (12:36 +0200)]
Add return annotation to Less_Than() function.

8 years agoRemove 'assert True' assertions with specific ones.
Reto Buerki [Mon, 12 Jul 2010 09:48:21 +0000 (11:48 +0200)]
Remove 'assert True' assertions with specific ones.

8 years agoSimplify loop range statements.
Reto Buerki [Mon, 12 Jul 2010 09:36:44 +0000 (11:36 +0200)]
Simplify loop range statements.

8 years agoSPARKFormat big_numbers.ads file.
Reto Buerki [Tue, 6 Jul 2010 16:16:46 +0000 (18:16 +0200)]
SPARKFormat big_numbers.ads file.