Skip to content

Commit ab87498

Browse files
hanno-beckerhanno-becker
authored
Merge pull request #367 from pq-code-package/cbmc-polyvec-compress
CBMC: Spec + proof `polyvec_[de]compress`
2 parents 761a7ca + 9bfa91b commit ab87498

22 files changed

+619
-79
lines changed

‎cbmc/proofs/polyvec_compress/Makefile

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = polyvec_compress_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = polyvec_compress
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c
20+
21+
CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_compress
22+
USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d10 $(MLKEM_NAMESPACE)scalar_compress_d11
23+
APPLY_LOOP_CONTRACTS=on
24+
USE_DYNAMIC_FRAMES=1
25+
26+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
27+
EXTERNAL_SAT_SOLVER=
28+
CBMCFLAGS=--smt2
29+
30+
FUNCTION_NAME = $(MLKEM_NAMESPACE)polyvec_compress
31+
32+
# If this proof is found to consume huge amounts of RAM, you can set the
33+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
34+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
35+
# documentation in Makefile.common under the "Job Pools" heading for details.
36+
# EXPENSIVE = true
37+
38+
# This function is large enough to need...
39+
CBMC_OBJECT_BITS = 10
40+
41+
# If you require access to a file-local ("static") function or object to conduct
42+
# your proof, set the following (and do not include the original source file
43+
# ("mlkem/poly.c") in PROJECT_SOURCES).
44+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
45+
# include ../Makefile.common
46+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
49+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
50+
# be set before including Makefile.common, but any use of variables on the
51+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
52+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
53+
54+
include ../Makefile.common

‎cbmc/proofs/polyvec_compress/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

‎cbmc/proofs/polyvec_compress/cbmc-viewer.json

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
{ "expected-missing-functions":
2+
[
3+
4+
],
5+
"proof-name": "poly_compress",
6+
"proof-root": "cbmc/proofs"
7+
}

‎cbmc/proofs/polyvec_compress/polyvec_compress_harness.c

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: MIT-0 AND Apache-2.0
3+
4+
/*
5+
* Insert copyright notice
6+
*/
7+
8+
/**
9+
* @file polyvec_compress_harness.c
10+
* @brief Implements the proof harness for polyvec_compress function.
11+
*/
12+
#include "poly.h"
13+
#include "polyvec.h"
14+
15+
/*
16+
* Insert project header files that
17+
* - include the declaration of the function
18+
* - include the types needed to declare function arguments
19+
*/
20+
21+
/**
22+
* @brief Starting point for formal analysis
23+
*
24+
*/
25+
void harness(void) {
26+
polyvec *r;
27+
uint8_t *a;
28+
29+
// TODO: remove cbmc-viewer.json
30+
// TODO: remove the README for all proofs
31+
32+
polyvec_compress(a, r);
33+
}

‎cbmc/proofs/polyvec_decompress/Makefile

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = polyvec_decompress_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = polyvec_decompress
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c
20+
21+
CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_decompress
22+
23+
ifeq ($(MLKEM_K),4)
24+
USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d11
25+
else
26+
USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d10
27+
endif
28+
APPLY_LOOP_CONTRACTS=on
29+
USE_DYNAMIC_FRAMES=1
30+
31+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
32+
EXTERNAL_SAT_SOLVER=
33+
CBMCFLAGS=--smt2
34+
35+
FUNCTION_NAME = $(MLKEM_NAMESPACE)polyvec_decompress
36+
37+
# If this proof is found to consume huge amounts of RAM, you can set the
38+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
39+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
40+
# documentation in Makefile.common under the "Job Pools" heading for details.
41+
# EXPENSIVE = true
42+
43+
# This function is large enough to need...
44+
CBMC_OBJECT_BITS = 10
45+
46+
# If you require access to a file-local ("static") function or object to conduct
47+
# your proof, set the following (and do not include the original source file
48+
# ("mlkem/poly.c") in PROJECT_SOURCES).
49+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
50+
# include ../Makefile.common
51+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
52+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
53+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
54+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
55+
# be set before including Makefile.common, but any use of variables on the
56+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
57+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
58+
59+
include ../Makefile.common

‎cbmc/proofs/polyvec_decompress/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

‎cbmc/proofs/polyvec_decompress/cbmc-viewer.json

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
{ "expected-missing-functions":
2+
[
3+
4+
],
5+
"proof-name": "poly_compress",
6+
"proof-root": "cbmc/proofs"
7+
}

‎cbmc/proofs/polyvec_decompress/polyvec_decompress_harness.c

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: MIT-0 AND Apache-2.0
3+
4+
/*
5+
* Insert copyright notice
6+
*/
7+
8+
/**
9+
* @file polyvec_decompress_harness.c
10+
* @brief Implements the proof harness for polyvec_decompress function.
11+
*/
12+
#include "poly.h"
13+
#include "polyvec.h"
14+
15+
/*
16+
* Insert project header files that
17+
* - include the declaration of the function
18+
* - include the types needed to declare function arguments
19+
*/
20+
21+
/**
22+
* @brief Starting point for formal analysis
23+
*
24+
*/
25+
void harness(void) {
26+
polyvec *a;
27+
uint8_t *r;
28+
29+
// TODO: remove cbmc-viewer.json
30+
// TODO: remove the README for all proofs
31+
32+
polyvec_decompress(a, r);
33+
}

