actuation_unit.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";

cryptol_add_path "../models";

actuate_unit_cryp <- cryptol_load "../models/RTS/ActuationUnit.cry";
actuate_unit_gen  <- llvm_load_module "generated/actuation_unit_impl.bc";

let actuate_d0_ref = {{ actuate_unit_cryp::Actuate_D0 }};
let actuate_d1_ref = {{ actuate_unit_cryp::Actuate_D1 }};

let actuate_d_spec f = do {
    (trips, ptr_trips) <- ptr_to_fresh "trips" (llvm_array 3 (llvm_array 4 (llvm_int 8)));
    old_trip           <- llvm_fresh_var "old" (llvm_int 8);
    llvm_precond {{ (old_trip == 0) || (old_trip == 1) }};
    llvm_execute_func [ptr_trips, llvm_term old_trip];
    let expected = {{ (zero # [f trips (0 != old_trip)]) : [8] }};
    llvm_return (llvm_term expected);
};

let actuate_d0 = actuate_d_spec actuate_d0_ref;
let actuate_d1 = actuate_d_spec actuate_d1_ref;

llvm_verify actuate_unit_gen "Actuate_D0" [] false actuate_d0 z3;
llvm_verify actuate_unit_gen "Actuate_D1" [] false actuate_d1 z3;