12.1. Only use certified subset¶

Identifier: CORE_CSTR_0010_SUBSET¶

Associated requirement ID: CORE_AVD_SUBSET_001.

The user shall only use the certified subset of the core library.

12.2. Compile with panic abort¶

Identifier: CORE_CSTR_0020_PANIC_ABORT¶

Associated requirement ID: CORE_AVD_SUBSET_001.

The user shall always provide the -C panic=abort option to rustc.

12.3. Only use stable functions¶

Identifier: CORE_CSTR_0030_SUBSET_ONLY_STABLE¶

Associated requirement ID: CORE_AVD_SUBSET_001.

The user shall not use experimental functions in the certified subset of the core library.

12.4. Use matching version of the core library and rustc¶

Identifier: CORE_CSTR_0040_MATCHING_VERSION¶

Associated requirement ID: CORE_AVD_SUBSET_001.

The user shall verify that the version of the core library and the version of rustc used to compile code match. This is ensured by following the Installation Procedures.

12.5. Review operands¶

Identifier: CORE_CSTR_0050_REVIEW_OPERANDS¶

Associated requirement ID: CORE_AVD_SUBSET_001.

The user shall manually verify that the implementations for operators they use in their source code are certified. They have to check all occurrences of operands listed in the core::ops module. For each occurrence, they have to check that the implementation for the combination of types is certified.

For example, there are many implementations for addition (trait Add).

One of those implementations could be certified, e.g. impl Add<i32> for i32. This would mean that it is legal in certified contexts to add two i32 s to each other.

Another implementation could be uncertified, e.g. impl Add<i64> for i64. This would mean that it is not legal in certified contexts to add two i64 s to each other.

Therefore, the source code has to be reviewed for all syntax that denotes an operator. The source code also has to be verified that the implementation of that operator, for that combination of types, is certified.

// this is in the core library:

trait Add<Rhs = Self> {
    type Output;
    const fn add(self, rhs: Rhs) -> Self::Output;
}

impl Add<i32> for i32 { /* ... */ } // certified
impl Add<i64> for i64 { /* ... */ } // uncertified

// this is in user code:

let a = 5_i32 + 10_i32; // legal
let b = 20_i64 + 40_i64; // illegal

12.6. Verify macro correctness¶

Identifier: CORE_CSTR_0060_VERIFY_MACROS¶

Associated requirement ID: CORE_AVD_MACROS_002.

The user shall verify that all code generated by macros is correct.