‎cbmc/proofs/scalar_decompress_d10/Makefile

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = scalar_decompress_d10_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = scalar_decompress_d10
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
20+
21+
CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d10
22+
USE_FUNCTION_CONTRACTS=
23+
APPLY_LOOP_CONTRACTS=on
24+
USE_DYNAMIC_FRAMES=1
25+
26+
# SMT backend for proving with contracts and quantifiers
27+
# To be re-enabled when CBMC Issue #8303 is fixed.
28+
# CBMCFLAGS=--smt2
29+
30+
# Uncomment this to see what commands litani is running...
31+
#VERBOSE=on
32+
33+
# If this proof is found to consume huge amounts of RAM, you can set the
34+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
35+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
36+
# documentation in Makefile.common under the "Job Pools" heading for details.
37+
# EXPENSIVE = true
38+
39+
# If you require access to a file-local ("static") function or object to conduct
40+
# your proof, set the following (and do not include the original source file
41+
# ("mlkem/poly.c") in PROJECT_SOURCES).
42+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
43+
# include ../Makefile.common
44+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
45+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
46+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
47+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
48+
# be set before including Makefile.common, but any use of variables on the
49+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
50+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
51+
52+
include ../Makefile.common

‎cbmc/proofs/scalar_decompress_d10/README.md

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
scalar_decompress_q_16 proof
4+
==============
5+
6+
This directory contains a memory safety proof for scalar_decompress_q_16.
7+
8+
To run the proof.
9+
-------------
10+
* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer.
11+
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
12+
to your path.
13+
* Run `make`.
14+
* Open `report/html/index.html` in a web browser.

‎cbmc/proofs/scalar_decompress_d10/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

‎cbmc/proofs/scalar_decompress_d10/cbmc-viewer.json

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
{ "expected-missing-functions":
2+
[
3+
4+
],
5+
"proof-name": "scalar_decompress_d10",
6+
"proof-root": "cbmc/proofs"
7+
}

‎cbmc/proofs/scalar_decompress_d10/scalar_decompress_d10_harness.c

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: MIT-0
3+
4+
/*
5+
* Insert copyright notice
6+
*/
7+
8+
/**
9+
* @file scalar_decompress_d10_harness.c
10+
* @brief Implements the proof harness for scalar_decompress_d10 function.
11+
*/
12+
13+
/*
14+
* Insert project header files that
15+
* - include the declaration of the function
16+
* - include the types needed to declare function arguments
17+
*/
18+
#include <poly.h>
19+
20+
/**
21+
* @brief Starting point for formal analysis
22+
*
23+
*/
24+
void harness(void) {
25+
uint32_t u;
26+
uint16_t d;
27+
d = scalar_decompress_d10(u);
28+
}

‎cbmc/proofs/scalar_decompress_d11/Makefile

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = scalar_decompress_d11_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = scalar_decompress_d11
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
20+
21+
CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_d11
22+
USE_FUNCTION_CONTRACTS=
23+
APPLY_LOOP_CONTRACTS=on
24+
USE_DYNAMIC_FRAMES=1
25+
26+
# SMT backend for proving with contracts and quantifiers
27+
# To be re-enabled when CBMC Issue #8303 is fixed.
28+
# CBMCFLAGS=--smt2
29+
30+
# Uncomment this to see what commands litani is running...
31+
#VERBOSE=on
32+
33+
# If this proof is found to consume huge amounts of RAM, you can set the
34+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
35+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
36+
# documentation in Makefile.common under the "Job Pools" heading for details.
37+
# EXPENSIVE = true
38+
39+
# If you require access to a file-local ("static") function or object to conduct
40+
# your proof, set the following (and do not include the original source file
41+
# ("mlkem/poly.c") in PROJECT_SOURCES).
42+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
43+
# include ../Makefile.common
44+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
45+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
46+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
47+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
48+
# be set before including Makefile.common, but any use of variables on the
49+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
50+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
51+
52+
include ../Makefile.common

‎cbmc/proofs/scalar_decompress_d11/README.md

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
scalar_decompress_q_16 proof
4+
==============
5+
6+
This directory contains a memory safety proof for scalar_decompress_q_16.
7+
8+
To run the proof.
9+
-------------
10+
* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer.
11+
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
12+
to your path.
13+
* Run `make`.
14+
* Open `report/html/index.html` in a web browser.

‎cbmc/proofs/scalar_decompress_d11/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

‎cbmc/proofs/scalar_decompress_d11/cbmc-viewer.json

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
{ "expected-missing-functions":
2+
[
3+
4+
],
5+
"proof-name": "scalar_decompress_d4",
6+
"proof-root": "cbmc/proofs"
7+
}

0 commit comments

Comments
 (0)