aygp-dr/freebsd-15-features.org Secret

## freebsd-15-features.org

      
    Raw
  

              freebsd-15-features.org
            
          
    FreeBSD 15.0 New Features - Validation Examples

Overview

Validation of new features introduced in FreeBSD 15.0-RELEASE on nexus server.

  Feature Description Status
  Native inotify Linux-compatible file notification API PASS
  OpenZFS 2.4.0 Latest ZFS with improvements PASS
  OpenSSL 3.5 Post-quantum cryptography support PASS
  pkgbase Base system installable via pkg N/A
  libsys separation Cleaner syscall interface PASS

1. Native inotify Support ✓

FreeBSD 15.0 adds native inotify(7) support for Linux compatibility.
Test C program

/* inotify_test.c - Test inotify on FreeBSD 15.0 */
#include <stdio.h>
#include <sys/inotify.h>
#include <unistd.h>

int main() {
    int fd = inotify_init();
    if (fd < 0) {
        perror("inotify_init");
        return 1;
    }
    
    int wd = inotify_add_watch(fd, "/tmp", IN_CREATE | IN_DELETE);
    if (wd < 0) {
        perror("inotify_add_watch");
        close(fd);
        return 1;
    }
    
    printf("inotify working on FreeBSD 15.0!\n");
    printf("fd=%d, wd=%d\n", fd, wd);
    
    inotify_rm_watch(fd, wd);
    close(fd);
    return 0;
}
Compile and run

cc -o /tmp/inotify_test examples/inotify_test.c && /tmp/inotify_test
Use case

inotify enables tools like inotifywait and applications expecting Linux-style
  file change notifications to work natively on FreeBSD.
pkg install inotify-tools  # Optional
inotifywait -m /tmp &      # Monitor /tmp for changes
2. OpenZFS 2.4.0 ✓

FreeBSD 15.0 includes OpenZFS 2.4.0 with performance improvements.
Check ZFS version

zfs version
ZFS pool status

zpool status zroot | head -15


Dataset listing

zfs list -o name,used,available,compression | head -10


ZFS 2.4 improvements


  Block cloning support
  Performance optimizations
  Better memory management
  Enhanced error handling

3. OpenSSL 3.5 with Post-Quantum Cryptography ✓

FreeBSD 15.0 includes OpenSSL 3.5 with ML-KEM (Kyber) support.
Check OpenSSL version

openssl version -a | head -5
Post-quantum algorithms available

openssl list -kem-algorithms


Generate post-quantum key (ML-KEM-768)

openssl genpkey -algorithm ML-KEM-768 -out /tmp/mlkem.pem
openssl pkey -in /tmp/mlkem.pem -text -noout | head -8
rm -f /tmp/mlkem.pem


Key Exchange Mechanisms (KEM) explained


  Algorithm Security Level Notes
  ML-KEM-512 NIST Level 1 Lightweight, fast
  ML-KEM-768 NIST Level 3 Balanced (recommended)
  ML-KEM-1024 NIST Level 5 Highest security
  X25519MLKEM768 Hybrid Classical + PQC combined

TLS 1.3 ciphers

openssl ciphers -v 'TLSv1.3' | head -5
4. pkgbase - Base System as Packages

FreeBSD 15.0 supports installing base system components via pkg (optional).
Status on this system

cat /etc/pkg/FreeBSD-base.conf 2>/dev/null || echo "pkgbase not configured (traditional install)"
pkgbase setup (if desired)

Create /usr/local/etc/pkg/repos/FreeBSD-base.conf:
FreeBSD-base: {
  url: "pkg+https://pkg.FreeBSD.org/${ABI}/base_release"
  mirror_type: "srv"
  signature_type: "fingerprints"
  fingerprints: "/usr/share/keys/pkg"
  enabled: yes
}
Then:
pkg update
pkg install FreeBSD-runtime FreeBSD-utilities
Benefits of pkgbase


  Granular base system updates
  Remove unused base components
  Mix release and stable packages
  Easier jail/container management

5. libsys Separation ✓

FreeBSD 15.0 introduces libsys.so.7 for cleaner syscall separation.
Check libsys presence

ls -la /lib/libsys.so*
Library dependency chain

ldd /bin/ls | grep -E "(libc|libsys)"
Architecture diagram

+-------------+
| Application |
+------+------+
       |
       v
+------+------+
| libc.so.7   |  <- Standard C library functions
+------+------+
       |
       v
+------+------+
| libsys.so.7 |  <- System call wrappers (NEW in 15.0)
+------+------+
       |
       v
+------+------+
|   Kernel    |  <- FreeBSD kernel
+-------------+

Benefits


  Cleaner architecture separation
  Easier syscall tracing with dtrace/ktrace
  Better security boundaries
  Simplified library updates

Important note

