diff --git a/src/security_block.ml b/src/security_block.ml index 2deab74..ba344b8 100644 --- a/src/security_block.ml +++ b/src/security_block.ml @@ -1,23 +1,23 @@ (* security_block.ml - Top-level security block integration - + Implements the embedded off-switch architecture from Petrie's paper. - + Components: - TRNG submodule for nonce generation - ECDSA submodule for license verification - Inline usage allowance counter - Inline workload with output gating - + State machine: - Requests nonce from TRNG at initialization - Publishes nonce for external license generation - Verifies received licenses via ECDSA - Increments allowance on valid license, then generates new nonce - On invalid license, returns to Publish with same nonce - + Workload output is gated by ANDing each bit with (allowance > 0). Allowance decrements every clock cycle (time-based authorization). - + Note: The Int8 Add workload is an example. In production, this would be replaced with actual essential chip operations (e.g., matrix multiply units, data routing logic). @@ -83,18 +83,17 @@ module State = struct | Publish | Verify_start | Verify_wait - | Update - [@@deriving sexp_of, compare, enumerate] + [@@deriving sexp_of, compare, equal, enumerate] end let create scope (i : _ I.t) = let open Always in let spec = Reg_spec.create ~clock:i.clock ~clear:i.clear () in let sm = State_machine.create (module State) spec ~enable:vdd in - + (* === TRNG Submodule === *) let trng_request_new = Variable.wire ~default:gnd in - + let trng = Trng.create (Scope.sub_scope scope "trng") { Trng.I. clock = i.clock @@ -105,15 +104,15 @@ let create scope (i : _ I.t) = ; load_seed = i.trng_load_seed } in - + (* === Nonce Register === *) let current_nonce = Variable.reg spec ~width:Config.nonce_width in - + (* === ECDSA Submodule === *) let ecdsa_start = Variable.wire ~default:gnd in let license_r_reg = Variable.reg spec ~width:Config.signature_width in let license_s_reg = Variable.reg spec ~width:Config.signature_width in - + let ecdsa = Ecdsa.create (Scope.sub_scope scope "ecdsa") { Ecdsa.I. clock = i.clock @@ -126,28 +125,28 @@ let create scope (i : _ I.t) = ; param_b3 = i.param_b3 } in - + (* === Usage Allowance (inline) === *) let allowance = Variable.reg spec ~width:Config.allowance_width in let increment_allowance = Variable.wire ~default:gnd in - + let enabled = allowance.value >:. 0 in - + (* Allowance update: increment takes priority, otherwise decrement each cycle *) let increment_amount = of_int ~width:Config.allowance_width Config.allowance_increment in - let incremented_allowance = + let incremented_allowance = let sum = allowance.value +: increment_amount in (* Saturate on overflow *) mux2 (sum <: allowance.value) (ones Config.allowance_width) sum in let decremented_allowance = allowance.value -:. 1 in - + (* === Statistics === *) let licenses_accepted = Variable.reg spec ~width:16 in - + (* === Init Delay Counter === *) let delay_counter = Variable.reg spec ~width:16 in - + (* === State Machine === *) compile [ (* Allowance update logic - runs every cycle independent of state machine *) @@ -157,7 +156,7 @@ let create scope (i : _ I.t) = ] @@ elif (allowance.value >:. 0) [ allowance <-- decremented_allowance; ] []; - + (* State machine *) sm.switch [ State.Init_delay, [ @@ -166,19 +165,19 @@ let create scope (i : _ I.t) = sm.set_next Request_nonce; ]; ]; - + State.Request_nonce, [ trng_request_new <-- vdd; sm.set_next Wait_nonce; ]; - + State.Wait_nonce, [ when_ trng.nonce_valid [ current_nonce <-- trng.nonce; sm.set_next Publish; ]; ]; - + State.Publish, [ (* Nonce is stable, wait for license submission *) when_ i.license_submit [ @@ -187,59 +186,55 @@ let create scope (i : _ I.t) = sm.set_next Verify_start; ]; ]; - + State.Verify_start, [ when_ (~:(ecdsa.busy)) [ ecdsa_start <-- vdd; sm.set_next Verify_wait; ]; ]; - + State.Verify_wait, [ when_ ecdsa.done_ [ - sm.set_next Update; - ]; - ]; - - State.Update, [ - if_ ecdsa.valid [ - (* Valid license: increment allowance, get new nonce *) - increment_allowance <-- vdd; - licenses_accepted <-- licenses_accepted.value +:. 1; - sm.set_next Request_nonce; - ] [ - (* Invalid license: return to Publish with same nonce *) - sm.set_next Publish; + if_ ecdsa.valid [ + (* Valid license: increment allowance, get new nonce *) + increment_allowance <-- vdd; + licenses_accepted <-- licenses_accepted.value +:. 1; + sm.set_next Request_nonce; + ] [ + (* Invalid license: return to Publish with same nonce *) + sm.set_next Publish; + ]; ]; ]; ]; ]; - + (* === Workload: Signed Int8 Addition with AND-based Output Gating === *) - let int8_sum = + let int8_sum = let a_signed = i.int8_a in let b_signed = i.int8_b in (a_signed +: b_signed).:[(7, 0)] (* Wrapping addition *) in - + (* SECURITY GATE: AND each output bit with enabled signal *) let enabled_mask = repeat enabled 8 in let gated_result = int8_sum &: enabled_mask in - + (* Pipeline register for workload output *) let result_reg = Variable.reg spec ~width:8 in let result_valid_reg = Variable.reg spec ~width:1 in - + compile [ result_valid_reg <-- i.workload_valid; result_reg <-- gated_result; ]; - + (* === State Encoding for Debug === *) - let state_encoding = + let state_encoding = uresize (sm.current) 4 in - + { O. nonce = current_nonce.value ; nonce_ready = sm.is Publish @@ -250,4 +245,4 @@ let create scope (i : _ I.t) = ; state_debug = state_encoding ; licenses_accepted = licenses_accepted.value ; ecdsa_busy = ecdsa.busy - } \ No newline at end of file + } diff --git a/test/test_arith.ml b/test/test_arith.ml index 9989960..4dfdcf9 100644 --- a/test/test_arith.ml +++ b/test/test_arith.ml @@ -1194,6 +1194,8 @@ Stdio.printf "=== End Montgomery Debug Test ===\n\n"; Stdio.printf "╚════██║██║ ██║██║ ██║ ██╔══╝ ╚════██║╚════██║\n"; Stdio.printf "███████║╚██████╔╝╚██████╗╚██████╗███████╗███████║███████║\n"; Stdio.printf "╚══════╝ ╚═════╝ ╚═════╝ ╚═════╝╚══════╝╚══════╝╚══════╝\n"; - Stdio.printf "\nAll Arith unit tests passed! ✓✓✓\n" - end else - Stdio.printf "\n✗ Some tests failed - review above for details\n" \ No newline at end of file + Stdio.printf "\nAll Arith unit tests passed! ✓✓✓\n"; + end else begin + Stdio.printf "\n✗ Some tests failed - review above for details\n"; + failwith "checks failed"; + end \ No newline at end of file diff --git a/test/test_ecdsa.ml b/test/test_ecdsa.ml index b98736f..4b6e1d3 100644 --- a/test/test_ecdsa.ml +++ b/test/test_ecdsa.ml @@ -346,6 +346,8 @@ let () = Stdio.printf "╚════██║██║ ██║██║ ██║ ██╔══╝ ╚════██║╚════██║\n"; Stdio.printf "███████║╚██████╔╝╚██████╗╚██████╗███████╗███████║███████║\n"; Stdio.printf "╚══════╝ ╚═════╝ ╚═════╝ ╚═════╝╚══════╝╚══════╝╚══════╝\n"; - Stdio.printf "\nAll ECDSA verification tests passed! ✓✓✓\n" - end else - Stdio.printf "\n✗ Some tests failed - review above for details\n" \ No newline at end of file + Stdio.printf "\nAll ECDSA verification tests passed! ✓✓✓\n"; + end else begin + Stdio.printf "\n✗ Some tests failed - review above for details\n"; + failwith "checks failed"; + end \ No newline at end of file diff --git a/test/test_mod_add.ml b/test/test_mod_add.ml index ecbde41..884ca62 100644 --- a/test/test_mod_add.ml +++ b/test/test_mod_add.ml @@ -132,9 +132,11 @@ let test () = Stdio.printf "=== Test Summary ===\n"; Stdio.printf "Passed: %d/%d\n" passed total; - if passed = total then - Stdio.printf "\n✓ All tests passed!\n" - else - Stdio.printf "\n✗ Some tests failed\n" + if passed = total then begin + Stdio.printf "\n✓ All tests passed!\n"; + end else begin + Stdio.printf "\n✗ Some tests failed\n"; + failwith "checks failed"; + end let () = test () diff --git a/test/test_mod_inv.ml b/test/test_mod_inv.ml index d933d7b..2104fdc 100644 --- a/test/test_mod_inv.ml +++ b/test/test_mod_inv.ml @@ -40,44 +40,44 @@ end let test () = Stdio.printf "=== ModInv Hardware Test (256-bit with Zarith) ===\n"; Stdio.printf "=== Assuming odd prime modulus ===\n\n"; - + let scope = Scope.create ~flatten_design:true () in let module Sim = Cyclesim.With_interface(ModInvWithModAdd.I)(ModInvWithModAdd.O) in let sim = Sim.create (ModInvWithModAdd.create scope) in - + let inputs = Cyclesim.inputs sim in let outputs = Cyclesim.outputs sim in - + let z_to_bits z = let hex_str = Z.format "%x" z in let padded = String.pad_left hex_str ~len:((Mod_inv.Config.width + 3) / 4) ~char:'0' in Bits.of_hex ~width:Mod_inv.Config.width padded in - + let test_case name x_z mod_z should_have_inverse expected_result_z_opt = Stdio.printf "Test: %s\n" name; Stdio.printf " x = %s\n" (Z.to_string x_z); Stdio.printf " modulus = %s\n" (Z.to_string mod_z); - + let x_bits = z_to_bits x_z in let mod_bits = z_to_bits mod_z in - + inputs.clear := Bits.vdd; inputs.start := Bits.gnd; inputs.x := Bits.zero Mod_inv.Config.width; inputs.modulus := Bits.zero Mod_inv.Config.width; Cyclesim.cycle sim; - + inputs.clear := Bits.gnd; Cyclesim.cycle sim; - + inputs.x := x_bits; inputs.modulus := mod_bits; inputs.start := Bits.vdd; Cyclesim.cycle sim; - + inputs.start := Bits.gnd; - + let max_cycles = 3000 in let rec wait cycle_count = if cycle_count >= max_cycles then begin @@ -86,53 +86,53 @@ let test () = end else if Bits.to_bool !(outputs.valid) then begin let result_bits = !(outputs.result) in let inverse_exists = Bits.to_bool !(outputs.exists) in - + Stdio.printf " Completed in %d cycles\n" cycle_count; Stdio.printf " Inverse exists: %b\n" inverse_exists; - - let test_passed = + + let test_passed = if Bool.(<>) inverse_exists should_have_inverse then begin - Stdio.printf " ERROR: Expected inverse to %sexist ✗\n" + Stdio.printf " ERROR: Expected inverse to %sexist ✗\n" (if should_have_inverse then "" else "not "); false end else if inverse_exists then begin - let result_z = + let result_z = let bin_str = Bits.to_bstr result_bits in Z.of_string_base 2 bin_str in Stdio.printf " result = %s\n" (Z.to_string result_z); - + let product = Z.(x_z * result_z mod mod_z) in let verified = Z.equal product Z.one in - - Stdio.printf " Verification: (x * result) mod modulus = %s\n" + + Stdio.printf " Verification: (x * result) mod modulus = %s\n" (Z.to_string product); - + if verified then Stdio.printf " Mathematical verification: PASS ✓\n" else Stdio.printf " Mathematical verification: FAIL ✗\n"; - - let matches_expected = + + let matches_expected = match expected_result_z_opt with | Some expected_z when Z.equal result_z expected_z -> Stdio.printf " Matches expected value ✓\n"; true | Some expected_z -> - Stdio.printf " Note: Expected %s but got %s\n" + Stdio.printf " Note: Expected %s but got %s\n" (Z.to_string expected_z) (Z.to_string result_z); verified | None -> verified in - + verified && matches_expected end else begin Stdio.printf " Correctly determined no inverse exists ✓\n"; true end in - + Stdio.printf "\n"; test_passed end else begin @@ -142,57 +142,57 @@ let test () = in wait 0 in - + let results = [ - test_case "3^(-1) mod 7" + test_case "3^(-1) mod 7" (Z.of_int 3) (Z.of_int 7) true (Some (Z.of_int 5)); - - test_case "7^(-1) mod 13" + + test_case "7^(-1) mod 13" (Z.of_int 7) (Z.of_int 13) true (Some (Z.of_int 2)); - - test_case "5^(-1) mod 11" + + test_case "5^(-1) mod 11" (Z.of_int 5) (Z.of_int 11) true (Some (Z.of_int 9)); - - test_case "17^(-1) mod 31" + + test_case "17^(-1) mod 31" (Z.of_int 17) (Z.of_int 31) true (Some (Z.of_int 11)); - - test_case "42^(-1) mod 2017" + + test_case "42^(-1) mod 2017" (Z.of_int 42) (Z.of_int 2017) true (Some (Z.of_int 1969)); - - test_case "123^(-1) mod 257" + + test_case "123^(-1) mod 257" (Z.of_int 123) (Z.of_int 257) true None; - - test_case "1^(-1) mod 7" + + test_case "1^(-1) mod 7" (Z.of_int 1) (Z.of_int 7) true (Some (Z.of_int 1)); - - test_case "2^(-1) mod 3" + + test_case "2^(-1) mod 3" (Z.of_int 2) (Z.of_int 3) true (Some (Z.of_int 2)); - + test_case "Large 64-bit inverse" (Z.of_string "123456789012345") (Z.of_string "999999999999999989") true None; - + test_case "128-bit inverse" (Z.of_string "123456789012345678901234567890") (Z.of_string "340282366920938463463374607431768211297") true None; - + test_case "254-bit: inverse mod 254-bit prime" (Z.of_string "123456789012345678901234567890") (Z.of_string "28948022309329048855892746252171976963317496166410141009864396001978282409867") true None; - + test_case "255-bit: inverse mod 255-bit prime" (Z.of_string "987654321098765432109876543210") (Z.of_string "57896044618658097711785492504343953926634992332820282019728792003956564819949") true None; - + test_case "256-bit: inverse mod secp256k1 prime" (Z.of_string "12345678901234567890") (Z.of_string "115792089237316195423570985008687907853269984665640564039457584007908834671663") true None; - + test_case "256-bit: inverse mod large odd prime" (Z.of_string "999999999999999999") (Z.of_string "115792089237316195423570985008687907853269984665640564039457584007913129639747") @@ -202,7 +202,7 @@ let test () = (Z.of_string "999999999999999999") (Z.of_string "0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141") true None; - + test_case "Edge: (m-1)^(-1) mod m" (Z.of_int 12) (Z.of_int 13) @@ -213,13 +213,13 @@ let test () = (Z.of_string "115792089237316195423570985008687907853269984665640564039457584007908834671663") true None; ] in - + let passed = List.count results ~f:Fn.id in let total = List.length results in - + Stdio.printf "=== Test Summary ===\n"; Stdio.printf "Passed: %d/%d\n" passed total; - + if passed = total then begin Stdio.printf "\n"; Stdio.printf "███████╗██╗ ██╗ ██████╗ ██████╗███████╗███████╗███████╗\n"; @@ -228,8 +228,10 @@ let test () = Stdio.printf "╚════██║██║ ██║██║ ██║ ██╔══╝ ╚════██║╚════██║\n"; Stdio.printf "███████║╚██████╔╝╚██████╗╚██████╗███████╗███████║███████║\n"; Stdio.printf "╚══════╝ ╚═════╝ ╚═════╝ ╚═════╝╚══════╝╚══════╝╚══════╝\n"; - Stdio.printf "\nAll cryptographic tests passed! ✓✓✓\n" - end else - Stdio.printf "Some tests failed - NOT READY FOR PRODUCTION ✗\n" + Stdio.printf "\nAll cryptographic tests passed! ✓✓✓\n"; + end else begin + Stdio.printf "Some tests failed - NOT READY FOR PRODUCTION ✗\n"; + failwith "checks failed"; + end let () = test () diff --git a/test/test_mod_mul.ml b/test/test_mod_mul.ml index 1301363..2b1f989 100644 --- a/test/test_mod_mul.ml +++ b/test/test_mod_mul.ml @@ -181,8 +181,10 @@ let test () = Stdio.printf "╚════██║██║ ██║██║ ██║ ██╔══╝ ╚════██║╚════██║\n"; Stdio.printf "███████║╚██████╔╝╚██████╗╚██████╗███████╗███████║███████║\n"; Stdio.printf "╚══════╝ ╚═════╝ ╚═════╝ ╚═════╝╚══════╝╚══════╝╚══════╝\n"; - Stdio.printf "\nAll tests passed! ✓✓✓\n" - end else - Stdio.printf "Some tests failed ✗\n" + Stdio.printf "\nAll tests passed! ✓✓✓\n"; + end else begin + Stdio.printf "Some tests failed ✗\n"; + failwith "checks failed"; + end let () = test () diff --git a/test/test_security_block.ml b/test/test_security_block.ml index b589b08..8cea046 100644 --- a/test/test_security_block.ml +++ b/test/test_security_block.ml @@ -3,48 +3,50 @@ open Base open Hardcaml +module State = Security_block.State + let () = Stdio.printf "=== Security Block Test ===\n\n"; - + let scope = Scope.create ~flatten_design:true () in let module Sim = Cyclesim.With_interface(Security_block.I)(Security_block.O) in let sim = Sim.create (Security_block.create scope) in - + let inputs = Cyclesim.inputs sim in let outputs = Cyclesim.outputs sim in - + let prime_n = Arith.Config.prime_n in - + (* secp256k1 curve parameters *) let param_a = Z.zero in let param_b3 = Z.of_int 21 in - + (* Generator point G *) let g_x = Z.of_string "0x79BE667EF9DCBBAC55A06295CE870B07029BFCDB2DCE28D959F2815B16F81798" in let g_y = Z.of_string "0x483ADA7726A3C4655DA4FBFC0E1108A8FD17B448A68554199C47D08FFB10D4B8" in - + (* Private key d = 2, Public key Q = 2G (must match ECDSA module's hardcoded Q) *) let private_key = Z.of_int 2 in - + let z_to_bits z = let hex_str = Z.format "%x" z in let padded = String.pad_left hex_str ~len:64 ~char:'0' in Bits.of_hex ~width:256 padded in - + let int8_to_bits i = Bits.of_int ~width:8 (i land 0xFF) in - + let bits_to_int8 b = let v = Bits.to_int b in if v > 127 then v - 256 else v in - + let bits_to_int64 b = Bits.to_int64 b in - + (* Modular arithmetic helpers *) let mod_inv_n a = Z.invert a prime_n in let mod_mul_n a b = Z.((a * b) mod prime_n) in @@ -52,7 +54,7 @@ let () = let prime_p = Arith.Config.prime_p in let mod_mul_p a b = Z.((a * b) mod prime_p) in let mod_inv_p a = Z.invert a prime_p in - + (* Reference: affine point addition *) let affine_add (x1, y1) (x2, y2) = let mod_add a b = Z.((a + b) mod prime_p) in @@ -72,20 +74,20 @@ let () = Some (x3, y3) end in - + (* Reference: scalar multiplication *) let scalar_mult k (x, y) = let rec loop n acc pt = if Z.equal n Z.zero then acc else - let acc' = + let acc' = if Z.(equal (n land one) one) then match acc with | None -> Some pt | Some a -> affine_add a pt else acc in - let pt' = + let pt' = match affine_add pt pt with | None -> pt | Some p -> p @@ -94,7 +96,7 @@ let () = in loop k None (x, y) in - + (* Generate a valid ECDSA signature for message hash z using nonce k *) let sign ~z ~k = match scalar_mult k (g_x, g_y) with @@ -108,7 +110,7 @@ let () = if Z.equal s Z.zero then None else Some (r, s) in - + let reset () = inputs.clear := Bits.vdd; inputs.license_submit := Bits.gnd; @@ -125,43 +127,33 @@ let () = inputs.clear := Bits.gnd; Cyclesim.cycle sim in - + let get_allowance () = bits_to_int64 !(outputs.allowance) in - + let get_enabled () = Bits.to_bool !(outputs.enabled) in - + let get_nonce () = Bits.to_z ~signedness:Unsigned !(outputs.nonce) in - + let get_nonce_ready () = Bits.to_bool !(outputs.nonce_ready) in - + let get_state () = - Bits.to_int !(outputs.state_debug) + List.nth_exn State.all (Bits.to_int !(outputs.state_debug)) in - + let get_licenses_accepted () = Bits.to_int !(outputs.licenses_accepted) in - - let state_name state = - match state with - | 0 -> "Init_delay" - | 1 -> "Request_nonce" - | 2 -> "Wait_nonce" - | 3 -> "Publish" - | 4 -> "Verify_start" - | 5 -> "Verify_wait" - | 6 -> "Update" - | _ -> "Unknown" - in - + + let state_to_string s = Sexp.to_string (State.sexp_of_t s) in + let wait_for_nonce_ready ~max_cycles = let rec loop n = if n >= max_cycles then begin @@ -177,7 +169,7 @@ let () = in loop 0 in - + let submit_license ~r ~s = inputs.license_submit := Bits.vdd; inputs.license_r := z_to_bits r; @@ -186,7 +178,7 @@ let () = inputs.license_submit := Bits.gnd; inputs.license_r := Bits.zero 256; inputs.license_s := Bits.zero 256; - + let max_cycles = 15_000_000 in let rec loop n last_state = if n >= max_cycles then begin @@ -194,7 +186,7 @@ let () = None end else begin let current_state = get_state () in - if last_state = 6 && current_state <> 6 then begin + if (State.equal last_state Verify_wait) && not (State.equal current_state Verify_wait) then begin Stdio.printf " Verification completed in %d cycles\n" n; Some current_state end else begin @@ -205,7 +197,7 @@ let () = in loop 0 (get_state ()) in - + let do_workload ~a ~b = inputs.workload_valid := Bits.vdd; inputs.int8_a := int8_to_bits a; @@ -216,93 +208,93 @@ let () = let valid = Bits.to_bool !(outputs.result_valid) in (result, valid) in - + let results = ref [] in let record result = results := result :: !results in - + (* ============================================== *) (* TEST 1: Initial state - allowance is 0 *) (* ============================================== *) - + Stdio.printf "Test 1: Initial state - allowance is 0, workload blocked\n"; - + reset (); - + let initial_allowance = get_allowance () in let initial_enabled = get_enabled () in - + Stdio.printf " Initial allowance = %Ld (expected 0)\n" initial_allowance; Stdio.printf " Initial enabled = %b (expected false)\n" initial_enabled; - + let pass = (Int64.(=) initial_allowance 0L) && (not initial_enabled) in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass; - + (* ============================================== *) (* TEST 2: Workload blocked when allowance = 0 *) (* ============================================== *) - + Stdio.printf "Test 2: Workload blocked when allowance = 0\n"; - + reset (); - + let (result, valid) = do_workload ~a:10 ~b:20 in - + Stdio.printf " Workload: 10 + 20\n"; Stdio.printf " Result = %d (expected 0 due to gating)\n" result; Stdio.printf " Valid = %b\n" valid; - + let pass = (result = 0) in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass; - + (* ============================================== *) (* TEST 3: State machine reaches Publish state *) (* ============================================== *) - + Stdio.printf "Test 3: State machine reaches Publish state with valid nonce\n"; - + reset (); - + inputs.trng_seed := z_to_bits (Z.of_int 42); inputs.trng_load_seed := Bits.vdd; Cyclesim.cycle sim; inputs.trng_load_seed := Bits.gnd; - + (match wait_for_nonce_ready ~max_cycles:200 with - | None -> + | None -> Stdio.printf " Failed to reach Publish state\n"; record false | Some nonce -> Stdio.printf " Nonce = %s\n" (Z.to_string nonce); - Stdio.printf " State = %s\n" (state_name (get_state ())); + Stdio.printf " State = %s\n" (state_to_string (get_state ())); let pass = get_nonce_ready () in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass); - + (* ============================================== *) (* TEST 4: Valid license increments allowance *) (* ============================================== *) - + Stdio.printf "Test 4: Valid license increments allowance\n"; - + reset (); - + inputs.trng_seed := z_to_bits (Z.of_int 12345); inputs.trng_load_seed := Bits.vdd; Cyclesim.cycle sim; inputs.trng_load_seed := Bits.gnd; - + (match wait_for_nonce_ready ~max_cycles:200 with | None -> Stdio.printf " Failed to reach Publish state\n"; record false | Some nonce -> Stdio.printf " Nonce (z) = %s\n" (Z.to_string nonce); - + let allowance_before = get_allowance () in let accepted_before = get_licenses_accepted () in - + let k = Z.of_int 7 in (match sign ~z:nonce ~k with | None -> @@ -311,37 +303,37 @@ let () = | Some (r, s) -> Stdio.printf " Generated r = %s...\n" (String.prefix (Z.to_string r) 30); Stdio.printf " Generated s = %s...\n" (String.prefix (Z.to_string s) 30); - + (match submit_license ~r ~s with | None -> record false | Some new_state -> let allowance_after = get_allowance () in let accepted_after = get_licenses_accepted () in - + Stdio.printf " Allowance before = %Ld\n" allowance_before; Stdio.printf " Allowance after = %Ld\n" allowance_after; Stdio.printf " Licenses accepted: %d -> %d\n" accepted_before accepted_after; - Stdio.printf " New state = %s (expected Request_nonce)\n" (state_name new_state); - - let pass = Int64.(>) allowance_after allowance_before + Stdio.printf " New state = %s (expected Request_nonce)\n" (state_to_string new_state); + + let pass = Int64.(>) allowance_after allowance_before && (accepted_after = accepted_before + 1) - && (new_state = 1) in + && (State.equal new_state Request_nonce) in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass))); - + (* ============================================== *) (* TEST 5: Workload works after valid license *) (* ============================================== *) - + Stdio.printf "Test 5: Workload works after valid license\n"; - + reset (); - + inputs.trng_seed := z_to_bits (Z.of_int 55555); inputs.trng_load_seed := Bits.vdd; Cyclesim.cycle sim; inputs.trng_load_seed := Bits.gnd; - + (match wait_for_nonce_ready ~max_cycles:200 with | None -> Stdio.printf " Failed to reach Publish state\n"; @@ -361,74 +353,74 @@ let () = | Some _ -> let enabled_now = get_enabled () in Stdio.printf " Enabled = %b (expected true)\n" enabled_now; - + let (result, valid) = do_workload ~a:10 ~b:20 in - + Stdio.printf " Workload: 10 + 20\n"; Stdio.printf " Result = %d (expected 30)\n" result; Stdio.printf " Valid = %b\n" valid; - + let pass = (result = 30) && valid && enabled_now in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass)))); - + (* ============================================== *) (* TEST 6: Invalid license - same nonce retained *) (* ============================================== *) - + Stdio.printf "Test 6: Invalid license does not increment allowance, same nonce retained\n"; - + reset (); - + inputs.trng_seed := z_to_bits (Z.of_int 99999); inputs.trng_load_seed := Bits.vdd; Cyclesim.cycle sim; inputs.trng_load_seed := Bits.gnd; - + (match wait_for_nonce_ready ~max_cycles:200 with | None -> Stdio.printf " Failed to reach Publish state\n"; record false | Some nonce_before -> Stdio.printf " Nonce (z) = %s\n" (Z.to_string nonce_before); - + let allowance_before = get_allowance () in - + let wrong_r = Z.of_int 11111 in let wrong_s = Z.of_int 22222 in - + Stdio.printf " Submitting invalid signature (r=11111, s=22222)\n"; - + (match submit_license ~r:wrong_r ~s:wrong_s with | None -> record false | Some new_state -> let allowance_after = get_allowance () in let nonce_after = get_nonce () in - + Stdio.printf " Allowance before = %Ld\n" allowance_before; Stdio.printf " Allowance after = %Ld\n" allowance_after; - Stdio.printf " New state = %s (expected Publish)\n" (state_name new_state); + Stdio.printf " New state = %s (expected Publish)\n" (state_to_string new_state); Stdio.printf " Nonce unchanged = %b\n" (Z.equal nonce_before nonce_after); - + let pass = Int64.(=) allowance_after allowance_before - && (new_state = 3) + && (State.equal new_state Publish) && Z.equal nonce_before nonce_after in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass)); - + (* ============================================== *) (* TEST 7: Signed Int8 addition - positive *) (* ============================================== *) - + Stdio.printf "Test 7: Signed Int8 addition - positive values\n"; - + reset (); - + inputs.trng_seed := z_to_bits (Z.of_int 777); inputs.trng_load_seed := Bits.vdd; Cyclesim.cycle sim; inputs.trng_load_seed := Bits.gnd; - + (match wait_for_nonce_ready ~max_cycles:200 with | None -> Stdio.printf " Failed to reach Publish state\n"; @@ -451,86 +443,86 @@ let () = let pass = (result = 80) in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass)))); - + (* ============================================== *) (* TEST 8: Signed Int8 addition - negative *) (* ============================================== *) - + Stdio.printf "Test 8: Signed Int8 addition - negative values\n"; - + let (result, _) = do_workload ~a:(-10) ~b:(-20) in Stdio.printf " Workload: -10 + -20 = %d (expected -30)\n" result; let pass = (result = -30) in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass; - + (* ============================================== *) (* TEST 9: Signed Int8 addition - mixed signs *) (* ============================================== *) - + Stdio.printf "Test 9: Signed Int8 addition - mixed signs\n"; - + let (result, _) = do_workload ~a:100 ~b:(-30) in Stdio.printf " Workload: 100 + -30 = %d (expected 70)\n" result; let pass = (result = 70) in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass; - + (* ============================================== *) (* TEST 10: Signed Int8 addition - wrapping *) (* ============================================== *) - + Stdio.printf "Test 10: Signed Int8 addition - overflow wrapping\n"; - + let (result, _) = do_workload ~a:127 ~b:1 in Stdio.printf " Workload: 127 + 1 = %d (expected -128 due to wrapping)\n" result; let pass = (result = -128) in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass; - + (* ============================================== *) (* TEST 11: Allowance decrements each cycle *) (* ============================================== *) - + Stdio.printf "Test 11: Allowance decrements each clock cycle\n"; - + let allowance_before = get_allowance () in - + for _ = 1 to 100 do Cyclesim.cycle sim done; - + let allowance_after = get_allowance () in let decrement = Int64.(-) allowance_before allowance_after in - + Stdio.printf " Allowance before = %Ld\n" allowance_before; Stdio.printf " Allowance after = %Ld\n" allowance_after; Stdio.printf " Decrement over 100 cycles = %Ld (expected 100)\n" decrement; - + let pass = Int64.(=) decrement 100L in Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass; - + (* ============================================== *) (* TEST 12: New nonce after valid license only *) (* ============================================== *) - + Stdio.printf "Test 12: New nonce generated after valid license only\n"; - + reset (); - + inputs.trng_seed := z_to_bits (Z.of_int 1000); inputs.trng_load_seed := Bits.vdd; Cyclesim.cycle sim; inputs.trng_load_seed := Bits.gnd; - + (match wait_for_nonce_ready ~max_cycles:200 with | None -> Stdio.printf " Failed to reach Publish state\n"; record false | Some nonce1 -> Stdio.printf " First nonce = %s\n" (Z.to_string nonce1); - + let k = Z.of_int 17 in (match sign ~z:nonce1 ~k with | None -> @@ -544,38 +536,38 @@ let () = | None -> record false | Some nonce2 -> Stdio.printf " Second nonce = %s\n" (Z.to_string nonce2); - + let pass = not (Z.equal nonce1 nonce2) in Stdio.printf " Nonces different = %b (expected true)\n" pass; Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass)))); - + (* ============================================== *) (* TEST 13: License for wrong nonce is rejected *) (* ============================================== *) - + Stdio.printf "Test 13: License signed for wrong nonce is rejected\n"; - + reset (); - + inputs.trng_seed := z_to_bits (Z.of_int 5000); inputs.trng_load_seed := Bits.vdd; Cyclesim.cycle sim; inputs.trng_load_seed := Bits.gnd; - + (match wait_for_nonce_ready ~max_cycles:200 with | None -> Stdio.printf " Failed to reach Publish state\n"; record false | Some nonce -> Stdio.printf " Actual nonce = %s\n" (Z.to_string nonce); - + let allowance_before = get_allowance () in - + let wrong_nonce = Z.of_int 9999 in let k = Z.of_int 7 in Stdio.printf " Signing wrong nonce = %s\n" (Z.to_string wrong_nonce); - + (match sign ~z:wrong_nonce ~k with | None -> Stdio.printf " Failed to generate signature\n"; @@ -585,37 +577,37 @@ let () = | None -> record false | Some new_state -> let allowance_after = get_allowance () in - + Stdio.printf " Allowance before = %Ld\n" allowance_before; Stdio.printf " Allowance after = %Ld\n" allowance_after; - Stdio.printf " New state = %s (expected Publish)\n" (state_name new_state); - - let pass = Int64.(<=) allowance_after allowance_before - && (new_state = 3) in + Stdio.printf " New state = %s (expected Publish)\n" (state_to_string new_state); + + let pass = Int64.(<=) allowance_after allowance_before + && (State.equal new_state Publish) in Stdio.printf " Allowance not incremented = %b (expected true)\n" pass; Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass))); - + (* ============================================== *) (* TEST 14: Cannot replay same license twice *) (* ============================================== *) - + Stdio.printf "Test 14: Cannot replay same valid license twice\n"; - + reset (); - + inputs.trng_seed := z_to_bits (Z.of_int 7777); inputs.trng_load_seed := Bits.vdd; Cyclesim.cycle sim; inputs.trng_load_seed := Bits.gnd; - + (match wait_for_nonce_ready ~max_cycles:200 with | None -> Stdio.printf " Failed to reach Publish state\n"; record false | Some nonce1 -> Stdio.printf " First nonce = %s\n" (Z.to_string nonce1); - + let k = Z.of_int 19 in (match sign ~z:nonce1 ~k with | None -> @@ -623,47 +615,47 @@ let () = record false | Some (r, s) -> Stdio.printf " Generated signature for first nonce\n"; - + let accepted_before = get_licenses_accepted () in (match submit_license ~r ~s with | None -> record false | Some _ -> let accepted_after_first = get_licenses_accepted () in Stdio.printf " First submission: accepted = %b\n" (accepted_after_first > accepted_before); - + (match wait_for_nonce_ready ~max_cycles:200 with | None -> record false | Some nonce2 -> Stdio.printf " Second nonce = %s\n" (Z.to_string nonce2); - + Stdio.printf " Attempting to replay same signature...\n"; (match submit_license ~r ~s with | None -> record false | Some new_state -> let accepted_after_second = get_licenses_accepted () in - - Stdio.printf " Second submission: accepted = %b\n" + + Stdio.printf " Second submission: accepted = %b\n" (accepted_after_second > accepted_after_first); - Stdio.printf " New state = %s\n" (state_name new_state); - + Stdio.printf " New state = %s\n" (state_to_string new_state); + let pass = (accepted_after_first = accepted_before + 1) && (accepted_after_second = accepted_after_first) - && (new_state = 3) in + && (State.equal new_state Publish) in Stdio.printf " Replay rejected = %b (expected true)\n" pass; Stdio.printf " %s\n\n" (if pass then "PASS ✓" else "FAIL ✗"); record pass))))); - + (* ============================================== *) (* TEST SUMMARY *) (* ============================================== *) - + let results_list = List.rev !results in let passed = List.count results_list ~f:Fn.id in let total = List.length results_list in - + Stdio.printf "=== Test Summary ===\n"; Stdio.printf "Passed: %d/%d\n" passed total; - + if passed = total then begin Stdio.printf "\n"; Stdio.printf "███████╗██╗ ██╗ ██████╗ ██████╗███████╗███████╗███████╗\n"; @@ -672,6 +664,8 @@ let () = Stdio.printf "╚════██║██║ ██║██║ ██║ ██╔══╝ ╚════██║╚════██║\n"; Stdio.printf "███████║╚██████╔╝╚██████╗╚██████╗███████╗███████║███████║\n"; Stdio.printf "╚══════╝ ╚═════╝ ╚═════╝ ╚═════╝╚══════╝╚══════╝╚══════╝\n"; - Stdio.printf "\nAll Security Block tests passed! ✓✓✓\n" - end else - Stdio.printf "\n✗ Some tests failed - review above for details\n" \ No newline at end of file + Stdio.printf "\nAll Security Block tests passed! ✓✓✓\n"; + end else begin + Stdio.printf "\n✗ Some tests failed - review above for details\n"; + failwith "checks failed"; + end