#include <stdint.h>

void msr_write(uint32_t index, uint64_t value);
uint64_t msr_read(uint32_t index);