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

actuator_cryp <- cryptol_load "../models/RTS/Actuator.cry";
actuator_gen  <- llvm_load_module "generated/actuator_impl.bc";

let actuate_actuator_ref = {{ actuator_cryp::ActuateActuator }};

let actuate_actuator_spec = do {
  input <- llvm_fresh_var "inp" (llvm_int 8);
  let expected = {{ (zero # [actuate_actuator_ref (take (reverse input))]) : [8] }};
  llvm_execute_func [llvm_term input];
  llvm_return (llvm_term expected);
};

llvm_verify actuator_gen "ActuateActuator" [] false actuate_actuator_spec z3;