emit: support casts from size_t to fixed-width integers

src/pass/emit.rs

@@ -1860,6 +1860,21 @@ impl<'a> Emitter<'a> {
                         (TypeT::SizeT, TypeT::SpecInt | TypeT::SpecNat) => {
                             unaryfn(Doc::text("SizeT.v"), val_doc)
                         }
+                        (TypeT::SizeT, TypeT::Int { signed, width }) => {
+                            if let Some(m) = get_int_mod(signed, width) {
+                                unaryfn(
+                                    Doc::text(format!(
+                                        "{}.{} (SizeT.v",
+                                        m,
+                                        if *signed { "int_to_t" } else { "uint_to_t" }
+                                    )),
+                                    val_doc.append(Doc::text(")")),
+                                )
+                            } else {
+                                self.report(default_msg.clone(), &v.loc);
+                                Doc::text("(admit())")
+                            }
+                        }
                         (TypeT::Int { signed, width }, TypeT::SizeT) => {
                             if let Some(m) = get_int_mod(signed, width) {
                                 unaryfn(
@@ -1893,7 +1908,6 @@ impl<'a> Emitter<'a> {
                         // (TypeT::Int { signed, width }, TypeT::SizeT) => todo!(),
                         // (TypeT::Int { signed, width }, TypeT::SLProp) => todo!(),
                         // (TypeT::SizeT, TypeT::Bool) => todo!(),
-                        // (TypeT::SizeT, TypeT::Int { signed, width }) => todo!(),
                         // (TypeT::SizeT, TypeT::SLProp) => todo!(),
                         // (TypeT::Pointer { to, kind }, TypeT::Bool) => todo!(),
                         (TypeT::Pointer(_, kind), TypeT::Bool) => {

test/cast_sizet_to_uint32/Makefile

@@ -0,0 +1 @@
+../_templates/Makefile

test/cast_sizet_to_uint32/cast_sizet_to_uint32.c

@@ -0,0 +1,17 @@
+#include "pal.h"
+#include <stddef.h>
+#include <stdint.h>
+
+uint32_t sizet_to_u32(size_t n)
+  _requires((_specint) n <= UINT32_MAX)
+  _ensures((_specint) return == n)
+{
+  return (uint32_t) n;
+}
+
+int32_t sizet_to_i32(size_t n)
+  _requires((_specint) n <= INT32_MAX)
+  _ensures((_specint) return == n)
+{
+  return (int32_t) n;
+}

test/cast_sizet_to_uint32/fstar.fst.config.json

@@ -0,0 +1 @@
+../_templates/fstar.fst.config.json

test/cast_sizet_to_uint32/pal.config.json

@@ -0,0 +1 @@
+../_templates/pal.config.json

test/cast_sizet_to_uint32/pal.h

@@ -0,0 +1 @@
+../pal.h