This is why interrupting freebsd-update install during 15.0 upgrade is
  dangerous: if libc.so.7 is installed before libsys.so.7, all dynamic
  executables fail with:
ld-elf.so.1: Shared object "libsys.so.7" not found

See: FreeBSD Bug 289769, fixed in FreeBSD-EN-25:18
6. System Verification

Kernel and userland versions

uname -a
freebsd-version -ku
Hardware info

sysctl hw.model hw.ncpu hw.physmem | awk '/physmem/ {printf "%s %.2f GB\n", $1, $2/1024/1024/1024} !/physmem/ {print}'
Validation Summary

=== FreeBSD 15.0 Features Validation Summary ===

1. Native inotify:
   Status: PASS

2. OpenZFS 2.4.0:
   zfs-2.4.0-rc4-FreeBSD_g099f69ff5
   Status: PASS

3. OpenSSL 3.5 + Post-Quantum:
   OpenSSL 3.5.4 30 Sep 2025
   ML-KEM-768: Available
   Status: PASS

4. pkgbase:
   Not configured (traditional install)
   Status: N/A (optional)

5. libsys separation:
   /lib/libsys.so.7 present
   Status: PASS

=== All core features validated ===

References


  FreeBSD 15.0-RELEASE Notes
  FreeBSD PkgBase Wiki
  OpenZFS Documentation
  OpenSSL 3.5 Documentation
  FreeBSD Bug 289769 (libsys)


## lean4-freebsd-15.org

      
    Raw
  

              lean4-freebsd-15.org
            
          
    Lean4 on FreeBSD 15.0-RELEASE Validation

Overview

Validation of Lean4 theorem prover on FreeBSD 15.0-RELEASE, updated from the
  14.3 validation document.
Version Information


  Component Version
  OS FreeBSD 15.0-RELEASE-p1
  Lean 4.27.0-pre
  Lake 5.0.0-src
  Package lean4-4.25.2.20251201

Prerequisites

procfs (Required)

Lean4 requires procfs to be mounted.
mount | grep proc
Ensure it’s in /etc/fstab:
proc /proc procfs rw 0 0
Installation

pkg install lean4
Verify installation:
lean --version
lake --version
Basic Validation

Theorem Proving ✓

theorem test : 1 + 1 = 2 := rfl
#check test
Evaluation ✓

#eval 2 + 2
Standard Library Access ✓

#check Nat.add_comm
Example: Natural Numbers

-- Natural number examples on FreeBSD 15.0

-- Basic theorem
theorem add_zero (n : Nat) : n + 0 = n := rfl

-- Proof by induction
theorem add_succ (n m : Nat) : n + Nat.succ m = Nat.succ (n + m) := rfl

-- Commutativity (from stdlib)
#check Nat.add_comm

-- Simple evaluation
#eval (List.range 10).map (· * 2)
Example: Propositional Logic

-- Propositional logic examples

-- Modus ponens
theorem modus_ponens (P Q : Prop) (hp : P) (hpq : P → Q) : Q :=
  hpq hp

