instrumentation.saw

// HARDENS Reactor Trip System (RTS) Assurance Case
// In support of a formal model of RTS system behavior written in the
// Cryptol DSL, verifying the implementation of the RTS, genenerated
// from Cryptol, and hand-written, in both Verilog and C.
//
// @author Alex Bakst <abakst@galois.com>
// @created November, 2021

// Copyright 2021, 2022, 2023 Galois, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

include "common.saw";
enable_experimental;

cryptol_add_path "../models";

instrumentation_cryp <- cryptol_load "../models/RTS/InstrumentationUnit.cry";
instrumentation_gen  <- llvm_load_module "generated/instrumentation_impl.bc";
instrumentation_hand <- llvm_load_module "handwritten/instrumentation_impl.bc";

let is_ch_tripped_ref = {{ instrumentation_cryp::Is_Ch_Tripped }};
write_verilog "Is_Ch_Tripped.v" is_ch_tripped_ref;

let generate_sensor_trips_ref = {{ instrumentation_cryp::Generate_Sensor_Trips }};
write_verilog "Generate_Sensor_Trips.v" generate_sensor_trips_ref;

let is_ch_tripped_spec = do {
    mode           <- llvm_fresh_var "mode" (llvm_int 8);
    sensor_tripped <- llvm_fresh_var "sensor_tripped" (llvm_int 8);
    llvm_precond {{ elem mode [0, 1, 2] }};
    llvm_precond {{ elem sensor_tripped [0, 1] }};
    llvm_execute_func [llvm_term mode, llvm_term sensor_tripped];
    let expected = {{ (zero # [is_ch_tripped_ref (drop mode) (0 != sensor_tripped)]) : [8] }};
    llvm_return (llvm_term expected);
};

let generate_sensor_trips_spec = do {
    (vals, ptr_vals)            <- ptr_to_fresh "vals" (llvm_array 3 (llvm_int 32));
    (setpoints, ptr_setpoints)  <- ptr_to_fresh "setpoints" (llvm_array 3 (llvm_int 32));
    llvm_precond {{ (vals @ instrumentation_cryp::S) < 0x80000000 }};
    llvm_execute_func [ptr_vals, ptr_setpoints];
    let reference_val = {{ generate_sensor_trips_ref vals setpoints }};
    let expected      = {{ (zero # reverse reference_val) : [8] }};
    llvm_return (llvm_term expected);
};

llvm_verify instrumentation_gen "Is_Ch_Tripped" [] false is_ch_tripped_spec z3;
llvm_verify instrumentation_hand "Is_Ch_Tripped" [] false is_ch_tripped_spec z3;
llvm_verify instrumentation_gen "Generate_Sensor_Trips" [] false generate_sensor_trips_spec z3;
llvm_verify instrumentation_hand "Generate_Sensor_Trips" [] false generate_sensor_trips_spec z3;