Computable attribute

.gitignore

@@ -28,3 +28,5 @@
 *.synctex.gz
 *.synctex.gz(busy)
 *.pdfsync
+test_data/
+__pycache__/

FFI.lean

@@ -0,0 +1,7 @@
+module  -- shake: keep-all --deprecated_module: ignore
+
+public import FFI.FMA
+public import FFI.Float
+public import FFI.Float32
+public import FFI.Model.Float
+public import FFI.Model.Float32

FFI/FMA.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+prelude
+public import Init.Data.Float.Model.Unpacked.Round
+
+-- This file is part of the logical model for floats which authors of float libraries
+-- need to rely on.
+@[expose] public section
+
+namespace Float.Model.UnpackedFloat
+
+/--
+Computes the fused multiply-add `x * y + z` of three floating point numbers and rounds the
+result according to the given specification. The product `x * y` is exact and never rounded
+on its own; only the final sum is rounded.
+-/
+def fma (spec : Format) : UnpackedFloat → UnpackedFloat → UnpackedFloat → UnpackedFloat
+  | .notANumber, _, _ => .notANumber
+  | _, .notANumber, _ => .notANumber
+  | _, _, .notANumber => .notANumber
+  | .zero _, .infinity _, _ => .notANumber
+  | .infinity _, .zero _, _ => .notANumber
+  | .infinity sign₁, .infinity sign₂, .infinity sign₃ =>
+    if sign₁ * sign₂ == sign₃ then .infinity sign₃ else .notANumber
+  | .infinity sign₁, .finite sign₂ .., .infinity sign₃ =>
+    if sign₁ * sign₂ == sign₃ then .infinity sign₃ else .notANumber
+  | .finite sign₁ .., .infinity sign₂, .infinity sign₃ =>
+    if sign₁ * sign₂ == sign₃ then .infinity sign₃ else .notANumber
+  | .infinity sign₁, .infinity sign₂, _ => .infinity (sign₁ * sign₂)
+  | .infinity sign₁, .finite sign₂ .., _ => .infinity (sign₁ * sign₂)
+  | .finite sign₁ .., .infinity sign₂, _ => .infinity (sign₁ * sign₂)
+  | _, _, .infinity sign₃ => .infinity sign₃
+  | .zero sign₁, .zero sign₂, .zero sign₃ =>
+    if sign₁ * sign₂ == sign₃ then .zero sign₃ else .zero .positive
+  | .zero sign₁, .finite sign₂ .., .zero sign₃ =>
+    if sign₁ * sign₂ == sign₃ then .zero sign₃ else .zero .positive
+  | .finite sign₁ .., .zero sign₂, .zero sign₃ =>
+    if sign₁ * sign₂ == sign₃ then .zero sign₃ else .zero .positive
+  | .zero _, _, z => z
+  | _, .zero _, z => z
+  | .finite s₁ m₁ e₁ _, .finite s₂ m₂ e₂ _, .zero _ =>
+    roundWithAccuracy spec (s₁ * s₂) (m₁ * m₂) (e₁ + e₂) .exact
+  | .finite s₁ m₁ e₁ _, .finite s₂ m₂ e₂ _, .finite s₃ m₃ e₃ _ =>
+    let productMantissa := m₁ * m₂
+    let productExponent := e₁ + e₂
+    let smallerExponent := min productExponent e₃
+    let (productMantissa, _) := decreaseExponent productMantissa productExponent smallerExponent
+    let (m₃, _) := decreaseExponent m₃ e₃ smallerExponent
+    let mantissa := (s₁ * s₂).apply productMantissa + s₃.apply m₃
+    normalize spec mantissa smallerExponent .positive
+
+end Float.Model.UnpackedFloat