-- Conjunction introduction
theorem and_intro (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
  ⟨hp, hq⟩

-- Conjunction elimination
theorem and_left (P Q : Prop) (h : P ∧ Q) : P :=
  h.left

theorem and_right (P Q : Prop) (h : P ∧ Q) : Q :=
  h.right

-- Disjunction
theorem or_intro_left (P Q : Prop) (hp : P) : P ∨ Q :=
  Or.inl hp

-- Double negation (classical)
theorem dne (P : Prop) : ¬¬P → P := by
  intro hnnp
  by_contra hnp
  exact hnnp hnp
Example: List Operations

-- List operations and proofs

def myLength : List α → Nat
  | [] => 0
  | _ :: xs => 1 + myLength xs

def myReverse : List α → List α
  | [] => []
  | x :: xs => myReverse xs ++ [x]

-- Prove length is preserved by reverse
theorem reverse_length (xs : List α) : (myReverse xs).length = xs.length := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
    simp [myReverse, List.length_append]
    omega

-- Map preserves length
theorem map_length (f : α → β) (xs : List α) : (xs.map f).length = xs.length := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp [ih]

#eval myReverse [1, 2, 3, 4, 5]
#eval myLength ["a", "b", "c"]
Example: Type Classes

-- Type class examples

class Monoid (α : Type) where
  unit : α
  op : α → α → α
  left_unit : ∀ x, op unit x = x
  right_unit : ∀ x, op x unit = x
  assoc : ∀ x y z, op (op x y) z = op x (op y z)

-- Natural numbers under addition form a monoid
instance : Monoid Nat where
  unit := 0
  op := (· + ·)
  left_unit := Nat.zero_add
  right_unit := Nat.add_zero
  assoc := Nat.add_assoc

-- List concatenation forms a monoid
instance : Monoid (List α) where
  unit := []
  op := (· ++ ·)
  left_unit := List.nil_append
  right_unit := List.append_nil
  assoc := List.append_assoc

-- Generic fold using monoid
def mconcat [Monoid α] (xs : List α) : α :=
  xs.foldl Monoid.op Monoid.unit

#eval mconcat [[1,2], [3,4], [5,6]]  -- [1, 2, 3, 4, 5, 6]
#eval mconcat [1, 2, 3, 4, 5]        -- 15
Lake Project Setup

Creating Projects

lake new creates a new project in a subdirectory:
lake new myproject
cd myproject && lake build


Initializing in Existing Directory

lake init initializes a project in the current directory:
mkdir -p /tmp/existingdir
cd /tmp/existingdir
lake init myproj
Common Mistake

Passing a path to lake init fails because it interprets the entire path as a package name:
lake init /tmp/test 2>&1 || true
Correct usage: navigate to directory first, then run lake init projectname.
Building a Project

cd myproject && lake build 2>&1 | head -10


Mathlib4 (Optional)

For advanced mathematics, add Mathlib4:
-- In lakefile.lean, add:
require mathlib from git
  "https://github.com/leanprover-community/mathlib4"
Then:
lake update
lake build
Note: Mathlib4 takes significant time to build (~30-60 min).
Emacs Integration

lean4-mode Setup

;; Lean4 mode for Emacs

(use-package lean4-mode
  :straight (lean4-mode
             :type git
             :host github
             :repo "leanprover/lean4-mode"
             :files ("*.el" "data"))
  :commands lean4-mode
  :mode ("\\.lean\\'" . lean4-mode)
  :config
  (setq lean4-keybinding-lean4-toggle-info "C-c C-i"))
Org-Babel Support

;; Add to init.el for org-babel lean4 support
(defun org-babel-execute:lean4 (body params)
  "Execute Lean4 code in org-babel."
  (let ((tmp-file (make-temp-file "lean4-" nil ".lean")))
    (with-temp-file tmp-file
      (insert body))
    (shell-command-to-string
     (format "lean --run %s 2>&1 || lean %s 2>&1" tmp-file tmp-file))))

(add-to-list 'org-babel-load-languages '(lean4 . t))
Validation Summary


  Test Status Notes
  Installation ✓ pkg install lean4
  procfs mounted ✓ Required for Lean
  lean –version ✓ 4.27.0-pre
  lake –version ✓ 5.0.0-src
  Theorem proving ✓ rfl, induction work
  #eval ✓ Evaluation works
  Standard library ✓ Nat, List, etc. accessible
  lake new ✓ Creates project in subdirectory
  lake init ✓ Initializes in current dir
  lake build ✓ Compiles projects successfully

Comparison: 14.3 vs 15.0


  Aspect FreeBSD 14.3 FreeBSD 15.0
  Lean version 4.23.0 4.27.0-pre
  Lake version 4.x 5.0.0-src
  procfs Required Required
  Core proving ✓ ✓
  Lake projects ✓ ✓
  Package size 1.90 GiB 2.20 GiB

References


  Lean 4 Official Site
  Lean Community
  FreeBSD 15.0 Release Notes
  Previous: Lean4 on FreeBSD 14.3
Feature	Description	Status
Native inotify	Linux-compatible file notification API	PASS
OpenZFS 2.4.0	Latest ZFS with improvements	PASS
OpenSSL 3.5	Post-quantum cryptography support	PASS
pkgbase	Base system installable via pkg	N/A
libsys separation	Cleaner syscall interface	PASS
Algorithm	Security Level	Notes
ML-KEM-512	NIST Level 1	Lightweight, fast
ML-KEM-768	NIST Level 3	Balanced (recommended)
ML-KEM-1024	NIST Level 5	Highest security
X25519MLKEM768	Hybrid	Classical + PQC combined
Component	Version
OS	FreeBSD 15.0-RELEASE-p1
Lean	4.27.0-pre
Lake	5.0.0-src
Package	lean4-4.25.2.20251201
Test	Status	Notes
Installation	✓	pkg install lean4
procfs mounted	✓	Required for Lean
lean –version	✓	4.27.0-pre
lake –version	✓	5.0.0-src
Theorem proving	✓	rfl, induction work
#eval	✓	Evaluation works
Standard library	✓	Nat, List, etc. accessible
lake new	✓	Creates project in subdirectory
lake init	✓	Initializes in current dir
lake build	✓	Compiles projects successfully
Aspect	FreeBSD 14.3	FreeBSD 15.0
Lean version	4.23.0	4.27.0-pre
Lake version	4.x	5.0.0-src
procfs	Required	Required
Core proving	✓	✓
Lake projects	✓	✓
Package size	1.90 GiB	2.20 GiB