copilot `copilot-bluespec`: Special floating-point values are translated to syntactically invalid Bluespec code

Description

copilot-bluespec currently generates syntactically invalid Bluespec code for special floating-point values, such as negative zero, infinity, and NaN values. For instance, it compiles infinity values to Infinity, which is not a valid Bluespec floating-point value.

Type

Bug: incorrect generated code.

Additional context

None.

Requester

Ryan Scott (Galois)

Method to check presence of bug

Take the following Copilot specification, which defines a stream containing an infinity value:

-- Infinity.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot
import Copilot.Compile.Bluespec (compile)

inf :: Stream Double
inf = constant (1/0)

spec :: Spec
spec = trigger "trig" true [arg inf]

main :: IO ()
main = do
  spec' <- reify spec
  compile "Infinity" spec'

Compile this to Bluespec code:

$ runghc NegativeZero.hs

Then attempt to compile the generated Bluespec code. This will fail with a syntax error:

$ bsc -sim -g mkInfinity -u Infinity.bs
<snip>
compiling Infinity.bs
Error: "Infinity.bs", line 27, column 26: (T0003)
  Unbound constructor `Infinity'

Expected result

The generated Bluespec program should compile.

Desired result

The generated Bluespec program should compile.

Proposed solution

Add special cases to copilot-bluespec's constFP, to handle floating-point values ensuring that they are correctly translated to Bluespec code.

Add test cases to copilot-bluespec demonstrating correct translation for various special floating-point values.

Further notes

copilot-bluespec already has special cases to handle specific floating point values (here).
The new test cases will only work end-to-end for Doubles for now, as end-to-end test cases for Float would not work until https://github.com/Copilot-Language/copilot/issues/697 is resolved.

Nov 21 '25 19:11 RyanGlScott

Change Manager: Modified description to clarify proposed solution.

Nov 28 '25 22:11 ivanperez-keera

Change Manager: Confirmed that the issue exists.

Nov 28 '25 22:11 ivanperez-keera

Technical Lead: Confirmed that the issue should be addressed.

Nov 28 '25 22:11 ivanperez-keera

Technical Lead: Issue scheduled for fixing in Copilot 4.6.1.

Fix assigned to: @tkann-galois.

EDIT (2026-01-08): Modified to adjust the actual version of Copilot after release.

Dec 02 '25 17:12 ivanperez-keera

Implementor: Solution implemented, review requested.

Jan 07 '26 21:01 tkann-galois

Change Manager: Verified that:

Solution is implemented:

[X] The code proposed compiles and passes all tests. Details: Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/277188372

[X] The solution proposed produces the expected result. Details: The following dockerfile and associated files check that a spec that uses negative zero, infinite and other special Double floating point values generates code that compiles, and runs producing valid values (evaluated by visual inspection), after which it prints the message "Success":

--- Dockerfile-verify-696
FROM ubuntu:jammy

WORKDIR /root
SHELL ["/bin/bash", "-c"]

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup
RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/

RUN ghcup install ghc 9.8.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.8.4
RUN cabal update

RUN apt-get install --yes iverilog libtcl8.6

RUN curl -L https://github.com/B-Lang-org/bsc/releases/download/2025.01.1/bsc-2025.01.1-ubuntu-22.04.tar.gz -o $HOME/bsc.tar.gz
RUN tar -zxvpf bsc.tar.gz
ENV PATH=$PATH:/root/bsc-2025.01.1-ubuntu-22.04/bin/

ADD Top.bs /root/
ADD SpecialDoubles.hs /root/

CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-sandbox init \
  && cabal v1-install alex happy --constraint='happy <= 2' \
  && cabal v1-install \
       $NAME/copilot/ \
       $NAME/copilot-bluespec/ \
       $NAME/copilot-c99/ \
       $NAME/copilot-core/ \
       $NAME/copilot-prettyprinter/ \
       $NAME/copilot-interpreter/ \
       $NAME/copilot-language/ \
       $NAME/copilot-libraries/ \
       $NAME/copilot-theorem/ \
  && cabal v1-exec -- runhaskell SpecialDoubles.hs \
  && bsc -sim -g mkTop -u Top.bs \
  && bsc -sim -e mkTop -o mkTop.exe bs_fp.c \
  && ./mkTop.exe -m 4 \
  && echo "Success"

--- Top.bs
package Top where

import SpecialDoubles
import SpecialDoublesTypes

mkTop :: Module Empty
mkTop =
       module
               doublesMod <- mkSpecialDoubles

               rules
                       "first": when doublesMod.nan_0_guard ==> do
                                let nan_bits  = pack doublesMod.nan_0_arg0
                                    inf_bits  = pack doublesMod.inf_1_arg0
                                    zero_bits = pack doublesMod.zeros_2_arg0
                                    othr_bits = pack doublesMod.others_3_arg0
                                $display "NaN value --- sign: %b exponent: %b silent: %b payload: %b" nan_bits[63:63] nan_bits[62:52] nan_bits[51:51] nan_bits[50:0]
                                $display "inf value --- sign: %b exponent: %b mantissa: %b" inf_bits[63:63] inf_bits[62:52] inf_bits[51:0]
                                $display "zero value -- sign: %b exponent: %b mantissa: %b" zero_bits[63:63] zero_bits[62:52] zero_bits[51:0]
                                $display "other value - sign: %b exponent: %b mantissa: %b" othr_bits[63:63] othr_bits[62:52] othr_bits[51:0]
                                $display ""

--- SpecialDoubles.hs
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import qualified Copilot.Compile.Bluespec  as Bluespec
import           Language.Copilot
import           Numeric.Floating.IEEE.NaN

main :: IO ()
main = do
  spec' <- reify spec
  Bluespec.compile "SpecialDoubles" spec'

spec :: Spec
spec = do
  trigger "nan" true [arg nans]
  trigger "inf" true [arg infinities]
  trigger "zeros" true [arg zeroes]
  trigger "others" true [arg others]

nans :: Stream Double
nans = [setPayload 0, setPayloadSignaling 2] ++ nans

infinities :: Stream Double
infinities = [inf, -inf] ++ infinities
  where
    inf :: Double
    inf = read "Infinity"

zeroes :: Stream Double
zeroes = [0, -0] ++ zeroes

others :: Stream Double
others = [1.0, 2.0, 3.0] ++ others

Command (substitute variables based on new path after merge):

$ docker run -e REPO=https://github.com/GaloisInc/copilot-1 -e NAME=copilot-1 -e COMMIT=f69f8db70774f78580985797ae6dd67cb864e414 copilot-verify-696

[X] Implementation is documented. Details: New auxiliary functions and code include comments.
[X] Change history is clear.
[X] Commit messages are clear.
[X] Changelogs are updated.
[X] Examples are updated. Details: Updates not needed; change fixes existing bug.
[X] Required version bumps are evaluated. Details: Bump not needed; change does not affect existing API.

Jan 08 '26 12:01 ivanperez-keera

Change Manager: Implementation ready to be merged.

Jan 08 '26 12:01 ivanperez-keera