Skip to content

Commit 554df0c

Browse files
jeffspel-cryptodryercashewSteveMaier-IRT
authored
Lookup table mont (#265)
* new montgomery code * Add Hacl code to support using Lookup_Table table entries in Montgomery form. * Add a newline to the end of Hacl_GenericField64.h * Removed the checks from the push path, only doing the pull_requests * new Karamel version of HACL * Changes for the merge * Fixed header issue * Add calls for the GetStatus to update the current status * changed alloca call to malloca call to resolve issue with Code Scanner * add constructor to API for testing. * moved the allocation outside the for loops for the code checker * Fixed comments on PR Co-authored-by: Jeff <spelmaa@wwu.edu> Co-authored-by: SteveMaier-IRT <steve.maier@infernored.com> Co-authored-by: Steve Maier <82616727+SteveMaier-IRT@users.noreply.github.com>
1 parent 7165e78 commit 554df0c

78 files changed

Lines changed: 6342 additions & 3454 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/pull-request.yml‎

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,6 @@ name: Pull Request
22

33
on:
44
workflow_dispatch:
5-
push:
6-
paths:
7-
- "apps/**"
8-
- "bindings/**"
9-
- "include/**"
10-
- "src/**"
11-
- "test/**"
12-
branches: [main]
135
pull_request:
146
paths:
157
- ".github/**"

‎bindings/netstandard/ElectionGuard/ElectionGuard.Encryption/PrecomputeAPI.cs‎

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,16 +106,29 @@ public interface IPrecomputeAPI
106106
/// </summary>
107107
public class Precompute : IPrecomputeAPI
108108
{
109+
readonly static int DUMMY_BUFFER_SIZE = 100; // set a buffer size that will be > 0 and < the default of 5000 for initialization
110+
readonly int INIT_COUNT = -1; // initializer for count to make sure we are getting a value back from the C++
111+
readonly int INIT_QUEUE_SIZE = -2; // initializer for the queue size to make sure that its diffrent than the count and being set
112+
109113
AutoResetEvent waitHandle;
110114

115+
/// <summary>
116+
/// Default constructor to initialize buffers for testing
117+
/// </summary>
118+
public Precompute()
119+
{
120+
NativePrecomputeBuffers.Init(max_buffers);
121+
}
122+
123+
111124
private PrecomputeStatus currentStatus = new PrecomputeStatus
112125
{
113126
Percentage = 0,
114127
CompletedExponentiationsCount = 0,
115128
CurrentState = PrecomputeState.NotStarted
116129
};
117130
private Thread workerThread;
118-
private int max_buffers = 0; // zero will say to run to a default number of runs
131+
private int max_buffers = DUMMY_BUFFER_SIZE;
119132
private ElementModP elgamalPublicKey;
120133

121134
/// <summary>
@@ -150,6 +163,14 @@ private void OnProgressEvent()
150163
/// <returns><see cref="PrecomputeStatus">PrecomputeStatus</see> with all of the latest information</returns>
151164
public PrecomputeStatus GetStatus()
152165
{
166+
int count = INIT_COUNT;
167+
int queue_size = INIT_QUEUE_SIZE;
168+
GetProgress(out count, out queue_size);
169+
if (count == queue_size)
170+
currentStatus.CurrentState = PrecomputeState.Completed;
171+
currentStatus.Percentage = (double)count / queue_size;
172+
currentStatus.CompletedExponentiationsCount = count;
173+
153174
return currentStatus;
154175
}
155176

include/FStar_UInt128.h renamed to include/karamel/FStar_UInt128.h

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,16 @@
66

77
#ifndef __FStar_UInt128_H
88
#define __FStar_UInt128_H
9-
#include <inttypes.h>
10-
#include <stdbool.h>
11-
#include "kremlin/internal/compat.h"
12-
#include "kremlin/lowstar_endianness.h"
13-
#include "kremlin/internal/types.h"
14-
#include "kremlin/internal/target.h"
159

1610

1711

1812

13+
#include <inttypes.h>
14+
#include <stdbool.h>
15+
#include "krml/internal/compat.h"
16+
#include "krml/lowstar_endianness.h"
17+
#include "krml/internal/types.h"
18+
#include "krml/internal/target.h"
1919
static inline FStar_UInt128_uint128
2020
FStar_UInt128_add(FStar_UInt128_uint128 a, FStar_UInt128_uint128 b);
2121

include/FStar_UInt128_Verified.h renamed to include/karamel/FStar_UInt128_Verified.h

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,14 @@
66

77
#ifndef __FStar_UInt128_Verified_H
88
#define __FStar_UInt128_Verified_H
9-
#include <inttypes.h>
10-
#include <stdbool.h>
11-
#include "kremlin/internal/types.h"
12-
#include "kremlin/internal/target.h"
139

1410

15-
#include "FStar_UInt_8_16_32_64.h"
1611

12+
#include "FStar_UInt_8_16_32_64.h"
13+
#include <inttypes.h>
14+
#include <stdbool.h>
15+
#include "krml/internal/types.h"
16+
#include "krml/internal/target.h"
1717
static inline uint64_t FStar_UInt128_constant_time_carry(uint64_t a, uint64_t b)
1818
{
1919
return (a ^ ((a ^ b) | ((a - b) ^ b))) >> (uint32_t)63U;

include/FStar_UInt_8_16_32_64.h renamed to include/karamel/FStar_UInt_8_16_32_64.h

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,16 @@
66

77
#ifndef __FStar_UInt_8_16_32_64_H
88
#define __FStar_UInt_8_16_32_64_H
9-
#include <inttypes.h>
10-
#include <stdbool.h>
11-
#include "kremlin/internal/compat.h"
12-
#include "kremlin/lowstar_endianness.h"
13-
#include "kremlin/internal/types.h"
14-
#include "kremlin/internal/target.h"
159

1610

1711

1812

13+
#include <inttypes.h>
14+
#include <stdbool.h>
15+
#include "krml/internal/compat.h"
16+
#include "krml/lowstar_endianness.h"
17+
#include "krml/internal/types.h"
18+
#include "krml/internal/target.h"
1919
extern Prims_int FStar_UInt64_n;
2020

2121
extern bool FStar_UInt64_uu___is_Mk(uint64_t projectee);
@@ -26,6 +26,10 @@ extern Prims_int FStar_UInt64_v(uint64_t x);
2626

2727
extern uint64_t FStar_UInt64_uint_to_t(Prims_int x);
2828

29+
extern uint64_t FStar_UInt64_zero;
30+
31+
extern uint64_t FStar_UInt64_one;
32+
2933
extern uint64_t FStar_UInt64_minus(uint64_t a);
3034

3135
extern uint32_t FStar_UInt64_n_minus_one;
@@ -70,6 +74,10 @@ extern Prims_int FStar_UInt32_v(uint32_t x);
7074

7175
extern uint32_t FStar_UInt32_uint_to_t(Prims_int x);
7276

77+
extern uint32_t FStar_UInt32_zero;
78+
79+
extern uint32_t FStar_UInt32_one;
80+
7381
extern uint32_t FStar_UInt32_minus(uint32_t a);
7482

7583
extern uint32_t FStar_UInt32_n_minus_one;
@@ -114,6 +122,10 @@ extern Prims_int FStar_UInt16_v(uint16_t x);
114122

115123
extern uint16_t FStar_UInt16_uint_to_t(Prims_int x);
116124

125+
extern uint16_t FStar_UInt16_zero;
126+
127+
extern uint16_t FStar_UInt16_one;
128+
117129
extern uint16_t FStar_UInt16_minus(uint16_t a);
118130

119131
extern uint32_t FStar_UInt16_n_minus_one;
@@ -158,6 +170,10 @@ extern Prims_int FStar_UInt8_v(uint8_t x);
158170

159171
extern uint8_t FStar_UInt8_uint_to_t(Prims_int x);
160172

173+
extern uint8_t FStar_UInt8_zero;
174+
175+
extern uint8_t FStar_UInt8_one;
176+
161177
extern uint8_t FStar_UInt8_minus(uint8_t a);
162178

163179
extern uint32_t FStar_UInt8_n_minus_one;

include/LowStar_Endianness.h renamed to include/karamel/LowStar_Endianness.h

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,16 @@
66

77
#ifndef __LowStar_Endianness_H
88
#define __LowStar_Endianness_H
9-
#include <inttypes.h>
10-
#include <stdbool.h>
11-
#include "kremlin/internal/compat.h"
12-
#include "kremlin/lowstar_endianness.h"
13-
#include "kremlin/internal/types.h"
14-
#include "kremlin/internal/target.h"
159

1610

17-
#include "FStar_UInt128.h"
1811

12+
#include "FStar_UInt128.h"
13+
#include <inttypes.h>
14+
#include <stdbool.h>
15+
#include "krml/internal/compat.h"
16+
#include "krml/lowstar_endianness.h"
17+
#include "krml/internal/types.h"
18+
#include "krml/internal/target.h"
1919
static inline void store128_le(uint8_t *x0, FStar_UInt128_uint128 x1);
2020

2121
static inline FStar_UInt128_uint128 load128_le(uint8_t *x0);

‎include/karamel/Makefile.basic‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
# A basic Makefile that KaRaMeL copies in the output directory; this is not
2+
# guaranteed to work and will only work well for very simple projects. This
3+
# Makefile uses:
4+
# - the custom C files passed to your krml invocation
5+
# - the custom C flags passed to your krml invocation
6+
# - the -o option passed to your krml invocation
7+
8+
include Makefile.include
9+
10+
ifeq (,$(KRML_HOME))
11+
$(error please define KRML_HOME to point to the root of your KaRaMeL git checkout)
12+
endif
13+
14+
CFLAGS += -I. -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/minimal
15+
CFLAGS += -Wall -Wextra -Werror -std=c11 -Wno-unused-variable \
16+
-Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-function \
17+
-Wno-unused-parameter -Wno-infinite-recursion \
18+
-g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE
19+
ifeq ($(OS),Windows_NT)
20+
CFLAGS += -D__USE_MINGW_ANSI_STDIO
21+
else
22+
CFLAGS += -fPIC
23+
endif
24+
CFLAGS += $(USER_CFLAGS)
25+
26+
SOURCES += $(ALL_C_FILES) $(USER_C_FILES)
27+
ifneq (,$(BLACKLIST))
28+
SOURCES := $(filter-out $(BLACKLIST),$(SOURCES))
29+
endif
30+
OBJS += $(patsubst %.c,%.o,$(SOURCES))
31+
32+
all: $(USER_TARGET)
33+
34+
$(USER_TARGET): $(OBJS)
35+
36+
AR ?= ar
37+
38+
%.a:
39+
$(AR) cr $@ $^
40+
41+
%.exe:
42+
$(CC) $(CFLAGS) -o $@ $^ $(KRML_HOME)/krmllib/dist/generic/libkrmllib.a
43+
44+
%.so:
45+
$(CC) $(CFLAGS) -shared -o $@ $^
46+
47+
%.d: %.c
48+
@set -e; rm -f $@; \
49+
$(CC) -MM $(CFLAGS) $< > $@.$$$$; \
50+
sed 's,\($(notdir $*)\)\.o[ :]*,$(dir $@)\1.o $@ : ,g' < $@.$$$$ > $@; \
51+
rm -f $@.$$$$
52+
53+
include $(patsubst %.c,%.d,$(SOURCES))
54+
55+
clean:
56+
rm -rf *.o *.d $(USER_TARGET)

‎include/karamel/Makefile.include‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
USER_TARGET=libkrmllib.a
2+
USER_CFLAGS=
3+
USER_C_FILES=fstar_uint128.c
4+
ALL_C_FILES=
5+
ALL_H_FILES=FStar_UInt128.h FStar_UInt_8_16_32_64.h LowStar_Endianness.h

include/fstar_uint128_gcc64.h renamed to include/karamel/fstar_uint128_gcc64.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@
1616
* FStar.UInt128 to avoid a maze of preprocessor guards and hand-written code.
1717
* */
1818

19-
/* This file is used for both the minimal and generic kremlib distributions. As
19+
/* This file is used for both the minimal and generic krmllib distributions. As
2020
* such, it assumes that the machine integers have been bundled the exact same
2121
* way in both cases. */
2222

include/fstar_uint128_msvc.h renamed to include/karamel/fstar_uint128_msvc.h

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,17 @@
11
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
22
Licensed under the Apache 2.0 License. */
33

4-
/* This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
5-
* then hand-edited to use MSVC intrinsics KreMLin invocation:
6-
* C:\users\barrybo\mitls2c\kremlin\_build\src\Kremlin.native -minimal -fnouint128 C:/users/barrybo/mitls2c/FStar/ulib/FStar.UInt128.fst -tmpdir ../secure_api/out/runtime_switch/uint128 -skip-compilation -add-include "kremlib0.h" -drop FStar.Int.Cast.Full -bundle FStar.UInt128=FStar.*,Prims
4+
/* This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
5+
* then hand-edited to use MSVC intrinsics KaRaMeL invocation:
6+
* C:\users\barrybo\mitls2c\karamel\_build\src\Karamel.native -minimal -fnouint128 C:/users/barrybo/mitls2c/FStar/ulib/FStar.UInt128.fst -tmpdir ../secure_api/out/runtime_switch/uint128 -skip-compilation -add-include "krmllib0.h" -drop FStar.Int.Cast.Full -bundle FStar.UInt128=FStar.*,Prims
77
* F* version: 15104ff8
8-
* KreMLin version: 318b7fa8
8+
* KaRaMeL version: 318b7fa8
99
*/
1010

1111
#ifndef FSTAR_UINT128_MSVC
1212
#define FSTAR_UINT128_MSVC
1313

14-
#include "kremlin/internal/types.h"
14+
#include "krml/internal/types.h"
1515
#include "FStar_UInt128.h"
1616
#include "FStar_UInt_8_16_32_64.h"
1717

@@ -448,9 +448,9 @@ inline static FStar_UInt128_uint128 FStar_UInt128_mul32(uint64_t x, uint32_t y)
448448
}
449449

450450
/* Note: static headers bring scope collision issues when they define types!
451-
* Because now client (kremlin-generated) code will include this header and
451+
* Because now client (karamel-generated) code will include this header and
452452
* there might be type collisions if the client code uses quadruples of uint64s.
453-
* So, we cannot use the kremlin-generated name. */
453+
* So, we cannot use the karamel-generated name. */
454454
typedef struct K_quad_s {
455455
uint64_t fst;
456456
uint64_t snd;

0 commit comments

Comments
 (0)