F* over TRAMP crashes

[R1kM]

I'm trying to run F* over TRAMP, and get the following error:

F*: subprocess exited. error in process filter: fstar-subp--process-response: Invalid state: Received orphan response "Json parsing failed." to query "?". Table of continuations was #s(hash-table size 65 test equal rehash-size 1.5 rehash-threshold 0.8 data ("1" [cl-struct-fstar-continuation "1" ignore (23654 55548 302255 44000)] "2" [cl-struct-fstar-continuation "2" #[128 "\302\300\303\301\"\"\207" [fstar-subp--overlay-continuation (#<overlay from 1 to 16 in Interop.fst/sshx:aymeric@aurorar8-0d73.wv.cc.cmu.edu:>) apply append] 6 "

(fn &rest ARGS2)"] (23654 55548 303432 11000)]))

My fstar-mode version is 20190129.603

[cpitclaudel]

:thinking: this is not looking good.
AFAICT, the remote F* process exited after complaining about an unparseable input. Can you run the same experiment after M-x fstar-toggle-debug? This should open an fstar-debug buffer with more clues for us to look at.

[R1kM]

Sure. From a slightly smaller file, I'm getting the following:

;;; Started F* interactive: ("fstar.exe" "/home/aymeric/everest/hacl-star/vale/code/arch/Arch.Types.fsti" "--ide" "--smt" "z3" "--smt" "/home/aymeric/everest/z3/bin/z3" "--include" "/home/aymeric/everest/hacl-star/specs/" "--include" "/home/aymeric/everest/hacl-star/obj/" "--include" "/home/aymeric/everest/hacl-star/vale/specs/interop" "--include" "/home/aymeric/everest/hacl-star/vale/code/crypto/sha" "--include" "/home/aymeric/everest/hacl-star/vale/code/crypto/poly1305/x64" "--include" "/home/aymeric/everest/hacl-star/vale/code/crypto/aes" "--include" "/home/aymeric/everest/hacl-star/vale/code/arch/x64/interop" "--include" "/home/aymeric/everest/hacl-star/vale/code/arch/x64" "--include" "/home/aymeric/everest/hacl-star/vale/code/arch" "--include" "/home/aymeric/everest/hacl-star/vale/code/lib/collections" "--include" "/home/aymeric/everest/hacl-star/vale/code/lib/math" "--include" "/home/aymeric/everest/hacl-star/vale/code/lib/util" "--include" "/home/aymeric/everest/hacl-star/vale/specs/crypto" "--include" "/home/aymeric/everest/hacl-star/vale/specs/defs" "--include" "/home/aymeric/everest/hacl-star/vale/specs/hardware" "--include" "/home/aymeric/everest/hacl-star/vale/specs/math" "--include" "/home/aymeric/everest/hacl-star/vale/code/crypto/ecc/curve25519/" "--max_fuel" "1" "--max_ifuel" "1" "--initial_ifuel" "0" "--z3cliopt" "smt.arith.nl=false" "--z3cliopt" "smt.QI.EAGER_THRESHOLD=100" "--z3cliopt" "smt.CASE_SPLIT=3" "--hint_info" "--use_hints" "--use_hint_hashes" "--cache_checked_modules" "--cache_dir" "/home/aymeric/everest/hacl-star/obj" "--use_extracted_interfaces" "true" "--smtencoding.elim_box" "true" "--smtencoding.l_arith_repr" "native" "--smtencoding.nl_arith_repr" "wrapped")
{"kind":"protocol-info","version":2,"features":["autocomplete","autocomplete/context","compute","compute/reify","compute/pure-subterms","describe-protocol","describe-repl","exit","lookup","lookup/context","lookup/documentation","lookup/definition","peek","pop","push","search","segment","vfs-add","tactic-ranges","interrupt","progress"]}
{"kind":"message","query-id":null,"level":"warning","contents":"Unable to open hints file: /home/aymeric/everest/hacl-star/vale/code/arch/Arch.Types.fsti.hints; ran without hints\n"}
{"kind":"message","query-id":null,"level":"info","contents":"(/home/aymeric/everest/hacl-star/vale/code/arch/Arch.Types.fsti) Unable to read hint file.\n"}
;;; Complete message received: (status: nil; message: ((kind . "protocol-info") (version . 2) (features "autocomplete" "autocomplete/context" "compute" "compute/reify" "compute/pure-subterms" "describe-protocol" "describe-repl" "exit" "lookup" "lookup/context" "lookup/documentation" "lookup/definition" "peek" "pop" "push" "search" "segment" "vfs-add" "tactic-ranges" "interrupt" "progress")))
;;; Complete message received: (status: nil; message: ((kind . "message") (query-id . :json-null) (level . "warning") (contents . "Unable to open hints file: /home/aymeric/everest/hacl-star/vale/code/arch/Arch.Types.fsti.hints; ran without hints
;;; ")))
;;; Complete message received: (status: nil; message: ((kind . "message") (query-id . :json-null) (level . "info") (contents . "(/home/aymeric/everest/hacl-star/vale/code/arch/Arch.Types.fsti) Unable to read hint file.
;;; ")))
;;; [18.33ms] Feature list received
;;; Processing queue
>>> {"query-id":"1","query":"vfs-add","args":{"filename":null,"contents":"module Arch.Types\n\nopen Types_s\nopen Collections.Seqs_s\nopen Collections.Seqs\nopen Words_s\nopen Words.Four_s\nopen Words.Seq_s\nopen Words.Seq\nopen FStar.Seq\nopen Words.Two_s\n\nunfold let ( *^ ) = nat32_xor\nunfold let ( *^^ ) = quad32_xor\n\nunfold let add_wrap32 (x:nat32) (y:nat32) : nat32 = add_wrap x y\nunfold let add_wrap64 (x:nat64) (y:nat64) : nat64 = add_wrap x y\n\nunfold let iand32 (a:nat32) (b:nat32) : nat32 = iand a b\nunfold let ixor32 (a:nat32) (b:nat32) : nat32 = ixor a b\nunfold let ior32 (a:nat32) (b:nat32) : nat32 = ior a b\nunfold let inot32 (a:nat32) : nat32 = inot a\nunfold let ishl32 (a:nat32) (s:int) : nat32 = ishl a s\nunfold let ishr32 (a:nat32) (s:int) : nat32 = ishr a s\n\nunfold let iand64 (a:nat64) (b:nat64) : nat64 = iand a b\nunfold let ixor64 (a:nat64) (b:nat64) : nat64 = ixor a b\nunfold let ior64 (a:nat64) (b:nat64) : nat64 = ior a b\nunfold let inot64 (a:nat64) : nat64 = inot a\nunfold let ishl64 (a:nat64) (s:int) : nat64 = ishl a s\nunfold let ishr64 (a:nat64) (s:int) : nat64 = ishr a s\n\nunfold let iand128 (a:nat128) (b:nat128) : nat128 = iand a b\nunfold let ixor128 (a:nat128) (b:nat128) : nat128 = ixor a b\nunfold let ior128 (a:nat128) (b:nat128) : nat128 = ior a b\nunfold let inot128 (a:nat128) : nat128 = inot a\nunfold let ishl128 (a:nat128) (s:int) : nat128 = ishl a s\nunfold let ishr128 (a:nat128) (s:int) : nat128 = ishr a s\n\nunfold let two_to_nat32 (x:two nat32) : nat64 = two_to_nat 32 x\n\nlet quad32_shl32 (q:quad32) : quad32 =\n  let Mkfour v0 v1 v2 v3 = q in\n  Mkfour 0 v0 v1 v2\n\nlet add_wrap_quad32 (q0 q1:quad32) : quad32 =\n  let open Words_s in\n  Mkfour (add_wrap q0.lo0 q1.lo0)\n         (add_wrap q0.lo1 q1.lo1)\n         (add_wrap q0.hi2 q1.hi2)\n         (add_wrap q0.hi3 q1.hi3) \n\nval lemma_BitwiseXorCommutative (x y:nat32) : Lemma (x *^ y == y *^ x)\nval lemma_BitwiseXorWithZero (n:nat32) : Lemma (n *^ 0 == n)\nval lemma_BitwiseXorCancel (n:nat32) : Lemma (n *^ n == 0)\nval lemma_BitwiseXorCancel64 (n:nat64) : Lemma (ixor n n == 0)\nval lemma_BitwiseXorAssociative (x y z:nat32) : Lemma (x *^ (y *^ z) == (x *^ y) *^ z)\n\nval xor_lemmas (_:unit) : Lemma\n  (ensures\n    (forall (x y:nat32).{:pattern (x *^ y)} x *^ y == y *^ x) /\\\n    (forall (n:nat32).{:pattern (n *^ 0)} n *^ 0 == n) /\\\n    (forall (n:nat32).{:pattern (n *^ n)} n *^ n == 0) /\\\n    (forall (n:nat64).{:pattern (ixor n n)} ixor n n == 0) /\\\n    (forall (x y z:nat32).{:pattern (x *^ (y *^ z))} x *^ (y *^ z) == (x *^ y) *^ z)\n  )\n\nval lemma_quad32_xor (_:unit) : Lemma (forall q . {:pattern quad32_xor q q} quad32_xor q q == Mkfour 0 0 0 0)\n\nlet quad32_double_lo (q:quad32) : double32 = (four_to_two_two q).lo\nlet quad32_double_hi (q:quad32) : double32 = (four_to_two_two q).hi\n\nval lemma_reverse_reverse_bytes_nat32 (n:nat32) :\n  Lemma (reverse_bytes_nat32 (reverse_bytes_nat32 n) == n)\n  [SMTPat (reverse_bytes_nat32 (reverse_bytes_nat32 n))]\n\nval lemma_reverse_bytes_quad32 (q:quad32) :\n  Lemma (reverse_bytes_quad32 (reverse_bytes_quad32 q) == q)\n  [SMTPat (reverse_bytes_quad32 (reverse_bytes_quad32 q))]\n\nval lemma_reverse_reverse_bytes_nat32_seq (s:seq nat32) :\n  Lemma (reverse_bytes_nat32_seq (reverse_bytes_nat32_seq s) == s)\n  [SMTPat (reverse_bytes_nat32_seq (reverse_bytes_nat32_seq s))]\n\nunfold let quad32_to_seq (q:quad32) : seq nat32 = four_to_seq_LE q\n\nlet insert_nat64_opaque = Opaque_s.make_opaque insert_nat64\n\nval lemma_insert_nat64_properties (q:quad32) (n:nat64) : \n  Lemma ( (let q' = insert_nat64_opaque q n 0 in\n            q'.hi2 == q.hi2 /\\\n            q'.hi3 == q.hi3) /\\\n           (let q' = insert_nat64_opaque q n 1 in\n            q'.lo0 == q.lo0 /\\\n            q'.lo1 == q.lo1))\n  [SMTPat (insert_nat64_opaque q n)]            \n         \nlet lo64_def (q:quad32) : nat64 = two_to_nat 32 (two_select (four_to_two_two q) 0)\nlet hi64_def (q:quad32) : nat64 = two_to_nat 32 (two_select (four_to_two_two q) 1)\n\nlet lo64 = Opaque_s.make_opaque lo64_def\nlet hi64 = Opaque_s.make_opaque hi64_def\n\nval lemma_lo64_properties (_:unit) :\n  Lemma (forall (q0 q1:quad32) . (q0.lo0 == q1.lo0 /\\ q0.lo1 == q1.lo1) <==> (lo64 q0 == lo64 q1))\n\nval lemma_hi64_properties (_:unit) :\n  Lemma (forall (q0 q1:quad32) . (q0.hi2 == q1.hi2 /\\ q0.hi3 == q1.hi3) <==> (hi64 q0 == hi64 q1))\n\nval lemma_equality_check_helper (q:quad32) :\n  Lemma ((q.lo0 == 0 /\\ q.lo1 == 0 ==> lo64 q == 0) /\\\n         ((not (q.lo0 = 0) \\/ not (q.lo1 = 0)) ==> not (lo64 q = 0)) /\\\n         (q.hi2 == 0 /\\ q.hi3 == 0 ==> hi64 q == 0) /\\\n         ((~(q.hi2 = 0) \\/ ~(q.hi3 = 0)) ==> ~(hi64 q = 0)) /\\\n         (q.lo0 == 0xFFFFFFFF /\\ q.lo1 == 0xFFFFFFFF <==> lo64 q == 0xFFFFFFFFFFFFFFFF) /\\\n         (q.hi2 == 0xFFFFFFFF /\\ q.hi3 == 0xFFFFFFFF <==> hi64 q == 0xFFFFFFFFFFFFFFFF)\n         )\n\nlet lemma_equality_check_helper_2 (q1 q2 cmp:quad32) (tmp1 result1 tmp2 tmp3 result2:nat64) : Lemma\n  (requires cmp == Mkfour (if q1.lo0 = q2.lo0 then 0xFFFFFFFF else 0)\n                          (if q1.lo1 = q2.lo1 then 0xFFFFFFFF else 0)\n                          (if q1.hi2 = q2.hi2 then 0xFFFFFFFF else 0)\n                          (if q1.hi3 = q2.hi3 then 0xFFFFFFFF else 0) /\\\n            tmp1 = lo64 cmp /\\\n            result1 = (if tmp1 = 0xFFFFFFFFFFFFFFFF then 0 else 1) /\\\n            tmp2 = hi64 cmp /\\\n            tmp3 = (if tmp2 = 0xFFFFFFFFFFFFFFFF then 0 else 1) /\\\n            result2 = tmp3 + result1)\n  (ensures (if q1 = q2 then result2 = 0 else result2 > 0))\n  =\n  lemma_equality_check_helper cmp;\n  ()\n\nval push_pop_xmm (x y:quad32) : Lemma\n  (let x' = insert_nat64_opaque (insert_nat64_opaque y (hi64 x) 1) (lo64 x) 0 in\n   x == x')\n\nval lemma_insrq_extrq_relations (x y:quad32) :  \n  Lemma (let z = insert_nat64_opaque x (lo64 y) 0 in\n         z == Mkfour y.lo0 y.lo1 x.hi2 x.hi3 /\\\n        (let z = insert_nat64_opaque x (hi64 y) 1 in\n         z == Mkfour x.lo0 x.lo1 y.hi2 y.hi3))\n\nval le_bytes_to_nat64_to_bytes (s:nat64) :\n  Lemma (le_bytes_to_nat64 (le_nat64_to_bytes s) == s)\n\nval le_nat64_to_bytes_to_nat64 (s:seq nat8 { length s == 8 }) :\n  Lemma (le_nat64_to_bytes (le_bytes_to_nat64 s) == s)\n\nval le_bytes_to_seq_quad32_to_bytes_one_quad (b:quad32) :\n  Lemma (le_bytes_to_seq_quad32 (le_quad32_to_bytes b) == create 1 b)\n\nval le_bytes_to_seq_quad32_to_bytes (s:seq quad32) :\n  Lemma (le_bytes_to_seq_quad32 (le_seq_quad32_to_bytes s) == s)\n\nval le_quad32_to_bytes_to_quad32 (s:seq nat8 { length s == 16 }) :\n  Lemma(le_quad32_to_bytes (le_bytes_to_quad32 s) == s)\n\nval le_seq_quad32_to_bytes_of_singleton (q:quad32) :\n  Lemma (le_quad32_to_bytes q == le_seq_quad32_to_bytes (create 1 q))\n\nval le_quad32_to_bytes_injective: unit ->\n  Lemma (forall b b' . le_quad32_to_bytes b == le_quad32_to_bytes b' ==> b == b')\n\nval le_quad32_to_bytes_injective_specific (b b':quad32) :\n  Lemma (le_quad32_to_bytes b == le_quad32_to_bytes b' ==> b == b')\n\nval seq_to_four_LE_is_seq_to_seq_four_LE (#a:Type) (s:seq4 a) : Lemma\n  (create 1 (seq_to_four_LE s) == seq_to_seq_four_LE s)\n\nval le_bytes_to_seq_quad_of_singleton (q:quad32) (b:seq nat8 { length b == 16 }) : Lemma\n  (requires q == le_bytes_to_quad32 b)\n  (ensures create 1 q == le_bytes_to_seq_quad32 b)\n\nval le_bytes_to_quad32_to_bytes (q:quad32) :\n  Lemma(le_bytes_to_quad32 (le_quad32_to_bytes q) == q)\n\nlet be_quad32_to_bytes (q:quad32) : seq16 nat8 =\n  seq_four_to_seq_BE (seq_map (nat_to_four 8) (four_to_seq_BE q))\n\nval be_bytes_to_quad32_to_bytes (q:quad32) :\n  Lemma (be_bytes_to_quad32 (be_quad32_to_bytes q) == q)\n  [SMTPat (be_bytes_to_quad32 (be_quad32_to_bytes q))]\n\nlet reverse_bytes_quad32_seq (s:seq quad32) : seq quad32 =\n  seq_map reverse_bytes_quad32 s\n\nval lemma_reverse_reverse_bytes_quad32_seq (s:seq quad32) :\n  Lemma (reverse_bytes_quad32_seq (reverse_bytes_quad32_seq s) == s)\n  [SMTPat (reverse_bytes_quad32_seq (reverse_bytes_quad32_seq s))]\n\nopen FStar.Mul\n\nval lemma_le_seq_quad32_to_bytes_length (s:seq quad32) : \n  Lemma(length (le_seq_quad32_to_bytes s) == (length s) * 16)\n  \n\nval slice_commutes_seq_four_to_seq_LE (#a:Type) (s:seq (four a)) (n:nat{n <= length s}) (n':nat{ n <= n' /\\ n' <= length s}) :\n  Lemma(slice (seq_four_to_seq_LE s) (n * 4) (n' * 4) ==\n        seq_four_to_seq_LE (slice s n n'))\n\nval slice_commutes_le_seq_quad32_to_bytes (s:seq quad32) (n:nat{n <= length s}) (n':nat{ n <= n' /\\ n' <= length s}) :\n  Lemma(slice (le_seq_quad32_to_bytes s) (n * 16) (n' * 16) ==\n        le_seq_quad32_to_bytes (slice s n n'))\n\nval slice_commutes_le_seq_quad32_to_bytes0 (s:seq quad32) (n:nat{n <= length s}) :\n  Lemma(slice (le_seq_quad32_to_bytes s) 0 (n * 16) ==\n        le_seq_quad32_to_bytes (slice s 0 n))\n\n(*\nval slice_commutes_le_bytes_to_seq_quad32 (s:seq nat8 { length s % 16 == 0 }) (n:nat{n * 16 <= length s}) :\n  Lemma(length (le_bytes_to_seq_quad32 s) == length s / 16 /\\\n        slice (le_bytes_to_seq_quad32 s) 0 n ==\n        le_bytes_to_seq_quad32 (slice s 0 (n*16)))\n*)\n\nval append_distributes_le_bytes_to_seq_quad32 (s1:seq nat8 { length s1 % 16 == 0 }) (s2:seq nat8 { length s2 % 16 == 0 }) :\n  Lemma(le_bytes_to_seq_quad32 (s1 @| s2) == (le_bytes_to_seq_quad32 s1) @| (le_bytes_to_seq_quad32 s2))\n"}}
>>> {"query-id":"2","query":"push","args":{"kind":"full","code":"module Arch.Types\n","line":1,"column":0}}
{"kind":"response","query-id":"?","status":"protocol-violation","response":"Json parsing failed."}
;;; Complete message received: (status: "protocol-violation"; message: ((kind . "response") (query-id . "?") (status . "protocol-violation") (response . "Json parsing failed.")))
{"kind":"message","query-id":"2","level":"progress","contents":{"stage":"loading-dependency","modname":"prims"}}
;;; Complete message received: (status: nil; message: ((kind . "message") (query-id . "2") (level . "progress") (contents (stage . "loading-dependency") (modname . "prims"))))
;;; Signal received: [killed
;;; ] [signal]

[cpitclaudel]

Thanks. It looks like F is receiving a bad JSON message, although what fstar-mode sends seems fine. Could you patch F to print back the JSON string before exiting? The change to make is in src/fstar/Fstar.Interactive.Ide.fs, in parse_interactive_query; I'd suggest adding query_str like this: ProtocolViolation ("Json parsing failed: " ^ query_str)

[R1kM]

This is weird, even by adding this (both on my local and remote F* versions), I still only get "Json parsing failed." without any more information

[cpitclaudel]

Are you using the OCaml build or the F# build?

[R1kM]

I'm not sure, I'm simply running make in the FStar directory to get an executable

[R1kM]

Btw, I have a simple workaround for this (running emacs with ssh -X instead of over TRAMP), so there is no need to spend a huge amount of time debugging :)

[cpitclaudel]

Hmm. This shouldn't matter, in fact :/ The debug log should show exactly which F* is run; can you make sure that it's the recompiled one?

[cpitclaudel]

Sorry, I missed your last message before posting mine. The workaround is great, but I'd like to get to the bottom of this nonetheless :)

[R1kM]

I think you were right, it was using the recompiled version, but apparently the OCaml one for which the F# change wasn't propagated. Below is the output for the file available here: https://github.com/project-everest/hacl-star/blob/8e739b1cd3159148da3e43b0eea3b128e24702d5/vale/code/arch/x64/interop/Cpuid_stdcalls.fst

It seems that the string given is partial, and stops in the middle of line 62. Do I need to modify a setting to remove a length limit on data sent over TRAMP?

Warning (emacs): Unknown status "protocol-violation" from F* subprocess (response was ["Json parsing failed with request{\"query-id\":\"1\",\"query\":\"vfs-add\",\"args\":{\"filename\":null,\"contents\":\"module Cpuid_stdcalls\\nopen Interop.Base\\nmodule IX64 = Interop.X64\\nmodule VSig = Vale.AsLowStar.ValeSig\\nmodule LSig = Vale.AsLowStar.LowStarSig\\nmodule V = X64.Vale.Decls\\nmodule IA = Interop.Assumptions\\nmodule W = Vale.AsLowStar.Wrapper\\nopen X64.MemoryAdapters\\n\\nmodule VC = X64.Cpuidstdcall\\n\\n(* A little utility to trigger normalization in types *)\\nlet as_t (#a:Type) (x:normal a) : a = x\\nlet as_normal_t (#a:Type) (x:a) : normal a = x\\n\\n[@__reduce__]\\nlet dom: IX64.arity_ok_stdcall td = []\\n\\n(* Need to rearrange the order of arguments *)\\n[@__reduce__]\\nlet aesni_pre : VSig.vale_pre 8 dom =\\n  fun (c:V.va_code)\\n    (va_s0:V.va_state)\\n    (sb:IX64.stack_buffer 8) ->\\n      VC.va_req_check_aesni_stdcall c va_s0 IA.win (as_vale_buffer sb)\\n\\n[@__reduce__]\\nlet aesni_post : VSig.vale_post 8 dom =\\n  fun (c:V.va_code)\\n    (va_s0:V.va_state)\\n    (sb:IX64.stack_buffer 8)\\n    (va_s1:V.va_state)\\n    (f:V.va_fuel) ->\\n      VC.va_ens_check_aesni_stdcall c va_s0 IA.win (as_vale_buffer sb) va_s1 f\\n\\n(* The vale lemma doesn't quite suffice to prove the modifies clause\\n   expected of the interop layer *)\\n[@__reduce__] unfold\\nlet aesni_lemma'\\n    (code:V.va_code)\\n    (_win:bool)\\n    (va_s0:V.va_state)\\n    (sb:IX64.stack_buffer 8)\\n : Ghost (V.va_state & V.va_fuel)\\n     (requires\\n       aesni_pre code va_s0 sb)\\n     (ensures (fun (va_s1, f) ->\\n       V.eval_code code va_s0 f va_s1 /\\\\\\n       VSig.vale_calling_conventions_stdcall va_s0 va_s1 /\\\\\\n       aesni_post code va_s0 sb va_s1 f))\\n = VC.va_lemma_check_aesni_stdcall code va_s0 IA.win (as_vale_buffer sb)\\n\\n(* Prove that vm_lemma' has the required type *)\\nlet aesni_lemma = as_t #(VSig.vale_sig_stdcall aesni_pre aesni_post) aesni_lemma'\\nlet code_aesni = VC.va_code_check_aesni_stdcall IA.win\\n\\n(* Here's the type expected for the check_aesni wrapper *)\\n[@__reduce__]\\nlet lowstar_aesni_t =\\n  IX64.as_lowstar_sig_t_weak_stdcall\\n    Interop.down_mem\\n    code_aesni\\n    8\\n    dom\\n    []\\n    _\\n    _\\n    (W.mk_prediction code_aesni dom [] (aesni_lemma code_aesni IA.win))\\n\\n(* And here's the check_aesni wrapper itself *)\\nlet lowstar_aesni : lowstar_aesni_t  =\\n  IX64.wrap_weak_stdcall\\n    Interop.down_mem\\n    code_aesni\\n    8\\n    dom\\n    (W.mk_prediction code_aesni dom [] (aesni_lemma code_aesni IA.win))\\n\\nlet lowstar_aesni_normal_t //: normal lowstar_aesni_t\\n  = as_normal_t #lowstar_aesni_t lowstar_aesni\\n\\nlet check_aesni () =  \\n  let x, _ = lowstar_aesni_normal_t () in //This is a call to the interop wrapper\\n  x\\n\\n(* Need to rearrange the order of arguments *)\\n[@__reduce__]\\nlet sha_pre : VSig.vale_pre 8 dom =\\n  fun (c:V.va_code)\\n    (va_s0:V.va_state)\\n    (sb:IX64.stack_buffer 8) ->\\n      VC.va_req_check_sha_stdcall c va_s0 IA.win (as_vale_buffer sb)\\n\\n[@__reduce__]\\nlet sha_post : VSig.vale_post 8 dom =\\n  fun (c:V.va_code)\\n    (va_s0:V.va_state)\\n    (sb:IX64.stack_buffer 8)\\n    (va_s1:V.va_state)\\n    (f:V.va_fuel) ->\\n      VC.va_ens_check_sha_stdcall c va_s0 IA.win (as_vale_buffer sb) va_s1 f\\n\\nopen X64.Machine_s\\nopen X64.Vale.State\\n\\n#set-options \\\"--z3rlimit 20\\\"\\n\\n(* The vale lemma doesn't quite suffice to prove the modifies clause\\n   expected of the interop layer *)\\n[@__reduce__] unfold\\nlet sha_lemma'\\n    (code:V.va_code)\\n    (_win:bool)\\n    (va_s0:V.va_state)\\n    (sb:IX64.stack_buffer 8)\\n : Ghost (V.va_state & V.va_fuel)\\n     (requires\\n       sha_pre code va_s0 sb)\\n     (ensures (fun (va_s1, f) ->\\n       V.eval_code code va_s0 f va_s1 /\\\\\\n       VSig.vale_calling_conventions_stdcall va_s0 va_s1 /\\\\\\n       sha_post code va_s0 sb va_s1 f))\\n = VC.va_lemma_check_sha_stdcall code va_s0 IA.win (as_vale_buffer sb)\\n \\n(* Prove that vm_lemma' has the required type *)\\nlet sha_lemma = as_t #(VSig.vale_sig_stdcall sha_pre sha_post) sha_lemma'\\nlet code_sha = VC.va_code_check_sha_stdcall IA.win\\n\\n(* Here's the type expected for the check_aesni wrapper *)\\n[@__reduce__]\\nlet lowstar_sha_t =\\n  IX64.as_lowstar_sig_t_weak_stdcall\\n    Interop"])

[cpitclaudel]

How odd. Thanks for investigating. There shouldn't be a length limit on data sent through Tramp. What exact path do you use? /ssh:, or /sshx:?

[R1kM]

I'm using /sshx:/

[cpitclaudel]

Can you try with /ssh:?

[pnmadelaine]

I ran into the same issue. I applied the patch you suggested to the compiler and the query is clearly truncated after a few thousands characters. The problem doesn't seem to occur for smaller files. I'm using /sshx:, /ssh: doesn't work for me and always leads to a timeout, even on smaller files.

[pnmadelaine]

The files are truncated after ~4300 characters. The limit is not exactly the same from file to file, but a given file is always cut at the same spot.

[cpitclaudel]

Sounds like the same issue as above: are you using sshx or ssh? TTYs truncate inputs at 4096 characters.

[pnmadelaine]

Sorry for the delayed response: I'm using sshx because using ssh causes a timeout. It's the first time I use sshx and I don't really know much about it, how is it that TTY limitations apply here?