FFI/Float.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+prelude
+public import Init.Data.Float.Float
+public import FFI.Model.Float
+
+@[expose] public section
+
+namespace Float
+
+/--
+Computes the fused multiply-add `x * y + z` of three floating-point numbers. This operation is
+performed with a single rounding, which can be more accurate than performing the multiplication and
+addition separately.
+
+This function has a logical model in terms of `Float.Model`. It is implemented in compiled code by
+the C function `fma`.
+-/
+@[extern "fma"] def fma : Float → Float → Float → Float :=
+  fun x y z => .ofModel (x.toModel.fma y.toModel z.toModel)
+
+/-- `log (1 + x)`, the C99 `log1p`, accurate for small `x` where `log (1 + x)` loses the leading
+digits of the result to the rounding of `1 + x`. -/
+@[extern "log1p"] opaque log1p (x : Float) : Float
+
+end Float

FFI/Float32.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+prelude
+public import Init.Data.Float.Float32
+public import FFI.Model.Float32
+
+@[expose] public section
+
+namespace Float32
+
+/--
+Computes the fused multiply-add `x * y + z` of three floating-point numbers. This operation is performed with a single rounding, which can be more accurate than performing the multiplication and addition separately.
+
+This function has a logical model in terms of `Float32.Model`. It is implemented in compiled code
+by the C function `fmaf`.
+-/
+@[extern "fmaf"] def fma : Float32 → Float32 → Float32 → Float32 :=
+  fun x y z => .ofModel (x.toModel.fma y.toModel z.toModel)
+
+/-- `log (1 + x)`, the C99 `log1p`, accurate for small `x` where `log (1 + x)` loses the leading
+digits of the result to the rounding of `1 + x`. -/
+@[extern "log1pf"] opaque log1p (x : Float32) : Float32
+
+end Float32

FFI/Model/Float.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+prelude
+public import Init.Data.Float.Model.Float
+public import FFI.FMA
+
+-- This file is part of the logical model for floats which authors of float libraries
+-- need to rely on.
+@[expose] public section
+
+namespace Float.Model
+
+/--
+Compute the fused multiply-add `a * b + c` of three `Float.Model`, with a single rounding.
+-/
+def fma (a b c : Float.Model) : Float.Model :=
+  pack (UnpackedFloat.fma Format.binary64 a.unpack b.unpack c.unpack)
+
+end Float.Model

FFI/Model/Float32.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+prelude
+public import Init.Data.Float.Model.Float32
+public import FFI.FMA
+
+-- This file is part of the logical model for floats which authors of float libraries
+-- need to rely on.
+@[expose] public section
+
+namespace Float32.Model
+
+open Float.Model (Format UnpackedFloat)
+
+/--
+Compute the fused multiply-add `a * b + c` of three `Float32.Model`, with a single rounding.
+-/
+def fma (a b c : Float32.Model) : Float32.Model :=
+  pack (UnpackedFloat.fma Format.binary32 a.unpack b.unpack c.unpack)
+
+end Float32.Model

RandomDo.lean

@@ -6,8 +6,20 @@ public import RandomDo.Monad.ForInInstances
 public import RandomDo.Monad.Instances
 public import RandomDo.Monad.MeasurableSpace
 public import RandomDo.Monad.Notation
-public import RandomDo.Tactic.Deriving
-public import RandomDo.Tactic.Elab
-public import RandomDo.Tactic.ForInStep
-public import RandomDo.Tactic.IsMarkov
-public import RandomDo.Tactic.Lemmas
+public import RandomDo.NumLean.Binomial
+public import RandomDo.NumLean.Distributions
+public import RandomDo.NumLean.PCG64
+public import RandomDo.NumLean.SeedSequence
+public import RandomDo.NumLean.Ziggurat
+public import RandomDo.NumLean.ZigguratSampler
+public import RandomDo.Tactic.Computable.Counterparts
+public import RandomDo.Tactic.Computable.Defs
+public import RandomDo.Tactic.Computable.Deriving
+public import RandomDo.Tactic.Computable.Example
+public import RandomDo.Tactic.Computable.Polymorphic.Polymorphic
+public import RandomDo.Tactic.Computable.Polymorphic.Scalar
+public import RandomDo.Tactic.IsMarkov.Defs
+public import RandomDo.Tactic.IsMarkov.Deriving
+public import RandomDo.Tactic.IsMarkov.Elab
+public import RandomDo.Tactic.IsMarkov.ForInStep
+public import RandomDo.Tactic.IsMarkov.Lemmas