Theory Misc.Bitfields

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Bitfields
  imports
    WordAdditional Word_Lib.Bit_Shifts_Infix_Syntax
begin
(*>*)

section ‹Utility functions for working with bitfields›

(*<*)
context
begin

unbundle bit_operations_syntax
(*>*)

text‹Extract a subfield, or range of bits, from an input word given a position and length of the
subfield.  Implicitly casts the subfield out of the original input word's length into another.›
definition extract_subfield :: ‹'a::{len} word ⇒ nat ⇒ nat ⇒ 'b::{len} word› where
  ‹extract_subfield w position l ≡
     ucast ((w >> position) AND ((1 << l) - 1))›

text‹Write a subfield at a position in a given word.›
definition write_subfield :: ‹'a::{len} word ⇒ nat ⇒ 'b::{len} word ⇒ 'a::{len} word› where
  ‹write_subfield w position f ≡
     let mask = (1 << LENGTH('b)) - 1 in
       (w AND NOT (mask << position)) OR ((ucast f AND mask) << position)›

(*<*)
end

end
(*>*)